Java Card字节码程序中的静态事务分析与格式良好性验证.

理论计算机科学电子笔记141（2005）145-162www.elsevier.com/locate/entcsJava Card字节码Renn'eRydhofHansen1信息学与数学建模技术大学千克林比伊戈尔·A. Siveroni2帝国理工学院计算机系英国伦敦摘要在Java Card字节码程序中使用事务可能相当棘手，需要程序员特别注意，以解决一些限制，并避免由于事务的不当使用而引入严重的运行时错误在本文中，我们提出了一种新的分析，结合控制和数据流分析的分析，跟踪在Java卡字节码程序中的活动事务。我们正式证明了分析的正确性，并展示了它如何可以用来解决上述问题，保证在Java Card字节码程序中的交易是格式良好的，从而不会引起运行时错误。关键词：Java Card字节码，格式良好的事务，静态分析，流逻辑1引言智能卡越来越多地用于需要一定安全性的应用中，例如电子地铁票和电子钱包。智能卡也是每个GSM手机的核心，1电子邮件：rrh@imm.dtu.dk2电子邮件：siveroni@doc.ic.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.032146R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）所谓的SIM（用户识别模块）卡实际上是智能卡。智能卡应用程序的广泛部署和通常的敏感性使得在智能卡上运行的程序必须正确执行。Java卡是一种特殊类型的智能卡，它具有卡上Java卡虚拟机，使其能够以Java方言为这种智能卡开发程序这些程序然后被编译成Java字节码的方言，称为Java Card虚拟机语言（JCVML）或Java Card字节码。JCVML程序的一个特殊问题是使用事务（一种确保变量原子更新的机制JCVML不允许事务嵌套，即，在任何给定时刻只能有一个打开的事务。尝试打开另一个事务将导致运行时错误;这也是在没有打开的事务时尝试关闭事务的结果。由于JCVML程序的性质，事务甚至可以以不同的方法打开和关闭，并取决于程序中的特定数据流。这使得实际上很难确保事务确实是格式良好的。在本文中，我们将展示如何以前开发的控制和数据流分析的JCVML类似的语言称为卡梅尔，一个合理的重建JCVML具有相同的表达能力的JCVML，但更适合于正式的方法，可以扩展到跟踪交易，并最终表明，一个给定的程序的交易确实是良好的形式，因此，该程序将永远不会引起一个交易相关的运行时错误。相关工作。 在[7]中，它显示了如何通过自动生成JML（Java建模语言）在Java Card程序中强制执行高级安全和安全属性，参见。[1]，注释为程序。事务的良构性是可以使用这种技术验证的高级属性的一个例子我们不知道任何针对Java Card字节码的相关工作，使用静态分析来解决这个问题似乎很新颖。2格式良好的事务JCVML API提供了对一个众所周知的基本工具的访问，用于在所述情况下确保数据和程序的完整性，即事务。事务保证在事务中发生的更新的原子性，即，或者所有更新都成功，或者没有一个更新成功。然而，智能卡上的资源相当有限，因此不允许嵌套JCVML事务，即，一次只能有一个活动事务：任何开始新事务的尝试R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）147cvoidatomicWrapper（byte[]，short）//T我们的团队0：API。getTransactionDepth//{0}1：如果le0转到4//{0}2：按1//键3：goto 5//跳4：push 0//{0}5：存储3//{0}6：加载3//{0}7：如果ne 0转到9//{0}8：API. 已完成事务//{0}9：加载0//{1}10：加载1//{1}11：load 2//{1}12：invokevirtualdossomething（byte[]，short）//{1}13：加载3//{1}14：ifne 0 goto 16//{1}15：API. transcommittsaction//{1}16：return//{0}}TD1{1}下一页{1}下一页{1}下一页{1}下一页∅{1}下一页{1}下一页{1}下一页∅{1}下一页{1}下一页{1}下一页{1}下一页{1}下一页{1}下一页∅{1}下一页Fig. 1. 包装器方法当一个事务已处于活动状态时，另一个事务将导致抛出异常; 2同样，如果在没有活动事务时尝试关闭事务（通过提交或中止），则将抛出异常最后，当程序终止时，必须没有活动的事务如果给定程序中任何可能的执行路径上的事务都不违反上述规则，则该程序的事务被称为良构的。由上述事务语义施加的限制导致了防御性编程风格，其中在开始新事务之前显式地检查事务是否在进行中，并且类似地在尝试关闭事务之前检查事务是否活动。此外，程序员经常必须“解决”不能嵌套事务的限制，并且这导致了事务的非平凡控制流程，其中事务可以在一个方法中开始并且在另一个方法中提交（或中止），这可能取决于第一个方法是否在事务已经在进行中的上下文中这些问题共同使得程序员很难确保事务确实是格式良好的，因为必须考虑所有可能的程序执行使用也可能打开或关闭事务的异常会使情况进一步复杂化。在第4节中，我们开发了一个程序分析，可以用来静态地保证程序中的所有事务都是良构的。在图1中，显示了一个称为atomicWrapper的Carmel方法，以说明具体的Carmel语法和上面讨论的有关事务的问题这个例子取自一个演示小程序，一个电子148R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）一个叫DeMoney的钱包，经过修改以适应我们的语言。它是由TrustedLogic作为SecSafe项目的一部分创建的[8]，并在[5]中指定。请注意，我们使用最后请注意，Carmel与JCVML一样，是一种基于堆栈的语言。atomicWrapper方法旨在用作一个名为dossomething（第9-12行）的方法的它说明了上面讨论的问题：如果在活动事务中调用包装器方法atomicWrapper，那么它不能启动新事务;这首先获取当前事务深度（第0行），然后在第1-5行中，根据当前事务深度，在局部变量号“3”中记录“0”或“1”（第1行中使用的“le”运算符是Carmel的小于或等于“0”运算符）。最后，在开始事务之前（第6-8行，其中第7行中使用的ne运算符是Carmel's not equal，' /='，operator）检查局部变量“3”的值(in第8行），那么它也应该在此方法中提交（第133卡梅尔语完整的JCVML包括100多条指令和一个全面的API，它实现了各种有用的例程，包括访问虚拟机我们没有指定对JCVML的分析Carmel语言是JCVML的抽象：它抽象了大部分面向实现的细节，例如，常量池，同时保留了JCVML的全部表达能力，实际上从JCVML到Carmel有一Carmel语言的语法和语义在[9，10]中有详细的定义和讨论出于演示目的，我们只包括展示主要见解所需的说明和功能Carmel的指令集包括堆栈操作、局部变量、对象生成、字段访问、简单条件、抛出异常以及方法调用和返回的指令：Instr：：= pushc|流行音乐|努莫普|新σ|调用虚拟m|| 返回|getfieldf|普特菲尔德F|如果cmpOp转到pc0|负载x|存储x|扔R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）149此外，我们还从API中包含了访问交易功能的说明Instr：：= ... | API.beginTransaction| API.commitTransaction|API.abortTransaction |A P I .getTransactionDepth一个卡梅尔程序，P ∈ Program，被定义为它声明的类的集合：P。班每个类σ∈Class包含一组方法σ。方法和场σ。菲尔德·菲尔德。每个由用于每个程序计数器的指令组成，在方法m中，pc∈N0。计算At（pc）∈Instr.为了清晰起见，我们将使用类似于JCVML的具体语法，如图1所示。3.1语义Carmel的语义是一个简单的，虽然涉及，结构操作语义（SOS），并在[9]中详细描述在本节中，我们将介绍一个简化版本的Carmel语义，它更适合于研究和呈现手头的问题。主要的简化是，也许有点令人惊讶的是，实际的底层事务机制的删除：而不是定义一个完整的事务语义，我们只是抽象出底层事务机制，只跟踪一个特殊语义组件中的事务深度。应该注意的是，虽然这种抽象对于证明和呈现目的来说非常方便，但它并没有使问题更容易解决，因此，跟踪事务深度对于我们的目的来说是足够的。一个值可以是一个数字或者一个对象引用（一个位置）：Val=+ObjRef。全局堆是从对象引用到对象的映射：Heap=ObjRef→Object，其中对象只是从字段名到值的映射：Object=Field→Val。对象是从类实例化的，我们使用o。class表示对象的类o∈Object。在JCVML中，只有Throwable类的对象可以用作异常，为了简单起见，我们允许任何类用作异常：Exception=Class。对操作数堆栈进行建模作为一个值序列：Stack=Val和局部堆（对于方法的局部变量）作为从（局部）变量到值的映射：LocHeap=Var→Val。堆栈帧记录当前事务深度（只能是0或1）、当前方法和程序计数器以及本地堆和操作数堆栈。为了方便我们的证明，我们还用上下文注释了当前方法，即，初始调用时的事务深度（0或1）。因此，一个带注释的方法（m，τm）属于定义域Method×{0，1}，iswrittenmτm。然后，由Frame={ 0， 1}×（Method×{0， 1}）×N0×LocHeap ×Stack给出s个堆栈帧的域。 例外情况定义了一个特殊的框架：ExcFrame={ 0， 1}×ObjRef×Method×N0。150R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）有了语义域，我们现在可以指定语义配置和归约规则。配置是运行配置或最终配置：Conf = RunConf + FinConf。运行配置的形式为：H，F：：SF，其中H∈Heap，SF∈ Frame，且F=πτ，mτm，pc，L，Sπ ∈Frame，说明程序是通用的在具有局部堆L和操作数栈S的方法m中的程序计数器pc处执行指令，并且该方法在事务深度τm中被调用，或者F= ττ，locX，mX，pcX<$∈ExcFrame，这意味着在方法mX中的程序计数器pcX处已经抛出异常，其中locX指向异常对象。如果τ= 1，则在活动事务内执行指令，如果τ= 0，则在当前指令处没有事务在进行中（注意，这当然可以不同于调用方法的转换深度：τm）。 最终配置的形式如下：表示程序在事务深度τ中终止，返回值为v（如果没有返回值，则v=v对于给定的程序P∈Program，这导致了以下形式的归约规则：P<$C=<$CJ对于C，CJ∈Conf。图2显示了一些有趣的指令的语义规则，完整的语义可以在[9]中找到（完整）事务API的语义如图3所示。在invokevirtual（方法调用）的归约规则中，我们必须注意正确处理动态分派在JCVML中，这是通过使用一个函数methodlogs来表示类层次结构来完成的 它接受一个方法标识符mJ和一个类o。类，作为参数，并返回方法，mv，其实现了mJ的主体，即，类中mJ的最新定义等级制度。 在同一个规则中，请注意，对对象的引用被传递给对象本身在局部变量0中。最后要注意的是，由格式不正确的事务引起的运行时错误被建模为卡住的配置。由于空间不足，仅显示实际返回值的return-指令。注意，必须处理两种情况：一种是“正常”方法返回，另一种是程序终止，即，在空调用栈上执行返回指令对于throw指令，我们使用finds函数（参见[9] A定义和解释）来检查是否存在被抛出的异常的本地处理程序;如果不存在，则将特殊的异常帧放在调用堆栈的顶部。这与官方的JCVM略有偏差，以便于SOS定义语义和证明分析的正确性在API的语义中需要注意的主要事情是，只有当当前事务深度为0时，开始事务（API. STIM事务）才会成功，即，没有其他交易正在进行中。类似地，使用指令API.commitTransaction提交或中止事务，R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）151vm.PractionAt（pc）=pushcPH，τ，mτm，pc，L，S：：SF=H，τ，mτm，pc+1，L，c：：S：：SFm.PractionAt（pc）=popPH，τ，mτm，pc，L，c：：S：：SF=H，τ，mτm，pc+1，L，S：：SFm. pactionAt（pc）=invokevirtualmJS= v1：：···：：v|M'|：：loc：：S0→v1，.，|›→V| M '|]|]PH，τ，mτm，pc，L，S：：SF=H，τ，mτ，0，LJ，G：：τ，mτm，pc，L，S：：SFm. parallel At（pc）=returnPH，τJ，mJτm'，pcJ，LJ，v：：SJ：：τ，mτm，pc，L，S：：SF=H，m. parallel At（pc）=returnPH，τ，mτm，pc，L，v：：S：：G=H，τ，Retvjm. pk10（pc）=throw如果finds（m，pc，H（locX）.class）=pc0，则f τ，mτm，pc 0，L，SF=πτ，locX，m，pc如果finds（m，pc，H（locX）.class）=πPH，τ，mτm，pc，L，locX：：S：：SF=H，F：：SF图二. 语义规则（节选）m. getTransactionAt（pc）=API.getTransactionDepthPH，τ，mτm，pc，L，S：：SF=H，τ，mτm，pc+1，L，τ：：S：：SFm. applicationAt（pc）=API. applicationTransactionPH，0，mτm，pc，L，S：：SF=PH，1，mτm，pc+1，L，S：：SFm. applicationAt（pc）=API.commitTransactionPH，1，mτm，pc，L，S：：SF=PH，0，mτm，pc+1，L，S：：SFm. abortationAt（pc）=API.abortTransactionPH，1，mτm，pc，L，S：：SF=PH，0，mτm，pc+1，L，S：：SF图三. 事务API或API.abortTransaction分别，只有在事务当前处于活动状态时才成功这意味着API. commitTransaction应该仅在当前事务深度为零的上下文执行，并且API.commitTransaction和API.abortTransaction指令应该仅如果当前事务深度为1，则执行这在下面的定义3.2中被正式化从上面和前一节的讨论中应该清楚，对于程序员来说，手动检查程序并保证所有可能的执行路径的所有事务总是格式良好的，即使不是不可能的，也是非常为了总结语义，我们需要定义初始配置。Carmel程序，如JCVML小程序，可以有多个入口点。为了简单起见，并且不失一般性，我们假设每个类σ都有一个入口点，记为mσ，带一个参数，一个对调用对象的（自）引用（记为locσ）：152R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）σ定义3.1（初始配置）如果P∈Program，则C是初始配置当且仅当C=H，0，m0，0，[0 <$→locσ]，：：和H（locσ）。class= σ，其中σ ∈ P. 类，mσ是σ的入口点。请注意，最初没有打开的事务 为了便于参考，我们定义P。入口是程序P的入口点集合。我们现在可以正式定义良构的概念：定义3.2（良构性）设C0是P∈Program的初始配置，且设C1∈Conf使得P∈C0= P∈C1，则P的事务称为良构的当且仅当对于所有配置C1=PH，Pτ，mτm，pc，L，Sτ：：SF，下式成立：(i) M. JumtionAt（pc）=API. JumtransactionJumper= 0(ii) M. ApproximationAt（pc）=API.commitTransactionapproximation=1(iii) M. AbortAction（pc）=API.abortTransaction（pc）= 1对于所有的构形C1= H，τ，Retv，τ = 0。4控制、数据和交易流分析在本节中，我们将介绍一个组合的控制、数据和事务流程分析，它可用于验证程序是否以格式良好的方式使用事务。该分析基于先前开发的控制和数据流分析（参见[4，3]的完整讨论）;这些分析然后扩展为跟踪活动交易的分析 ， 我 们 称 之 为 交 易 流 分 析 。 事 务 处 理 流 分 析 （ transaction crowthanalysis，TFA）跟踪程序中每条指令可能的事务处理深度（保守近似）我们已经发现，为了获得我们的目的所需的精度，TFA必须是上下文相关的分析（参见[6]），其中上下文被视为调用给定方法的事务深度;因此只有两种可能的上下文，即零和一，这极大地限制了复杂性的增加，这通常是由于将上下文添加到分析中4.1抽象领域数字的抽象域反映了这样一个事实，即我们需要跟踪常数，而不是涉及常数的计算，因为任何使用操纵或计算的事务深度值都很难验证（手动和自动），并且应该被视为高度可疑：Z=ZT。 我们将把ZT的顶元素写成INT。对于对象引用，我们遵循“通常”的R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）153[11]中的图形，并将对象引用抽象到它们相应的类中：ObjRef=Class。如果需要更高的精度，可以使用基于[11]的文本对象图的抽象然而，对于典型的Java Card程序，前者是完全可以接受的，因为很少有类被实例化超过一次。为了便于阅读，我们将σ∈ObjRef写成（Refσ）。抽象异常的定义域与类的定义域相同：Exception=ObjRef。一个值要么是一个数字，要么是一个对象引用;这很容易直接建模为：Val+ObjRef，然后我们将使用这些值的集合作为我们的抽象值：Val=P（Val+ObjRef）。如上所述，分析是上下文相关的，其中事务深度（在方法调用时）为上下文：上下文={ 0， 1}。我们遵循Freund和Mitchell的方法，参见。[2]，并跟踪每个指令和每个上下文的本地堆和操作数堆栈（以及事务深度）;这使得对本地堆、操作数堆栈和事务深度的分析是低敏感的（过程内），这对于跟踪事务深度的变化和分析在开始或结束事务之前检查事务深度的情况是由于一条指令是由一个方法和一个程序计数器唯一确定的，为了方便起见，我们引入地址的概念：地址=方法×N0。然后，局部堆被建模为一个映射，对于每个上下文和地址，从（局部）变量到抽象值：LocHeap=Context→Addr→Var→Val。堆栈被建模为抽象值的序列（同样，每个上下文一个和指令）：Stack=Context→Addr→（Valt）T。一个bs道堆一个真正的so以一种简单的方式建模，作为从对象引用到抽象对象：堆=上下文→对象引用→对象。抽象对象是从字段到抽象值的映射：Object=Field→Val。要跟踪不在本地处理的异常，需要使用异常缓存：ExcCache=Context→Method→ P（Exception）。最后，为了跟踪每条指令的事务深度，我们使用以下公式：Trans=Context→Addr→ P（{0， 1}）。4.2流程逻辑规范流逻辑框架是一种面向规范（而不是面向实现）的程序分析方法。而不是详细说明如何进行分析的框架是用来指定它意味着什么分析结果是一个可接受的，或正确的，分析的程序。这种分离使得在框架中指定分析非常方便，并且通常会产生（相对）清晰和简洁的规范。我们对控制、数据和交易分析的判断采用以下四个因素（H、L、S、E、T、D）：|=（ m0，pc0） ：instr意味着（pro-posed）分析是（H，L，S，E，TD），是指令的正确近似。154R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）（H，L，S，E，TD）|=（m0，pc0）：API.getTransactionDepthi <$δ∈T<$D{0，1}（m0，0）：T<$Dδ（m0，pc0）/=∞TDδ（m0，pc0）±TDδ（m0，pc0+ 1）<$δJ∈T<$Dδ（m0，pc0）：{δJ}：：S<$δ（m0，pc0）±S<$δ（m0，pc0+1）Lδ（m0，pc0）±Lδ（m0，pc0+1）（H，L，S，E，TD）|=（m0，pc0）：API.交易i<$δ∈T<$D{0，1}（m0，0）：T<$Dδ（m0，pc0）/=∞{1}ΔTΔDδ（m0，pc0+1）S<$δ（m0，pc0）±S<$δ（m0，pc0+1）Lδ（m0，pc0）±Lδ（m0，pc0+1）（H，L，S，E，TD）|=（m0，pc0）：API.commitTransaction <$δ∈T<$D{0，1}（m0，0）：T<$Dδ（m0，pc0）/=∞{0}TDδ（m0，pc0+1）S<$δ（m0，pc0）±S<$δ（m0，pc0+1）Lδ（m0，pc0）±Lδ（m0，pc0+1）见图4。 事务API在程序代码PC中使用的方法instrl，∈Heap，L∈LocHeap，S∈∈Stack，E ExcCache，以及 TD∈Trans. 稍后我们将展示如何提升它以覆盖整个程序并考虑初始配置。在图4、5和6中显示了流逻辑规范的摘录，完整规范可以在[4，3]中找到。请注意，为了增强流逻辑规范的可读性，我们使用换行符和缩进，而不是显式地写出所有的合取运算符。出于篇幅考虑，我们只详细讨论一些指令有关分析的控制流程和数据流程方面的完整讨论，请参见[4，3]。为了便于理解和简洁，我们引入了简写符号：TD{0，1}（m，pc）来表示TD0（m，pc）<$TD1（m，pc）。由于我们的分析是上下文相关的分析，其中上下文是调用当前方法（表示为m）的事务深度所有指令的规范都预先定义为<$δ∈T<$D{0，1}（m0，0）以确保考虑调用当前方法的所有可能上下文然后，该抽象上下文被用作操作的抽象域的索引，并被写为子脚本，例如，δ在是的。考虑到上述情况，现在可以分析API.getTransactionDepth指令了（如图4所示）。首先，我们必须确保在-结构在所有可能的上下文中被分析，当前方法已经被调用，但我们只继续分析，如果当前指令实际上是在这样的上下文中执行的这表示如下由所有指令施加的条件：T <$δ ∈ T<$D{0，1}（m0，0）：T<$Dδ（m0，pc0）/=T。注意，在给定上下文中可到达的所有指令δ将具有R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）155TDδ（m0，pc0）因此，上述含义的前提可以看作是一个简单的可达性测试，通过忽略无法访问的指令和上下文。现在，分析指令的结果很简单：由于该指令不会改变事务深度，因此仅复制性新符号：T<$Dδ（m0，pc0）<$T<$Dδ（m0，pc0+ 1）. 接下来，当前的抽象事务深度被放在堆栈的顶部，指令：<$δJ∈T<$Dδ（m0，pc0）：{δJ}：：S<$δ（m0，pc0）±S<$δ（m0，pc0+1），其中±是抽象值的有限序列的逐点扩张。菲-最后，由于没有修改局部变量，它们只是被复制到下一个指令：Lδ（m0，pc0）±L<$δ（m0，pc0+1）. 这里是point-wise将图中的图推广到定义域Var→Val中的映射。的规格API. transaction非常相似，只是这里的transaction深度发生了变化;在执行指 令 之 后 ， transaction 深 度 肯 定 为 1 ： {1} transactiontransactiontransactiondegreeδ（m0，pc0+ 1）。其余交易指令的分析类似，我们不再赘述这里.invokevirtual指令的流逻辑规范（参见图5）主要由将实际参数移动到被调用方法的公式组成，并确保复制返回值，具体语义的运作方式我们在这里不详细讨论这方面的分析，只参考[4]。就本文的目的而言，关于invokevirtual的分析，第一个值得注意的有趣之处是当前抽象上下文如何作为基本上下文： δJ∈TDδ（m0，pc0）：{δJ} TDδJ（mv，0），其中mv是通过搜索类层次结构找到的调用方法的理由：建筑请注意，δJ既用作值，也用作索引。第二件要注意的事情是，被调用的方法的上下文（即事务深度的值）如何被写回调用方法，返回：T<$DδJ（mv，ENDmv）<$T<$Dδ（m0，pc0+1）. 这里（mv，ENDmv）是 一个spe-以类似于“exit”的方式使用方法“m v“的控制流图中的节点请注意，由于被调用的方法可能会改变事务深度，因此我们只需使用从被调用的方法返回的上下文，并忽略调用时的上下文。除了与方法调用相关的正常控制流程之外，我们还必须为此，HANDLE谓词是156R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）（H，L，S，E，TD）|=（m0，pc0）：invokevirtualm我的 ∀δ∈TˆD{0,1}(m0,0):TˆDδ(m0,pc0)∅⇒A1：：· ··：：A|M|：：B：：XaSδ（m0，pc0）：（Refσ）∈B：mv=methods（m，σ）<$δJ∈T<$Dδ（m0，pc0）：{δJ}TDδ'（mv，0）{（Refσ）}：：A1：：· · ·：：A|M|±Lδ'（mv，0）[0. |]|]T<$Dδ'（mv，ENDmv）<$T<$Dδ（m0，pc0+1）<$（（RefσX），TX）∈E<$δ（mv）：HANDLE（Lδ，SδEδ，TDδ）（（RefσX），TX，（m0，pc0））A：：aSδ'（mv，ENDmv）：A：：X±Sδ（m0，pc0+1）Lδ（m0，pc0）±Lδ（m0，pc0+1）（H，L，S，E，TD）|=（m0，pc0）：throw我的 ∀δ∈TˆD{0,1}(m0,0):TˆDδ(m0,pc0)∅⇒B：：XaS<$δ（m0，pc0）：（RefσX）∈B：手柄（（RefσX），TDδ（m0，pc0），（m0，pc0））（Lδ，SδEδ，TDδ）定义：图五. 方法调用和异常抛出手LE（L<$δ，S<$δE<$δ，T<$Dδ）（（RefσX），TX，（m，pc））finds（m，pc，σX）=σ x（（RefσX），TX）∈E<$δ（m）finds（m，pc，σX）=pcX{（RefσX）}±S<$δ（m，pcX）L<$δ（m，pc）±L<$δ（m，pcX）TX<$T<$Dδ（m，pcX）谓词使用findlist函数来检查给定的异常是否有本地处理程序。如果不存在本地处理程序，则异常和事务深度TX被保存在缓存中;如果找到处理程序，则堆栈、本地堆和事务深度被向前复制到处理程序。throw指令（参见图5）只是使用上面定义的HANDLE谓词，根据在堆栈顶部找到的对象引用抛出一个异常由于事务深度只应被存储和加载，而不应在计算中使用（以便于验证事务深度的正确使用），因此简单的常量跟踪分析是足够的，尽管如果需要，可以用更精确的数据流分析来代替它。本数据流分析的简单性在算术运算分析中最为明显（见图6），因为所有运算都会导致INT（INT的顶部元素）被推到堆栈上{INT}：：X±S<$δ（m0，pc0+1）.R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）157（H，L，S，E，TD）|=（m0，pc0）：numopop我的 <$δ∈T<$D {0，1}（m0，0）：T<$Dδ（m0，pc0）=/∅⇒A1：：A2：：XaS<$δ（m0，pc0）：{INT}：：X±S<$δ（m0，pc0+1）Lδ（m0，pc0）±Lδ（m0，pc0+1）T<$Dδ（m0，pc0）<$T<$Dδ（m0，pc0+1）（H，L，S，E，TD）|=（m0，pc0）：ifcmpOpgotopc我的 <$δ∈T<$D {0，1}（m0，0）：T<$Dδ（m0，pc0）=/∅⇒A1：：A2：：XaS<$δ（m0，pc0）：c^ond（cmp Op，A1，A2）Sδ（m0，pc0）±Sδ（m0，pc）Lδ（m0，pc0）±Lδ（m0，pc）T<$Dδ（m0，pc0）<$T<$Dδ（m0，pc）c^ond（<$cmp Op，A1，A2）S<$δ（m0，pc0）±S<$δ（m0，pc0+1）Lδ（m0，pc0）±Lδ（m0，pc0+1）T<$Dδ（m0，pc0）<$T<$Dδ（m0，pc0+1）图六、算术运算和条件运算的流逻辑摘录条件句更有趣，这里我们定义了两个抽象比较谓词，指示是否可以采取真和/或假分支：c^on d（cmpOp，A1，A2）（INT∈A1<$A2）<$（<$n1∈A1<$n2∈A2：cmpOp（n1，n2））这是利用可达性属性来提高分析精度的另一个示例我们现在可以提升分析以覆盖整个程序。在这里，我们必须确保考虑初始配置（H，L，S，E，TD）|=Pin（m，pc）∈P. 地址：M. 指令At（pc）=instr（H，L，S，E，TD）|=（m，pc）：instrσ∈P。（Refσ）∈L<$0（mσ，0）<${0}<$T<$D0（mσ，0）4.3语义正确性为了证明分析的语义正确性，我们采取了类似于[6]的方法，并定义了所有语义对象的表示函数和程序配置之间的正确性关系然后，我们表明，分析保持这些评估下，通过建立一个主题减少分析的属性。因为我们做的是简单的常数跟踪，所以数字被简单地表示为它们自己：β（n）={n}。在分析规范中，对数字的任何算术运算都导致INT。位置只有相对于给定堆，因此位置的表示函数需要相关的158R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）ObjRefObjRef对象ValVal堆叠ValValValObjRefheap作为附加参数： 如果H（锁定）。类=σ，则βH（loc）={（Refσ）}。Carmel中的值是数字或位置，因此值的表示函数：β（v），对于v∈和βH（五）v∈ObjRef. 抽象对象被简单地认为是从场到抽象值：βH（o）（f）= βH（o. （f）。 堆将位置映射到对象。由于同一个类的所有对象都被表示为同一个抽象对象，堆的表示函数必须找到给定类的所有对象，然后使用这些对象的表示（最小上界）.β堆（H）（参考σ）=loc ∈dom（H）βH（loc）=（Refσ）H对象 （H（loc））抽象堆栈是抽象值的序列，导致一个直接的-堆栈的ward表示函数：βH（v1：：···：：vn）=βH（v1）：：···：βH（vn）。局部堆有一个类似的简单表示函数：HLocHeap（L）（x）=βH（L（x））.有了基本语义域的表示函数我们现在可以将这些定义提升到堆栈框架和语义配置。为此，我们使用正确性关系来指定何时在分析中正确表示堆栈帧或语义配置第一个堆栈帧：mτm，pc，L， SH（L<$，S<$，T<$D）i <$ τ∈T<$D（m，pc）企业简介HLocHeapτm（L）±Lτm（m，pc）H堆叠(S) 公司简介（m，pc）从本质上说，上述正确性关系只是简单地说，状态框架中的语义对象的抽象表示应该包含在分析中。 唯一需要注意的是事务深度在当前方法被称为（方法m上的τm注释）作为分析的一个参数，例如， Sτm（m，pc）. 它扩展到覆盖整个调用堆栈（堆栈帧序列），并注意处理异常通过传播不在本地处理的异常来正确地处理帧F1：：···：：FnZH调用堆栈（L，S，TD） ii∈ {2，...，n}：ZH帧（L，S，TD）F=πτ，mτm1，pc， L， SπFRH（L，S，TD）1 111 111帧F1=πτX，l ocX，mX，pcXπ（βH（H（l ocX）. class），{τX}）∈E<$δ（mX）运行配置的正确性关系定义如下：ββββRRR.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）159H，SF<$R<$ RunConf（H<$，L<$，S<$，E<$，T<$D）i <$βHeap（H）±H<$pZH帧 （L，S，TD）SFR160R.R. 汉森，内务部。Siveroni/Electronic Notes in Theoretical Computer Science 141（2005）最终配置处理起来特别简单H，τ，CRConf（H，L，S，E，TD）iC∈RunConfCRRunConf（H，L，S，E，TD）C∈FinConfCRFinConf（H，L，S，E，TD）我们现在可以声明并证明分析规范在语义上是正确的。这是通过建立用于分析的主题归约属性来完成的通过证明分析结果在执行下是不变的：定 理 4.1 （ 合 理 性 ） 若 P∈C0 为 初 始 配 置 的 程 序 ， 且 A| = P 使 得P<$C0=<$$>C1且P<$C1=<$C2则C1R<$ ConfA蕴涵C2R<$ ConfA。证据 通过对求值序列长度的归纳，结合实例分析，利用一个技术引理证明调用栈是良构的。Q5形式良好在本节中，我们将展示如何使用上一节中讨论的分析来静态验证Carmel程序中的事务确实是格式良好的。下面我们定义了一个程序的属性，并对该程序进行了分析，描述了如何使用该分析来保证程序具有格式良好的事务：定义5.1（静态良构性）一个程序P，被称为具有静态良构的遍历，其中h为A=（H，L，S，E，TD）当且仅当A|= P，对于instr= m。在（pc）处，以下成立：(i) instr=API. xml事务处理TD{0，1}（m，pc）{0}(ii) instr=API.commitTransaction测试ID{0，1}（m，pc）验证{1}(iii) instr=API.abortTransactionTD{0，1}（m，pc）{1}(iv) 对所有的mσ∈P. 且pc ∈ PC则mσ。Increase（pc）=returnIncreaseTD{0，1}（mσ，pc）{0}请注意，由于程序只能通过抛出（未捕获的）异常或在初始入口点执行返回指令来终止因此，检查所有入口点的所有返回指令只能在没有事务活动时执行是足够的。更精确的替代方案R.R