Java字节码静态单赋值形式中抽象解释验证简化的有效集成方法

--理论计算机科学电子笔记131（2005）27-38www.elsevier.com/locate/entcs集成Java字节码验证Andreas Gal，Christian W.Probst，Michael Franz迈克尔·弗朗茨·普罗布斯特1加州大学信息与计算机科学学院Irvine，CA，92697，USA摘要现有的Java验证器执行迭代的数据流分析，以发现存储在堆栈或寄存器中的值的明确类型。我们的新验证算法使用抽象解释来获得程序中每个寄存器和堆栈位置的定义/使用信息，这反过来又用于将程序转换为静态单赋值形式。 在SSA中，核查简化为每个SSA变量的定义类型之间的简单类型兼容性检查 以及每种用途的类型。通过堆栈和寄存器的值的相邻转换不再显式验证。这种集成的方法比传统的字节码验证更有效，但仍然与严格验证一样安全，因为可以诱导整体程序正确性。一旦从每个定义流向所有相关用途的数据已知是类型安全的。保留字：抽象解释、验证、优化1介绍移动程序可能是恶意的。从不可信方或经由不可信网络连接接收此类移动程序的主机将需要1 电邮地址：gal，probst，uci.edu这项研究的部分资金来自美国国家科学基金会（NSF），德赠款TC-0209163和ITR-0205712和海军研究办公室（ONR）联合国-根据协议编号00014 -01-1-0854。美国政府被授权为政府目的复制和分发重印本，尽管上面有任何版权注释。 本文所含的观点和结论是作者的观点和结论，不应被解释为必然代表国家科学基金会、海军研究办公室或 美国任何其他机构政府的1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.02028A. Gal等人/理论计算机科学电子笔记131（2005）27保证移动代码不会造成任何损害。为此，Java虚拟机（JVM）开创了代码验证的概念，通过该概念，接收主机检查每个到达的移动程序，以排除潜在的恶意行为，甚至在开始执行之前。这种分析是必要的，因为JVM中临时变量的位置不是静态类型的。如果验证成功，则原始字节码将被转发到JVM的执行组件，该组件可以是解释器或即时编译器。具体而言，除了表示验证是否成功的结果之外，验证者计算的所有其他信息都将被丢弃，并且不会向前传递。在许多情况下，当即时编译器随后再次执行非常相似的数据流分析时，这会导致工作重复。在本文中，我们简要概述了一种替代验证机制，以避免这种重复工作。我们没有直接验证Java虚拟机语言（JVML）字节码，而是以这样一种方式对其进行注释，即指令之间的值的流变得显式，而不是通过操作数堆栈，然后将注释的字节码转换为静态单赋值（SSA）形式[3]。SSA中的验证程序大大减少了程序中必须进行类型检查的点的数量，因为只有值的生产者和消费者才被验证。通过堆栈和寄存器的值的相邻转换不再显式验证。这种集成方法比传统的字节码验证更有效，但仍然与严格验证一样安全，因为一旦从每个定义到所有相关用途的数据流已知是类型安全的，就可以诱导整体程序正确性。我们的基准测试表明，将JVML转换为SSA并在此表示中验证程序所需的总时间仍然小于直接在JVML上执行标准验证算法所需的时间。我们的方法不会对无需JIT编译就能解释的方法施加任何开销，因为基于SSA的验证总体上仍然比传统的验证器快。本文的其余部分组织如下：第2节简要概述了传统的Java字节码验证器，并介绍了基于SSA的验证。第3节将我们的方法的性能与Sun的标准验证器的性能进行了比较。第4节讨论了相关的工作，第5节包含我们的结论，并指出未来的工作。A. Gal等人/理论计算机科学电子笔记131（2005）2729- ≤ ≤instruction：：= core|数据流core：：= const n |lconst l |iadd |Ladd|伊费格湖|返回数据流：：= pop |DUP|双2 |iStore X|负载x |lstore x |lload xFig. 1. JVML S中的说明。 参数n、l、x和L必须满足条件1n5，l∈ {0，1}，x，L ∈ N.2静态单一分配表本节介绍了JVML的一个子集，简要描述了传统的Java字节码验证，并讨论了我们的方法中使用的抽象以及我们的新验证方法。2.1公司简介图1显示了JVMLS的语法，它是JVML的一个子集，我们在这里使用它来进行说明。我们将指令集分为核心指令和数据流指令.核心指令对存储在操作数栈上的值进行操作，而数据流指令仅通过操纵操作数栈的状态并在操作数栈和变量之间交换值来促进核心指令之间的值的数据流。值由核心指令产生，并可由其他核心指令消耗。在值的生存期内，它可以驻留在操作数堆栈上，也可以驻留在变量中，并且可以同时驻留在多个位置。数据流指令既不产生也不消耗值，它们只是在堆栈位置和变量之间传输22.2Java字节码验证JVML指令可以在两个位置读取和存储中间值：操作数堆栈和局部变量。这些位置是ad-hoc多态的，因为在程序执行期间，相同的堆栈位置或局部变量可以保存不同类型的值。验证确保这些位置被一致地使用，并且中间值总是使用它们最初写入的相同类型读回。验证也保证了控制流的安全性，但这是一项相对微不足道的任务。相反，验证数据流是否类型良好则相当复杂。JVM字节码验证器[12，25]使用迭代数据流分析和JVML指令的抽象解释器。与JVM不同，抽象解释器的堆栈单元和局部变量存储类型，而不是2即使它消耗一个值，pop指令也是一个数据流指令，因为它只是操纵堆栈，使得最顶部的值不再可以使用。30A. Gal等人/理论计算机科学电子笔记131（2005）27价值观从验证器的角度来看，JVM指令是对类型执行的操作。JVML验证工作在方法级别。通过共归纳的论证，如果每个方法都是可验证的，那么整个程序也是可验证的。在本文的其余部分，我们使用程序和方法互换。Java字节码验证器的主要职责是检查堆栈位置和局部变量是否以类型安全的方式使用。如果值的定义和使用具有兼容的类型，则会出现这种情况。为了确保这一点，验证器算法必须确定每个指令的所有堆栈位置和变量的类型。2.3抽象于JVML，价值的定义与其用途之间并无明显联系。然而，即使定义-使用链可用于JVML程序中的每个值，通过比较每个定义的类型及其用途来完成一次扫描。如果我们考虑如何对JVMLS的指令进行分类，其原因就变得更加明显。只有核心指令定义和使用值。数据流指令仅仅便于核心指令之间的数据流对于Core指令，任何消费操作数的预期类型和任何产生值的类型总是静态已知的。相反，数据流指令是多态的。一般来说，在不知道数据流指令的操作数类型的情况下，dup指令的结果类型，例如，取决于堆栈顶部的值的类型虽然局部变量访问指令（如iloadx）建议更强的静态类型，但这仅适用于标量类型。在JVM中，使用astore x和aload x写入和读取局部变量中的对象引用，并且仍然需要进行数据流分析以确定所访问变量的精确类型。我们的方法的基本原理是用寄存器文件替换堆栈和局部变量，并重新定义指令的动态语义以实际在这些寄存器上工作。这种替换允许我们将基于堆栈的代码转换为SSA，并仅在值的定义和实际使用之间执行类型检查。我们将程序中的每条指令抽象为一个元组，该元组由执行该指令之前的堆栈深度组成，从堆栈单元和局部变量到定义它们的指令的映射，指令读取和写入的堆栈单元和局部变量的集合，以及从堆栈单元到驻留在其中的值的映射。A. Gal等人/理论计算机科学电子笔记131（2005）2731这些组件的主要贡献是允许动态语义在寄存器文件上工作，并在验证之前将代码转换为SSA。2.4算法我们的方法的目标是避免预先迭代的数据流分析来验证JVML。相反，JVML代码被注释，使得核心指令之间的值的队列变得显式，而不是依赖于操作数堆栈。这使我们能够消除所有的数据流指令从代码后SSA建设。这些指令不再需要，因为它们只促进数据流，但实际上并不计算任何东西。一旦代码仅由核心指令组成并且是SSA形式，就可以通过将每个定义的类型与相应的使用直接关联来执行类型安全检查（定义-使用验证）。对于一个小的示例程序，注释步骤的结果如图2所示。在执行指令之前，每个指令都用当前堆栈深度进行注释 使用这些注释和JVMLS的动态语义，指令不再依赖堆栈将操作数连接到它们的定义。堆栈上的值相对于它们到堆栈底部的距离进行标记 由iconst指令产生的值例如，在先前为空的堆栈上执行，将被标记为0，因为它当前位于堆栈的底部。这种标记允许解析堆栈引用，而无需实际维护堆栈数据结构。例如，用sd=0注释的iconst指令总是写其结果是堆叠电池0。在未注释的JVML中，接收生成值的堆栈单元将取决于程序中该点处动态堆栈的状态。遵循JVML机器模型，我们将长整数分成两半。因此，对长整数进行操作的指令推送和弹出值对PC指令StackDepth堆叠Vars012345011lconst00LL2lconst12LLLL3iconst14LLLL 我4伊费格湖5LLLL5双24LLLLLL6Ladd6LLLL7L：拉德4LL8lstore02LL图二. 一个示例程序，以及堆栈和变量状态的抽象。 每个指令在执行该特定指令之前用堆栈深度标记。 L代表 LONG，L'代表LONG '，I代表INT.32A. Gal等人/理论计算机科学电子笔记131（2005）27在操作数堆栈上和从操作数堆栈中读取。相应地，对于长整数的每个定义，定义了两个值，一个用于下半部分（LONG类型），一个用于上半部分（LONG在注释阶段之后，我们的验证算法首先计算所有值定义的迭代优势边界（IDF）[20]，即写入堆栈单元或局部变量的值程序中的每个可达指令数据流指令既不产生也不消耗任何值，并通过复制传播消除。在转换为SSA和复制传播之后，我们可以执行实际的类型检查。与传统验证器执行的类型推断类似，φ节点的类型是φ节点引用的每个定义（φ操作数）的公共超类型，而常规核心指令总是定义具有不同类型的值。 这些可以与它们各自的用途相匹配，在线性时间内对程序进行一次扫描类型检查是惰性执行的，在这个意义上，只有最小数量的指令被检查，以确保整体类型安全，而对于数据流指令，只有适当的数据流得到保证。仅考虑动态语义，验证的数据流显然等同于解释原始JVML程序所产生的数据流。然而，由于数据流指令已经被消除，由其静态语义强制执行的一些限制不再适用。例如，下面的JVML程序将被Java验证器拒绝，但它是有效的在我们基于SSA的方言中：1：lconst02：iStore13：负载14：lstore2在这个例子中，在第1行中，一个长整数作为一对半整数（LONG，LONGJ）被压入堆栈。将长整数部分存储在整数寄存器中（第2行）会被传统的验证器拒绝。相反，由于我们的验证器不考虑数据流指令的类型规则，它接受这个代码片段，因为在第1行中推入的（LONG，LONGJ）对在第4行中使用之前在堆栈上恢复值得注意的是，这个程序虽然被JVM拒绝，但在执行时是完全安全由于篇幅限制，我们无法详细说明如何验证异常，数组和对象初始化，而是参考我们的技术报告[7]。A. Gal等人/理论计算机科学电子笔记131（2005）27333基准为了评估我们的基于SSA的验证器的性能，我们已经实现了一个原型验证器的基础上本文提出的算法。我们的原型在验证之前内联子程序。为了与Java的标准验证器进行公平的比较我们的理由是，Java中的子例程结构已经过时，可能会在Java虚拟机的未来版本中被删除。此外，我们目前的算法依赖于这样一个事实，即控制流程图可以从JVML代码中快速恢复。在存在子例程的情况下，情况并非总是如此，因为从子例程返回的边不是显式的。作为比较基准，我们将基于SSA的验证器的总运行时间与Sun基于DFA的验证器的运行时间进行比较。在这两种情况下， 我们使用作为Sun KVM [ 24 ]一部分的预验证工具这两个验证器都是用C实现的，使用相同的底层框架来读取和Java类文件。为了消除任何缓存效应并补偿定时错误，两个验证器都对测试集中的每个方法运行100次。现时并无既定基准以测试审核员之表现。SPECjvm [19]等基准测试套件旨在评估代码执行的性能，而不是代码验证。因此，我们决定使用Java类库（JDK 1.4.2）的各个部分作为测试集 。 图 3 列 出 了 所用 类 的 一 些 特征 。 所有 的 测 试 都 是在 Pentium 42.53GHz CPU和512MB RAM上进行的，运行在RedHat Linux 9下。图4比较了传统的基于DFA的验证器和我们的基于SSA的验证器的总运行时间。在比较总运行时间时，SSA形式的验证比传统算法快约15%。不考虑计算支配者关系和支配边界所花费的时间，基于SSA的验证大约快45%。总数量方法方法大小堆栈深度当地变量øMaxøMaxøMaxjava/*649041.3640652.74142.4737java/io121338.1212952.3982.3515java/lang133638.4140652.32102.1737java/math40572.6730413.1683.7329爪哇209626.804173.05112.3115java/util235949.2129162.64142.6225图三. 用于比较基于SSA的验证器运行时的测试集的特征与传统验证器的运行时间相同34A. Gal等人/理论计算机科学电子笔记131（2005）27在基于SSA的验证的情况下，必须进行类型检查的指令数量比传统的验证器大约少38%。唯一值得注意的例外是java/math，它实际上需要稍微多一点的指令来进行SSA形式的类型检查。这是由我们对LONG和DOUBLE类型的处理造成的，我们将其分为两部分，而传统的验证器可以在一个步骤中处理它们见图4。比较传统的基于DFA的验证器和我们的基于SSA的验证器的总运行时间和必须进行类型检查的指令数量。1614121086420java/java/iojava/langjava/math爪哇java/util验证（DFA）验证（SSA，总计）DomDF检查180160140120100806040200java/java/iojava/langjava/math爪哇java/util验证（DFA）验证（SSA）[秒][type支票（千）]A. Gal等人/理论计算机科学电子笔记131（2005）27354相关工作除了对JVM的非正式描述[12]之外，还提出了JVML及其验证器的一些正式规范[6，11，21]。 在这种情况下，子程序是特别感兴趣的，并且已经为它们提出了几种类型系统[15，16，22]。所有这些方法都有一个共同点，它们依赖于某种形式的迭代数据流分析[11，17]来决定类型安全。证明携带代码（PCC）[14]通过减轻代码消费者验证代码的负担来解决这个问题。相反，代码生产者计算并证明验证条件。代码使用者重新计算验证条件，并检查附加的证明是否有效。PCC甚至可以用来证明机器码的安全性。相比之下，基于SSA的验证仅限于移动代码格式（如Java），但其优点是它只需要实际代码作为输入，而不需要其他信息（如证明）。分裂验证器方法[23]基于轻量级字节码验证[18]的思想，将PCC思想应用于Java字节码。Preverifier用JVM在类加载期间执行的数据流分析的固定点来注释JVML。对于带注释的类文件，验证被简化为确认注释确实是一个有效的固定点。就像Necula的PCC一样，注释扩大了类文件的整体大小，而我们的方法不依赖于任何额外的注释。与拆分验证器类似，Java智能卡验证器[10]通过并行字节码转换减轻了验证器的负担预处理器工具确保Java堆栈在每个分支指令之后为空，并且所有寄存器都是单类型的。与我们的方法相反，Java智能卡验证器对于没有以这种方式处理的Java类文件失败。固有安全的移动代码表示格式（如SafeTSA [1]）消除了验证的需要，因为移动代码以自一致的格式存储，只能表示格式良好和类型良好的程序。就像PCC一样，这种格式比基于SSA的验证具有系统优势，但需要放弃现有的Java类文件格式，这并不总是可以接受的。我们的方法和SafeTSA有一个共同点，它们都以SSA形式向JIT提供代码，用于加速代码生成。基于SSA的表示已被用于几种方法来编译字节码。Marmot [4]是一个研究高级编程语言实现的研究平台。我们的主要区别是36A. Gal等人/理论计算机科学电子笔记131（2005）27Marmot只接受可验证的程序。输入程序的这个属性允许对代码的属性做出某些假设例如，关于局部变量和堆栈条目的类型。与我们的工作类似，Marmot内联子例程以避免复杂的编码，作为正常的控制流，类似于Freund [5]。正如Kelsey和Appel所观察到的[2，8]，SSA形式和函数式编程之间有着密切的关系。因此，League et al. [9]的工作与我们的工作直接相关。λJVM是Java字节码的函数表示，它使数据流显式化，就像我们的工作一样。他们还将验证分为两个阶段，一个是在构建λJVM代码期间，另一个是稍后的简单类型检查。然而，它们最初执行常规的数据流分析，以推断每个程序点处的堆栈和局部变量的类型。这与我们的方法相反，将验证分为两个阶段的原因正是为了避免初始数据流分析。5结论和今后的工作现有JVML验证器执行大量数据流分析，但不会将此分析结果保留以供后续代码生成和优化阶段使用。我们提出了一种替代验证器，不仅比标准的Java验证器更快，但它额外计算了支配树，并将程序带入静态单一分配形式。因此，相应的计算不需要在动态编译流水线的由于我们的算法比传统的Java字节码验证具有更低的在可验证移动代码的更大背景下，我们的研究结果表明，验证不应该孤立地“预先”实践，而是与客户端移动代码管道的其余部分集成。因此，我们希望我们的方法可以应用于JVM之外的其他移动代码系统，例如Microsoft我们的工作也与所有已经在内部使用SSA进行代码优化的现有JVM实现相关。如果一个VM已经有了将代码转换为SSA的方法，那么拥有一个“预先”的基于数据流的验证器就是多余的。我们已经证明了延迟类型检查并首先将程序转换为SSA是可能的。事实上，我们的算法是第一个将Java代码安全地转换为SSA的方法，而无需任何先前的数据流分析和验证。在将来，我们计划研究如何支持子例程A. Gal等人/理论计算机科学电子笔记131（2005）2737in our framework框架.虽然子例程正在迅速从JVML中消失，但从学术角度来看，它们仍然很有趣。他们加强了一个问题是否以及如何基于SSA的表示可以获得多态代码，其中不是所有的控制流边缘是明确的。我们也有兴趣探索JVML代码的结构化SSA注释。为此，JVML代码以这样一种方式重新排列，即基于特定结构感知的SSA验证器可以推断代码的最终SSA形式，而无需实际计算支配树和迭代支配边界。由于代码仍然是用纯JVML表示的，因此它与现有VM完全向后兼容，并且不需要任何额外的注释。虽然重新排列的代码可能不如其原始形式紧凑，但该方案将进一步减少所需的验证时间。引用[1] Amme，W.，N. Dalton，J. von Ronne和M. Franz，SafeTSA：A Type Safe and RepersonalSecure Mobile-Code Representation Based on Static Single Assignment Form，in：Proceedingsof the ACM SIGPLAN137[2] Appel，A. W.， SSA是函数式编程，ACM SIGPLAN Notices33（1998），pp.17-20.[3] 塞隆河，J. Ferrante，B. K.罗森，M。N. Wegman和F. K. Zadeck，Eccently Computing StaticSingle Assignment Form and the Control Dependence Graph ， ACM Transactions onProgramming Languages and Systems，1991，pp.451-490[4] 菲 茨 杰 拉 德 ， R. T. B. Knoblock ， E. 鲁 夫 湾 Steensgaard 和 D. Tarditi ， Marmot ： AnOptimizing Compiler for Java，Software-Practice and Experience30（2000），pp. 199-232.[5] Freund，S. N.，Java字节码子程序的成本和好处，在：OOPSLA的Java研讨会正式基础会议记录，1998年。[6] Freund，S. N.和J. C. Mitchell，A Formal Specification of the Java Bytecode Language andBytecode Verifier，in：Proceeings of the 1999 ACM SIGPLAN Conference on Object-OrientedProgramming，Systems，Languages Applications（OOPSLA147比166[7] Gal，A.，C. W. Probst和M. Franz，Proofng：Eccient SSA-based Java Verification，TechnicalReport 04-10，University of California，Irvine，School of Information and Computer Science（2004）.[8] 凯 尔 西 河 一 、 A correspondence between continuation passing style and static singleassignment form，ACM SIGPLAN Notices30（1995），pp.13比22[9] League，C.，V.Trifonov和Z. 邵，功能Java字节码，在：第五届世界系统学、控制论和信息学会议论文集，2001，Java虚拟机的中间表示工程研讨会。[10]Leroy，X.， Java智能卡上的字节码验证，软件实践和经验32（2002），pp. 319-340[11] Leroy ， X. ， Java Bytecode Verification ： Algorithms and Formalizations ， Journal ofAutomated Reasoning30（2003）. 235-269。[12] Lindholm，T.和F. Yellin，38A. Gal等人/理论计算机科学电子笔记131（2005）27[13] 微软合作，微软. NET。http：//www. Microsoft. com/net/.[14] Necula、G. C.的方法，Proof-Carrying Code，in：Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages（POPL），Paris，France，1997，pp. 106- 119[15] 奥卡拉汉河Java字节码子例程的简单、全面的类型系统，在：第26届ACM SIGPLAN编程语言原理研讨会（POPL）会议记录，圣安东尼奥，德克萨斯州，1999年，第100页。70比78[16] 钱志，A Formal Specification of Java Virtual Machine Instructions for Objects，Methods andSubrountines，in：Formal Structures and Semantics of Java，1999. 271-312.[17] 钱志，Java字节码验证的标准固定点迭代，ACM编程语言和系统交易22（2000），pp。638-672.[18] 罗 斯 ， E. 和 K. H. Rose ， Lightweight Bytecode Verification ， 1998 年 ， 《 OOPSLA-Workshop on the Formal Underpinnings of the Java Paradigm》[19] SPEC，JVM98基准测试。 http://www.spec.org/jvm98（2001年）。[20] Sreedhar ， V.C. 和 G.R. Gao ， A Linear Time Algorithm for Placingφ-nodes ， in ：Proceedingsofthe22ndACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgramming Languages（POPL），San Francisco，California，1995，pp.62比73[21] 施塔克河，J.S chmid和E. Büorger，“ J a v a 和 J a v a 虚 拟 机 ： 定 义 、 验 证 和确 认 ” ， S p r i n g e r - V e r l a g ， 2 0 0 1 年 。[22] 斯塔塔河和M. Abadi，A Type System for Java Bytecode Subroutines，ACM Transactions onProgramming Languages and Systems21（1999）.90比137[23] SunMicrosystems ， JSR-000139 连 接 有 限 设 备 配 置 1.1 。 http ： //www. jcp 。org/en/jsr/detail？id= 139。[24] Sun Microsystems，“KVM -千字节虚拟机白皮书”。美国加利福尼亚州帕洛阿尔托，1999年。[25] Yellin，F.，Java中的低级安全性，369-380.