基于自动机的Java程序运行时验证框架及其安全性和锁序反转的讨论

理论计算机科学电子笔记144（2006）109-124www.elsevier.com/locate/entcs使用ANOJ的Volker Stolz1和Eric Bodden1部计算机科学编程语言与程序分析亚琛工业大学52056Aachen，Germany摘要我们提出了一个Java程序的运行时验证框架。属性可以在线性时间时态逻辑（LTL）中指定，在AJ切入点上。这些属性在程序执行过程中通过基于自动机的方法进行检查，其中转换通过方面触发。不需要Java源代码，因为ANOJ在字节码级别上工作，因此甚至允许第三方应用程序的插装作为一个例子，我们讨论了安全性和锁序反转。关键词：自动验证，LTL，AIBJ，面向方面编程，交替自动机。1引言为了避免不当行为，许多软件产品包括断言，该断言检查执行路径上的某些状态是否满足给定的约束，以及其他情况下是否中止执行或执行特定的错误处理。这些断言通常仅限于测试变量的值。然而，不仅对单个状态进行推理，而且对一系列状态进行推理，往往是方便的。这使开发人员能够推理控制流程和执行路径。在以前的工作[15]中，我们讨论了有限路径上参数化LTL公式的符号检查器，它允许我们例如。来推理在多线程应用程序中发现的通常称为锁顺序反转的问题。在运行时，将指出1Ema il：{stolz，bodden}@ i2. 为了我的一个提克。rw th-a aa ch e n。De1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.007110诉Stolz，E.Bodden/Electronic Notes in Theoretical Computer Science 144（2006）109给开发商。我们已经实现了一个工作原型，具有类似的功能，Java应用程序使用符号检查器的基础上，我们在下面描述的代码生成方法这项工作的主要贡献是提出了一种替代的，基于自动机的解决方案，允许更多的表现力，虽然产生更好的性能。前一种方法的一个主要缺点是，驱动检查器的注释必须插入到被测应用程序的源代码中。出于实用的目的，我们提供了一个带注释的并发库替换。因此，希望使用此框架的应用程序必须重新编译。此外，这种基于源代码的钩子可能会导致严重的面向对象属性问题，例如行为子类型：为某个类声明的任何规范也应该适用于它的所有子类。在方法体中使用源代码注释并不遵循这样的隐式规则。因此，我们以这样一种方式限制我们的形式主义，即它只允许推理定义良好的接口，即方法调用和字段访问。Valgrind [11]最近的成功表明，对更好的调试支持有足够的需求（与模型检查等技术相比在第2节中，我们对时序逻辑做了一个简短的介绍。 我们不是符号化地检查公式，而是将其转换为交替自动机。第3节讨论了（Java）应用程序的插装，并重点介绍了AIBJ中的面向方面编程第4节中的LTL和AIBJ的组合为每个公式产生了一个状态机，通过一个有限自动机进行检查，其中转换由一个方面驱动。我们讨论了参数化自动机的一个扩展，用于处理带有状态的循环模式，并在第5节中得出结论2从LTL到交替自动机在本节中，我们给出了LTL的有限路径语义，并提醒读者如何将LTL公式转换为交替自动机。2.1LTL的路径语义线性时间时态逻辑（LTL）[12]是计算树逻辑CTL的子集，并使用描述沿计算路径的事件的运算符扩展命题逻辑。含义：• “Next”诉Stolz，E.Bodden/Electronic Notes in Theoretical Computer Science 144（2006）109111• “Finally”• “Globally” (G• “Until”• “释放”（Release）：U的对偶;表示第二个属性沿着路径保持直到并包括第一个属性保持的第一个状态，尽管第一个属性最终不需要保持。LTL通常定义为无限路径。对于运行时验证，我们假设验证过程在某个时间点停止，相应地，LTL公式必须在有限路径上求值。因此，我们声明语义如下。设PROP是一组原子命题，w = w [1]. n是一条有限的路径。F或每个路径p∈{ p 1，.，p ∈ {p1，.，以及式I和式II：w[j]|=tt，w[j]|=ff,w[j]|=p我的p∈w[j]|= Xϕ我的j当前命题=int n>（）;（）：p1（）{ currentPropositions.add（p1）; }（）：p2（）{ currentPropositions.add（p2）;}after（）：p1（）||publicvoid run（）{state= state.transition（currentPropositions）; if（state.equals（Formula.TT））{//将公式报告为满足} else if（state.equals（Formula.FF））{//将公式报告为伪造}state.clear（）; //重置命题向量}}图3.第三章。方面实现第9页的初始化示例见图4。仪器步骤可以在运行时检查是否符合给定的公式4.4开销由于触发断言评估的钩子，验证通常必须在插装的应用程序中引入某种开销这个开销与公式的数量和公式的长度成线性关系。 调用、执行和设置切入点仅必要时，由APDJ执行。 if（）切入点可能导致任意大的开销。因此，不应在公式内进行这种昂贵的评估。只要点-120诉Stolz，E.Bodden/Electronic Notes in Theoretical Computer Science 144（2006）109cut被限制为字段匹配，如if（User.loggedIn），开销相当低。通过使用ANOJ作为实现策略，我们自动继承了ANOJ实现所带来的所有强大优化功能。特别是，与早期的方法相反，对于不导致对给定公式之一的进一步评估的连接点，根本没有开销例如，公式G（！call（C.f（）只会是当C.f（）被真正调用时，它会被求值。我们相信，我们的实现是有效的，考虑到我们的形式主义的表现力，除了通常的开销引入的使用面向方面的编程，这是已知的是在该地区不超过百分之二相比，基于非模块化的实现。通过对abc编译器的不断改进，这种开销可能会减少ANOJ编织器确保只在需要插装以触发计算的位置关于这一点，实现具有最佳的低开销。当静态地预计算完整的转换表时，我们在每个这样的插装点上支付的成本可以分为• 对方面实例的虚方法调用的开销，• 相关自动机的状态变化，由一个整数组合和一个整数赋值组成前者很可能随着weaver实现的改进而被消除一旦完全支持内联，甚至这个虚方法调用也会消失。后者是不可避免的。当公式需要状态时，必须进行一些这是下一节的主题。4.5锁序反转我们使用一个更复杂的例子来激发对参数化公式的需求：为了避免锁序反转的问题（参见。[6]，[15]），我们想通过一个LTL公式断言，如果两个锁以特定的顺序被使用（其间没有解锁），如果用户也以交换的顺序使用这些锁，系统应该警告用户，因为在并发程序中，这意味着当两个线程的执行被安排在一个不幸的顺序时，它们可能会死锁。注意，在这个例子中，我们并不想中止执行：我们在这里只对警告感兴趣，因为违反公式可能不会2与M的沟通Webster，IBM Hursley Performance Labs，2003年诉Stolz，E.Bodden/Electronic Notes in Theoretical Computer Science 144（2006）109121与僵局同时发生。为了观察整个执行路径的行为（其中错误行为可能只是子路径），我们将公式包装到时态全局中。因此，如果我们考虑一个带有显式锁定和解锁方法的类Lock，就像我们在任何编程语言中找到它们一样，我们得到两个线程pi，pj和两个锁lx，ly的公式（如果LTL是一种适当的指定语言，它是可验证的）：<$lock（pi，ly）U（lock（pi，lx）<$（<$unloc k（pi，lx） Ulock（pi，ly）→G<$（<$lock（pj，lx）U（lock（pj，lx）<$（<$unlock（pj，lx），ij，x/=y请注意，该公式有四个参数：两个锁和两个线程。使用当前的实现，这意味着我们必须预先生成所有可能的公式实例。这种预生成可以基于固定的最大锁和线程数，也可以基于运行时的锁/线程创建。这两种方法都有缺点。第一个将忽略任何大于指定上限的值后者需要对对象创建和当前跟踪进行额外的插装，由于内存原因，这通常限于运行的一个子进程在这个例子中，线程标识符应该作为参数传递，尽管在典型的实现中它可能是隐式的（例如，存储在特殊变量中或可通过API获得）。为了在我们的形式主义中表达这种此附加功能的实现正在进行中，将在未来的演示文稿中介绍绑定可以很容易地通过AFA中的约束（附加合取）来建模，其中约束的更新和检查与在线评估密切相关。将上面的公式转换为允许变量绑定的LTL语法的新变体，将得到以下表达式(we为了清楚起见，区分LTL和AALJ中的逻辑运算符pointcut lock（Threadt，Lockl）：call（Lock.lock（Thread））args（t）target（l）;pointcut unlock（Threadt，Lockl）：call（Lock.unlock（Thread））args（t）target（l）;螺纹i，j;锁紧x，y;<$lock（i，y）U（lock（i，x）<$（<$unlock（i，x）U（lock（i，y）<$<$target（x）→G<$（<$lock（j，x）U（lock（j，y）<$args（i）<$（<$unlock（j，y） Ulock（j，x）变量绑定的工作原理类似于Prolog：第一次调用包含target或args的方面将变量绑定到当前值。 所有其他引用同一变量的事件都被转换为谓词。新122诉Stolz，E.Bodden/Electronic Notes in Theoretical Computer Science 144（2006）109跟踪的不同匹配部分的绑定将导致相关子公式的新的具体化这具有为由隐含的左手侧观察到的每个行为生成单独的公式的期望效果5相关工作JavaPathExplor er[7]由于Havelund和Ros，使用了一种指定运行时行为的类似方法。它们使用类似的有限路径上的LTL语义，尽管它们的方法不是基于AOPWalker和Viggers [16]提出了一种对AJ语言的扩展，即trace-cuts.跟踪切割不像切入点那样匹配执行流程中的事件，而是匹配这些事件的跟踪 这些轨迹通过切入点上的上下文无关表达式来指定。由于这种方法提供了一种语言扩展，因此不能与普通的Java编译器结合使用。Tracecut不提供状态的自动跟踪受到这项工作的启发，Allan等人[1]用tracematches扩展了abc编译器，允许在切入点表达式中绑定自由变量这解决了严格基于在执行期间实际出现的那些值来为参数的每个有效组合绑定上述公式的问题ABC中的实现遵循与我们在[15]中提出的方法类似的思想然而，Allan等人在他们的模型中没有使用交替自动机。我们感觉使用AFA作为底层表示，绑定可以以一种非常自然的方式融合Klose和Ostermann [9]讨论了时态关系如何用GAMMA（一种在最小面向对象核心语言之上的面向方面语言）来切入点是用类似Prolog的语言指定的，包括可以使用谓词isbefore/after进行比较的时间戳。它们的原型需要一个已经存在的跟踪来应用方面，并且不适用于现有的语言。Java-MaC[8]是Java的运行时保证工具。Meta事件定义语言（MEDL）用于指定安全属性。由于MaC架构应该是独立于语言的，因此原始事件定义语言（PEDL）提供了与目标语言（这里是Java）的绑定。虽然Java-PEDL被设计为与Java紧密对应，但它并不像ANOJ那样使用自如，因为表达式不是在Java之后建模的，而是实际上是Java表达式。此外，MEDL中的状态似乎仅限于原始类型。Valgrind [11]是一个通过在运行时检测x86程序来分析它们的系统提供了用于检测内存管理和线程错误的工具扩展Valgrind应该是自然的选择，如果应用程序诉Stolz，E.Bodden/Electronic Notes in Theoretical Computer Science 144（2006）109123编译为本机代码（例如，从C或C++）应被检测。事实上，早期版本包含一个实现Eraser算法的工具，该算法可以检测多线程程序中的数据竞争[14]。Temporal Rover[4]是Time Rover，Inc.它通过源到源转换处理嵌入在注释中的LTL断言6结论和今后的工作我们已经提出了一个运行时验证框架，基于面向方面的编程与ANOJ。将以切入点为性质的LTL公式转化为自动机。通过方面，我们在执行过程中“遍历”自动化，通过进入错误状态来检测违规。我们目前的实现支持完整的形式主义，但没有访问运行时状态。我们讨论的参数化公式，克服了这个问题的改进一旦这个实现完成，最终的工具将提供一种形式主义，它比我们所知道的任何以前的方法更有表现力，更自然地面向对象推理。LTL的一个局限性是，它限制我们只能推理规则属性，而上下文无关的属性通常也很有趣重新考虑4.1节中的例子，其中有一个变化，即希望指定“C.f（）的每个调用最终都跟有一个对C.g（）的匹配调用“。即应当单个C.g（）不再可能释放多个C.f（）. 然而，将表达能力提高到上下文无关属性的能力并不是微不足道的[2]。虽然我们的方法应该能够处理这样的虽然我们可以通过跟踪状态来解决问题，但我们还缺乏一个合适的LTL语言扩展来利用这一点。在并发系统的上下文中，同步点对应用程序的行为至关重要 ANOW J已经允许匹配同步d_m_e_th_d_s，尽管不是同步的（ob_j）{. }-blocks。不幸的是，通常不可能静态地确定匹配编译后，在字节码级别上执行monitorenter和monitorescort指令。但是，这可以动态地解决。我们的Java逻辑观察器JLO原型可以从http://www-i2.informatik.rwth-aachen.de/JLO/网站。引用[1] C. Allan，P. Av gu st inov，A. S. 西蒙湖 H endr en，S. Ku zins，O. 好了，奥。 deMor，D. 塞雷尼G. Sittamplan和J. Tibble。将跟踪匹配添加到AASPJ（提交给OOPSLAabc技术报告abc-2005-01，麦吉尔大学，2004年。124诉Stolz，E.Bodden/Electronic Notes in Theoretical Computer Science 144（2006）109[2] R. K.K. Etessami和P. Madhusudan。 嵌套调用和返回的时态逻辑。 在K. Jensen和A.Podelski，编辑，Tools and Algorithms for the Construction and Analysis ofSystems（TACAS 2004），计算机科学讲义第2988卷。Springer，2004.[3] P. Av gu st inov，A. S. Chr istensen，L. H endr en，S. 库兹因斯，J。 好了，奥。 我会的。deMor，D.塞雷尼湾Sittampalam和J. Tibble。abc：一个可扩展的AIBRJ编译器。在AOSD '05 ：Proceedings of the Fourth International Conference on AEO-oriented Software Development中。ACM Press，2005.[4] D. 德鲁辛斯基时空漫游者和ATG漫游者在K。 Havelund，J. Penix，andW. Visser，editors，SPIN Model Checking and Software Verification（7th InternationalSPIN Workshop），Volume 1885 ofLecture Notes in Computer Science，pages 323斯普林格。[5] B. Finkbeiner和H.B.西普玛使用交替自动机检查有限迹。系统设计中的形式化方法，24（2）：101[6] K. 哈夫隆 使用可扩展性分析指导Java程序的模型检查 在K. Havelund ， J.Penix 和 W.Visser ， editors ， SPIN Model Checking and SoftwareVerification （ 7th International SPIN Workshop ） ， Volume 1885 ofLecture Notes inComputer Science，Stanford，USA，2000.斯普林格。[7] K. 他是一个很好的人。 Rosu. AnOverviewofheRuntimeVerifica t ionTolJavaPathEx p l.系统设计中的形式化方法，24（2）：189[8] M.金，M。Viswanathan，S.卡南岛Lee和O.V. Sokolsky。Java-MaC：Java程序的运行时保证方法。系统设计中的形式化方法，24（2）：129-155，2004。[9] K. Klose和K.奥斯特曼回到未来：切入点作为跟踪上的谓词。在2005年，美国芝加哥，面向语言的基础讲习班（FOAL[10] T. Lindholm和F.耶琳JavaTM虚拟机规范Addison-Wesley，1997年。[11] N.内瑟科特和J·苏厄德。Valgrind：一个程序监督框架。在第三次研讨会上验证（RVElsevierScience Publishers，2003.[12] A. 普努埃利程序的时序逻辑1977年，第18届IEEE计算机科学基础研讨会论文集[13] G. Roosuand d K. 好的。从逻辑公式中提取最小动态范围。技术报告01-15，高级计算机科学研究所（RIACS），2001年。[14] S.萨维奇，M。Burrows，G. Nelson，P. Sobalvarro，and T.安德森Eraser：A Dynamic DataRace Detector for Multi Threaded Programs.ACM Transactions on Computer Systems，15（4），1997.[15] 诉 Stolz 和 F. 哈 。 并 发 Haskell 程 序 的 验 证 在 K 。 Havelund and G. Rosu ， editors ，ForurthWorkshoponRuntimeVerication（RVElsevier Science Publishers.[16] R.J. Walker和K.维格斯通过声明性事件模式实现协议。在RN。泰勒和M.B.Dwyer，编辑，第12届软件工程基础国际研讨会。ACM，2004年。