基于区域的Java字节码验证器：内存安全执行和管理

理论计算机科学电子笔记141（2005）183-201www.elsevier.com/locate/entcs一个带区域标注的Java字节码验证器Sigmund Cherem和Radu Rugina{siggi，rugina}@ cs.cornell.edu计算机科学系康奈尔大学Ithaca，NY14853摘要本文提出了一种扩展Java字节码的内存安全执行验证器，支持基于区域的内存管理和显式释放原语。验证器读取带区域注释的字节码，这些字节码通过创建和删除内存区域、在区域中分配对象以及将区域作为参数传递的指令来增强标准Java字节码。验证确保当区域中的对象正在使用时，每个区域都是活动的，并且程序不会遵循悬挂引用。验证器要求与字节码一起提供区域安全证书。验证过程包括方法体的加载时验证和方法调用的延迟链接验证。我们的区域系统支持非词法作用域的区域和dangling指针;本文提出的验证器可以成功地处理这两个特性。 我们的实验表明，证书的大小在实践中是可以接受的，并且区域验证很少产生运行时开销。关键词：字节码验证，基于区域的内存管理1介绍具有基于区域的存储器管理的系统将对象一起分组在区域中，然后一次解除分配区域中的所有对象。区域有许多吸引人的属性，包括数据局部性和高效的集体释放。更重要的是，编译器可以静态地启用基于区域的内存管理：它可以自动确定如何将对象分组在区域中以及何时释放区域。这种方法对于实时系统特别有吸引力，因为实时系统不能被垃圾收集器中断无限长的时间1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.030184S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183在最近的工作中，我们提出了Jreg，一个Java程序的区域分析和转换系统[6]，它可以将输入Java程序转换为基于区域的内存管理的输出程序在我们的系统中，区域没有词法作用域，所以它们可以在控制流中的任何一点被创建或删除。此外，我们允许悬挂指针，但要求程序永远不会遵循这样的引用。这两个特性都提高了我们系统的准确性和可扩展性，但对于编译器来说，识别区域生存期以及验证器检查它们更具挑战性在我们的系统中的区域转换是一个字节码级别的transformation和灰，并产生区域注释的字节码。生成的字节码在扩展的虚拟机中执行，具有对区域的运行时支持。但是，没有运行时检查来确保当程序访问这些区域中的对象因此，如果程序在某个区域中的对象仍在使用时错误地释放该区域，则会导致系统崩溃。在本文中，我们提出了一个验证区域注释字节码。验证器的目标是确保当程序访问这些区域中的对象时，这些区域都是活的，并且程序永远不会跟踪悬挂指针。这样的验证器可以用来检查我们的区域转换的结果是安全的。由于我们的编译器中的分析和转换算法相当复杂，它们的实现容易出错;事实上，这里提出的区域验证器已经指出了我们编译器中的实现错误。此外，验证器还可以检查其他系统生成的区域注释字节码的正确性。本文中提出的验证过程仅旨在验证区域操作;所有其他字节码级别的检查都由标准字节码验证器执行。我们提出了一个数据流验证算法，检查程序中每个方法的区域为了验证程序中的方法，验证器要求与字节码一起提供区域证书。这些证书中的信息描述了各种方法效果，包括区域别名和区域访问;从携带证明的代码的角度来看[17]，该区域信息可以被视为转换正确的我们还提出了一个虚拟方法调用的惰性链接验证算法，以确保方法调用可以安全地每个方法调用仅在第一次执行时检查。与本文提出的方法相反，大多数现有的基于区域的系统[20，8，12，4，7]使用类型系统来确保1我们使用区域创建和移除这两个术语，而不是分配和释放，以避免对象分配和区域分配之间的歧义。S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183185区域操作。然而，基于数据流分析的方法在我们的系统中更合适，原因有两个。首先，我们的系统使用的区域不是词法范围，并允许悬空引用。因此，不可能使用程序的语法结构来确定区域生存期。第二，我们在字节码级别上操作，其中局部变量是无类型的，并且可能在不同的点上保存不同类型的值;同样，需要进行据我们所知，这是在字节码级别检查基于区域的程序正确性的第一种方法。本文其余部分的结构如下。第2节介绍了Jreg系统的概述。第3节给出了一个带有区域注释的示例程序，第4节介绍了我们系统中的区域字节码。第5节详细介绍了验证过程。第6节讨论了实验结果。最后，我们在第7节讨论相关工作，并在第8节总结。2Jreg：一个基于区域的Java系统Jreg系统是一个分析和转换系统，为Java程序提供基于区域的内存管理[6]。它由一个区域编译器和一个具有区域运行时支持的虚拟机组成。区域编译器在Soot基础设施中实现为字节码级转换：给定输入程序，编译器自动生成具有区域构造的输出程序。转换后的程序显式地创建新区域，将对象放置在区域中，将区域作为参数传递，并显式地删除区域。这些分析是在Soot中的三地址代码中间表示中实现的。由区域编译器产生的区域注释的字节码然后在支持区域注释的字节码并提供区域运行时存储器管理的扩展虚拟机中执行。区域虚拟机构建在开源Ka e VM的解释器之上[22]。区域编译器分三步执行转换。首先，它使用一个对数据流不敏感但对上下文敏感的指向分析来为每种方法生成一个区域指向图。图中的节点表示区域，边表示点到关系。 第二，系统使用一个低敏感区域活性分析，以确定区域的生存期。最后，它使用计算出的点到图和区域生存期来在程序中放置区域注释。转换的目标是确保每当程序访问对象时，包含该对象的区域是活动的;同时，静态地最小化区域的生存期。186S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183该系统还使用了对异常和多线程的运行时支持当一个区域中的对象被多个线程并发访问时，每个线程在不再需要该区域时删除该区域。运行时系统使用共享区域的线程计数器来确保只有最后一个线程实际删除该区域。最后，当抛出异常时，异常运行时系统确保在它沿程序堆栈向上走的过程中删除局部区域。3例如我们举例说明了我们的系统支持的基于区域的程序。图1显示了由我们的区域编译器生成的区域注释程序;输入程序是相同的，但没有区域注释。验证器的目标是成功地检查这个程序的执行是内存安全的。为了可读性，我们显示程序的Java版本，而不是字节码。这个程序操作链表：方法make迭代地构造一个链表对象的列表;方法reverses循环地反转一个列表;方法test调用这些方法来执行一个简单的列表计算。region注释是不言自明的：create动态地创建一个或多个region，remove动态地删除regions;对象分配上的子句因此，每个方法都接收两种参数：标准Java参数和区域参数。方法make有两个区域参数r1和r2。该方法期望这些区域由其调用者创建;当调用时，make将把新列表放置在这些区域中：r1将保存列表的主干，r2将保存表示列表数据的整数对象方法reverse递归地反转接收器对象中的列表。反向列表是一个新列表，但具有与原始列表相同的数据对象。此方法接收区域r3作为参数，并将反向列表的脊放置在此区域中。在方法体中，区域r3在递归调用时作为实际参数传递虽然reversal方法访问原始列表中的对象，但不需要传递保存该列表的区域以进行reverse，因为reverse并不显式引用此区域。最后，方法test调用make来创建一个包含10个元素的列表，反转该列表，并打印反转后的列表的内容。该方法创建区域r6（用于列表主干）和r7（用于列表元素），将它们传递给make，并将结果放在x中然后，程序为S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183187reversed list，将其传递给reverse，并将结果存储在y中。在调用reverse之后，区域r6中的旧列表x的脊不再需要并且可以被丢弃。在打印结果之后，区域r8和r7也可以被回收。请注意，区域r6和r8是部分重叠的，我们可以准确地描述它们的生存期，因为区域没有词法作用域。class List{ Object data;List next;static List make r1，r2>（intn）{ Listt，y = null;public void run（）{newList（）;t.data= r2中的新值; t.next=y;y =t;}返回y;}public void run（）{Listt= r3中的new List（）;t.data= data;if（next==null）t.next=null;其他t.next= next.reverse r3>（）; returnt;}voidtest（）{create r6;List x = make r6，r7>（10）;create r8;Listy = x.reverse r8>（）;remove r6;对于（;y！= System.out.println（y.data）;y.next删除r7，r8;}}Fig. 1. 示例：基于区域的列表操作方法使反向测试指向关系(r1，下一个，r1）(r1，data，r2）(r3，下一个，r3）(r3，data，r5）(r4，下一个，r4）(r4，data，r5）(r6，下一个，r6）(r6，data，r8）(r7，下一个，r7）(r7，data，r8）局部区域传入区域参数区域标准参数的{}{r1，r2}{r1，r2}{r1}{r1，r2}{}{r3，r4，r5}{r3}{r3，r4}{r3，r4}{r6、r7、r8}{}{}{}{}图二、示例中方法的区域信息图2中的表显示了区域编译器用来生成此程序的关键信息。该信息也是验证过程中的关键，代表了必须与字节码一起提供的区域证书中的大部分信息。它包括区域指向信息和关于不同类别的区域的信息的188S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183指向信息使用（R，F，RJ）形式的三元组来描述区域之间的混叠关系，所述三元组指示区域R中的任何对象的场F引用区域RJ中的对象。 指向关系在整个方法中保持不变（因为它们是以一种不依赖于带宽的方式计算的），并描述了执行方法的别名效应。验证者并不假设证书的正确性，而是检查所提供信息的有效性。每个方法的区域包括但不限于在该方法的变换代码中出现的区域。例如，只有r3出现在reverse代码中;然而，该方法的区域信息还涉及其他两个区域r4和r5。每个方法的区域分为两类：1）本地区域，在方法中创建的区域; 2）传入区域，由当前方法的调用者创建的区域。例如，make和reverse中的所有区域都是传入区域，而test中的所有区域都是本地区域。传入区域包括以下三个子类别：• 参数区域。这些是在代码中作为参数传递的区域例如，r1和r2在make中，或r3在reverse中。传递这些区域是因为被调用方将在这些区域中分配新对象，并且在分配站点需要其他区域（例如r4）不需要传递，即使被调用者可以访问其中的对象。• 标准参数的区域。这些是放置标准方法参数的区域标准参数包括接收方对象this和返回值。简而言之，我们将标准参数的区域称为参数区域，并将它们与上述参数区域区分开来。在我们的例子中，reverse的参数请注意，传入的区域正好是从指向图中的参数区域可到达的区域• 使用区域。这些是方法（及其调用的方法）访问或放置对象的区域。因此它是参数区域的超集;它通常也是实参区域的超集，除非在方法中不使用生成的代码仅引用局部区域和参数区域。尽管剩余的传入区域S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）1831894扩展区域字节码在我们的系统中，除了标准的局部变量和操作数堆栈外，每个帧还包含两个额外的组件来处理区域操作：• 一组局部区域变量。这些是使用区域索引值从0开始标识的区域变量保存对区域句柄的引用。• 一个单独的区域堆栈，用于将区域作为参数传递给调用。因此，我们将区域变量和区域参数与标准变量和参数分开。这使我们能够在现有字节码系统之上以一种干净的方式构建扩展，而不会干扰底层标准字节码的结构。这种分离有两个好处。首先，我们可以使用标准验证器来执行标准安全检查;并使用我们的验证器来检查区域扩展。其次，区域注释程序可以在标准VM上以最小的变化执行-我们的系统使用以下8个区域字节码指令：• createri：分配一个新的区域句柄，并将其存储在索引ri处的局部区域变量中。变量在此语句之前不得引用有效的区域句柄（即，不允许多次创建区域• removeri：释放位于索引ri推荐信 变量必须引用有效的局部区域句柄。• newregci ri、anewarrayregci ri、newwarrayregtyp ri、multianewarrayregci dimri：将对象或数组分配到由索引ri处的region局部变量指示的区域中。这里ci是类索引，typ是一个常量，表示一个基本类型，dim是数组维数。当分配指令执行时，我们要求索引ri• pushregri：将存储在索引ri处的region变量中的引用推送到region堆栈上。当执行这样的指令时，索引ri5验证过程验证过程包括加载时验证阶段和链接验证阶段。每种方法的验证都需要一个区域安全证书，其中包含该方法的区域影响的信息（包括其指向图，其访问区域和其他信息）。190S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183此信息必须与字节码一起提供，并且必须在验证期间可用。加载时验证发生在加载新类时，由检查每个方法主体的数据流分析组成。验证仅在过程内执行，方法调用被忽略。但是，加载时验证检查类层次结构中被重写方法的区域影响的一致性。当方法被调用时，链接验证会动态地检查方法调用。目标是确保呼叫者和被呼叫者之间区域响应的一致性。验证只在第一次调用方法时进行;之后，调用站点被标记为已成功检查，并且在该站点上的子调用不会引起验证开销。5.1地区安全性证书我们的系统要求证明区域操作安全性的证书可用于每种方法，并与字节码一起提供（作为类文件中的属性）。这些信息是由我们的区域编译器作为转换过程的一部分自动生成的。让我们用Rm表示方法m的所有区域的集合，用Im表示m的传入区域。对于每个方法m，类文件将包括以下信息：• 该区域指向信息Gm<$Rm×F×Rm，其中F是字段名称的集合。每个元素（r，f，rJ）∈Gm表明，在m的整个执行过程中，r中每个对象的字段f引用rJ中的一个对象。该信息捕获方法m的区域混叠效应。• 对于方法体中的每个调用点，返回值在该调用点的区域（仅当返回值是引用时）。我们将这些信息表示为映射cm：Cm→Rm，其中Cm是m中的调用点的集合。• 论元区域的有序集合Am∈Im这些是m的标准参数（包括接收器和返回参数）的区域。• 传入区域Im的有序集合。• 传递给方法m的参数区域的有序集合Pm∈Im。• 由m使用（访问）的区域的集合Um=m。核查员并不认为证书的正确性是理所当然的。特别是，它不依赖于点到图是正确的。相反，当提供的信息不正确时，验证失败S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）1831915.2加载时间验证当一个新的类被加载时，验证器对每个方法执行数据流分析。核查员将：a）在操作数栈上确定局部变量和引用的区域; b）跟踪活动区域; c）检查字段访问总是发生在活动区域中，并且与封闭方法的声明的使用区域集一致。为了使分析形式化，我们假设每个方法都表示为控制流图，其节点是以下指令之一i∈ Instri：：= loade|店鄂|推P|op|调用我|返回|新闻注册|pushreg r|创建r|删除re∈ Expre：：= x |x.fp ∈ Primp：：= n|真正|虚假|null其中x∈Var是局部变量，f∈F是字段名，r是区域变量（如果m是当前方法，则r∈Rm），p是原始值（整数常数n，布尔值和null）。加载和存储在操作数堆栈顶部和局部变量或字段。压入指令将基元值压入堆栈。 操作op弹出顶部的前两个值执行操作（例如，算术、逻辑或比较），并将结果放回操作数堆栈;操作数必须都是引用或都是原始值，并且结果始终是原始值。方法调用从操作数堆栈弹出它们的参数，从区域堆栈弹出所有区域，并将它们的结果放回操作数堆栈。Return语句从操作数栈弹出方法的结果（如果有的话）。动态分配newregr创建一个新对象并将其放置在region中R.指令pushregr将区域r压入区域堆栈。最后，创建和remove具有前面部分中讨论的行为分析使用区域堆栈对操作数堆栈上的对象区域进行建模，定义如下：S：：=|S：r|S：T|S：其中，T指示空引用，T指示非空基元值或分析无法确定精确区域的引用。区域堆栈与此类似，但不包含“T”值。数据流信息是一个元组（So，Sr，V，L），其中So对操作数堆栈中的区域建模，Sr对区域堆栈上的区域建模，V：Var→Rm{T，}将变量映射到它们的区域T或;LRm是活动区域的集合。 我们假设第5.1节中提供的所有信息在分析期间可用。 如果当前分析的方法是m，192S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183用于加载、存储、推送和操作的传递函数如下：[[loadx]]（So，Sr，V，L）=（So：V（x），Sr，V，L）[[loadx.f]]（So，Sr，V，L）=（So：v，Sr，V，L），如果V（x）=rJ∈L<$rJ∈Um<$$>（v=T <$（v=r<$（rJ，f，r）∈Gm））[[storex]]（SO：v，Sr，V，L）=（SO，Sr，V[x<$→v]，L）[[storex.f]]（So：v，Sr，V，L）=（So，Sr，V，L），若V（x）=rJ∈L<$rJ∈Um<$$>（v∈ {T，<$}<$（v=r<$（rJ，f，r）∈Gm））⎧如果p/=null，则n（So：T，Sr，V，L）[[pushp]]（So，Sr，V，L）=n（So：n，Sr，V，L）如果p= null[[op]]（So：v1：v2，Sr，V，L）=（So：T，Sr，V，L）如果现场访问loadx.f和storex.f的传递函数中的边条件不满足，则验证失败。这些指令要求访问的区域是在一个已知的区域中，该区域是活的，在用于该方法的被访问的区域的集合中，并且被访问的区域的该区域是活的。场在区域图中找到（除非场有一个原始值）。上面的其他四个指令不需要检查，并且总是成功。特别是，允许loadx和storex操作悬挂引用，只要程序随后不使用这些引用访问它们的目标对象。当分析到达一个调用点cs时，它调用了一个带有k个标准参数和j个区域参数的方法m，它只是弹出这些参数，并在这个调用点推送返回值的区域，在cm中可用：[[invokem]]（So：vk：. ：v1，rj：.. ：r1，V，L）=（So：cm（cs），m，V，L）被调用方法的验证被推迟，直到程序的执行调用了这个方法。分析保存有序集Acs={cm（cs），v1，..， vk}的实际参数区域（包括返回值），有序集Pcs={r1，.，rj}的实际参数区域，以及该位置处的活动集合L。最后，返回指令是流程图中的退出节点，因此它们没有传递函数。然而，验证器检查返回值是否存储在Am的返回区域S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183193中。194S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183区域指令的传递函数如下：[[newregr]]（So，Sr，V，L）=（So：r，Sr，V，L），如果r∈L<$r∈Um<$（r∈Im <$r∈Pm）[[pushregr]]（So，Sr，V，L）=（So，Sr：r，V，L），if（r∈Im<$r∈Pm）[[remover]]（So，，V，L）=（So，，V，L− {r}），ifr∈L<$r/∈Im[[creater]]（So，，V，L）=（Soar，，V ar，L<${r}），ifr/∈L<$r/∈Im⎧（Sa r）：Tifreach（rJ，r）其中（S：rJ）ar=（Sa r）：rJ否则⎧如果V（x）=rJ，并且达到（rJ，r），则为（V a r）（x）=V（x）否则reach（rJ，r）惠rJ= r（rJ，f . （RJ，f，RJJ）∈Gmreach（RJJ，r）动态分配newreg检查分配区域是否处于活动状态。它还检查在该指令中指定的区域r是否不是本地重定向。gion（r∈Im），则必须将其作为参数传递给当前方法（r∈Pm）.对pushreg进行类似的检查。然而，当用pushreg传递一个区域时，分析并不检查pushreg是否被传递。gion是活动的;相反，系统将此检查推迟到以后的链接验证期间创建和删除的传递函数禁止连续的区域创建操作，或连续的删除操作;并限制区域创建和删除仅本地区域。因此，传入区域不能在被调用者中删除这种选择简化了验证（可以放宽这一条件，但分析和证明必须扩展有关每个方法可能删除的区域的信息最后，create和remove需要region堆栈Sr为空，因为region参数预计在方法调用之前被压入，而不会在其间创建或移除region。creater的规则更复杂，因为它必须特别注意以下无效程序：creater;x.f=newCinr;remover;creater; x.f.g= 1;在这个例子中，有两个动态区域具有相同的名称r。移除后，fieldx.f会持有一个对“旧”区域r的悬空引用。第二次创建不能将其转换为有效的引用。验证者通过将So和V中可以达到的每个区域设置为T，S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183195R通过零个或多个场访问新创建的区域R。这是使用滤波操作a完成的。为了完成数据流分析，我们定义了合并操作，该合并操作将数据流信息控制-数据流连接点相结合。两个人的合并元组（So，Sr，V，L）H（SJ，SJ，VJ，LJ）是逐点的，并产生（SoHSJ，SrH奥罗SJ，VHVJ，LHLJ）。 为了连接两个操作数栈SoHSJ，我们要求罗日堆栈具有相同的大小。 然后，连接是按分量的：（S：v）H（S：v）vJ）=（S H SJ）：（v H vJ）和这里，值的合并对应于区域s的一个顶点格 ：rHr=r，rHrJ=T，如果r=/rJ，则 r Hv=vH t=v，并且THv = vHT =T。请注意，该格的高度为2，而标准字节码验证的格可以具有任意高度，这取决于类层次结构。 因此，我们的数据流验证将收敛得更快 对于区域堆栈，我们要求Sr=SJ=，即，区域堆栈在连接点处必须为空变量映射的合并也是逐点的：VHVJ=VJJ，其中VJJ（x）=V（x）HVJ（x）。最后，我们要求活集合在连接点处相等：LJ=L;否则，验证器产生错误。该分析将方法开始时的数据流信息映射为（m，m，Vm，Um），其中Vm将m的每个形式参考参数映射到其在Am中的相应区域，并将所有其他变量映射到T。最后，当前方法（Um）使用的所有区域必须在方法入口。除了本节介绍的数据流分析之外，加载时验证还检查类层次结构中虚方法的区域一致性。由于这种验证使用的技术与链接验证中使用的技术相似，我们将其描述推迟到5.4节。5.3链接验证链接验证的目的是检查被调用的方法是否违反了在调用者中对其区域效应所做的假设。系统延迟检查方法：每个调用站点仅在执行第一次到达它时才被验证验证方法调用的关键部分是在传入的被调用方区域和调用方区域之间建立对应。考虑方法m中调用方法n的调用站点。验证器然后使用工作列表构造从n的区域到m的区域的映射α算法该算法从自变量区域An={r0，.，rk}和实际区域Acs={v0，.，vk}在调用者m的加载时验证期间记录。 An和Acs的大小必须匹配，196S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183M否则验证失败。此外，对于n的每个参考参数，Acs中的相应值必须是区域或区域;如果它是T，验证失败。为简单起见，假设v0，..，vk是所有区域，它们包括返回值的区域。算法如下：MAPPINGAL租M（）1令{r0，..，rk}= An2令{v0，..， vk}= Acs3对于i= 0 tok，doα（ri）=vi4W=An5while（W不为空）6从W中减去r1m7对于每个域f，使得（r1m，f，r2m）∈Gm8如果α（r2m）没有定义，9则若（α（r1m），f，r2n）∈Gn10则α（r2m）=r2n11W =W{r2m}12否则验证器错误13其他若（α（r1m），f，α（r2m））/∈ Gn14则验证器错误该算法通过匹配An和Acs中对应的区域来映射α;然后，它使用工作列表方法从这些集合开始遍历区域图Gn和Gm，构建映射，并检查被调用者信息Gn是否保守地一旦映射成功构造，（r，f，RJ）∈Gn意味着（α（r），f，α（RJ））∈G，它描述了嵌入的概念。在第3节的示例中，调用方法试验中的反向为：α（r3）= r8，α（r4）= r6，α（r5）= r7。一旦构造了映射α，验证者检查以下内容：• (P1)被调用方使用的传入区域对应于调用站点处的活动区域：{α（r）|r∈Un}<$Lcs;• (P2)被调用方使用的传入区域对应于调用方中使用的区域：{α（r）|r∈Un}<$Im<$Um;• (P3)调用者Pn={p1，.， pj}匹配在调用点Pcs={r1，.， rj}：α（pi）=ri，其中i = 1. J.如果所有这些检查都已成功验证，则可以安全地调用方法并执行调用。S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）1831975.4方法覆盖验证只有当方法调用不是动态分派时，上面描述的链接验证才能保证内存安全。为了确保在虚方法调用存在的情况下安全执行，验证器必须确保每个方法的区域效应包含覆盖它的所有方法的区域效应。这种方法重写检查发生在加载时，工作方式如下。每当一个新的方法m被加载时，验证器在类层次结构中寻找m立即覆盖的方法mJ如果存在这样的方法，验证者检查mJ的区域信息是否近似于m的区域信息。验证基本上包括制造一个从mJ到m的伪调用，它将mJ的形式参数作为实际参数传递给调用站点，并以与5.3节中描述的类似方式分析这个伪调用。该算法将在m的区域和覆盖方法mJ的区域之间构建映射。在伪调用位置的实际实参区域和实际参数区域正是调用方方法mJ的形式实参和参数区域。 在构建了区域映射之后，验证器检查属性（P2）和（P3）是否对伪调用位置保持（属性（P1）不需要检查）。5.5其他结构一些语言结构需要特殊处理。因为很难识别存储在静态字段中的对象的生命周期，所以我们的区域编译器将这些对象放置在一个不朽的区域中，该区域的生命周期跨越整个程序的生命周期。验证器相应地工作：不朽区域是每个方法的框架中的一个特殊区域（索引为0）;从静态字段中加载或存储的区域必须是不朽区域。同时也要求被抛出的对象必须在不朽区域。对于多线程，验证器要求子线程使用的所有区域都必须作为参数传递给线程启动方法m，即Um=Pm。此外，验证器将所有这些参数区域视为线程启动方法中的局部区域这些区域是共享区域，运行时系统将确保只有最后一个试图删除这些区域的线程才会真正删除它们，如第2节所述。6实验我们已在内置于Soot基础设施中的Jreg区域编译器中实现了区域证书生成[21]。编译器生成区域cer-198S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183程序原始BC区域BCReg. BC+证书百分增加已验证方法调用bh301333167736573百分之二十一283537比索尔808084919556百分之十八239405em3d118341278414854百分之二十六248439健康161431721420464百分之二十七253446MST116671209014738百分之二十六259435周边156631594318161百分之十六269432功率242742476726598百分之九246419treeadd520654385912百分之十四232393tsp109721131912378百分之十三242435Voronoi256012669630786百分之二十273560图3.第三章。以字节为单位的程序大小，认证开销;方法和调用已验证。使用我们的编译器分析结果与区域注释的字节码一起定义;分析和证书生成都发生在三地址中间表示中。这是可能的，因为所有的区域信息，包括指向信息，是独立于如何将中间代码降低到字节码。区域编译器生成区域证书作为类文件中的方法属性。大多数属性与代码结构无关;只有有关调用位置的返回区域的信息取决于调用的程序计数器。此特定属性编码在 与行号属性的方式相同我们还在Ka e虚拟机的解释器中实现了验证器[22]。我们在VM执行标准字节码验证之后立即执行加载时验证。当第一次遇到调用时，在运行时，链接验证是惰性的。为此，我们包含了一个标记，以指示调用是否已被验证。我们使用Olden benchmarks for Java [5]对验证器进行了评估图3的左半部分显示了这些程序的字节码大小统计数据：第一列显示了应用程序的原始大小;第二列显示了带有区域指令但没有区域证书的字节码的大小;第三列显示了包括证书的字节码的大小;第四列显示了带有完整注释的程序的大小比原始程序增加的百分比。这些数字表明，这组程序的平均尺寸增加达到可接受的19%。正如预期的那样，区域证书负责区域字节码的大部分大小增加。检查证书大小，我们确定，平均而言，35%的证书大小是由于点到图;更有趣的是，22%的证书大小是由于点到图。S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183199需要存储表示指向关系中的字段的字符串。我们指出，我们并未尝试优化这些尺寸，更好的表示和压缩技术可能会产生更小的证书。我们亦已收集有关该等基准的实际验证过程的统计数据。图3的左半部分显示了在类加载期间验证的方法的数量和在程序执行期间检查的调用站点的数量。这些数字包括库方法的验证。最后，执行时间表明Ka e解释器中的验证运行时开销是微不足道的：程序运行时间在10到266秒之间，验证开销平均为0.18%，最大为0.6%。这些结果证实了这样的预期，即一旦证书中的关键信息可供验证者使用，安全检查就会变得便宜我们设想，即使对于即时编译系统，区域验证开销仍然很小。6.1Bug检测和修复验证器已经成功地在我们的区域编译器中发现了几个错误。验证器检测到的第一个错误是在合并点处存在不一致的活动区域集。 被拒绝的代码表明，在某些情况下，编译器没有为带有空假分支的条件语句放置适当的删除指令。验证器发现的第二个问题是，所有字符串，包括常量，都被视为堆对象。 当然，定弦不应该被分配区域，而是放在仙域。检测到的第三个错误是，我们的编译器在继承和方法重写的情况下生成不一致的区域参数签名。我们已经成功修复了所有这些bug。事实证明，核查员在两个方面很有帮助。首先，它捕获了一些错误，否则这些错误会悄悄地通过，因为它们不会损坏内存。其次，它给出了错误原因的良好指示，并且更容易修复它们。7相关工作在基于区域的内存管理的语言支持领域已经有大量的研究。Tofte和Talpin [20]提出了一种简单类型lambda演算的区域推理算法，并使用这种技术为ML程序提供自动区域支持[2，19]。在他们的系统中区域是词汇作用域，这对区域的生命周期强加了一个堆栈规则. Aiken、Fahndrich和Levien [1]建立在这种方法的基础上，但在词汇上，200S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183将区域分配与区域解除分配解耦。RC系统[10]和Cyclone [12]提出了对C程序中区域的语言支持其他一些系统扩展了Java的区域支持。Christiansen和Velschow提出了RegJava [8]，它用区域注释的类类型扩展了Java。博亚帕蒂等他提出了一个在Java程序中结合所有权和区域类型的系统[4]。我们自己最近的工作[6]和Chin et. [7]提出了一种区域推理算法，它能自动地将输入的Java程序转换成具有区域支持的输出程序[7]。最后，Java的实时规范（RTSJ）[3]提供了一个API来支持作用域内存区域和不朽内存;但是，它需要运行时检查来确保内存安全（例如，不存在悬空引用）。相比之下，我们的方法在字节码级别提供了轻量级区域支持，本文中提出的验证器消除了运行时检查的需要。除了[1，13，10]之外，大多数C，Java和ML的区域系统都使用词法范围的区域，使用区域类型系统，并生成可以进行类型检查以确保正确性的良好类型输出程序。像[1]这样的系统没有提供检查转换结果是否正确的方法像RC [10]这样的系统使用运行时技术来确保内存安全。据我们所知，本文中的工作是第一个解决字节码级别的区域安全性验证。在字节码验证领域，已经提出了各种分析算法，如最近的调查[15]所示。基本的Java字节码验证算法是由Sun的Gosling和Yellin [16，11]提出的，它基于数据流分析。我们的区域验证与标准JVM验证是正交的，因为它只检查区域构造，但其他方面则依赖于标准验证器来执行所有其他检查。标准字节码验证通常由于对象初始化和子例程验证而变得复杂。对象初始化需要某种形式的必须别名分析，以确定对象是否已正确初始化。已经提出了相当简单的关于别名的推理方法，以及某些限制[9]，以确保正确的初始化。另一个问题是子例程，其中需要上下文敏感的方法来允许更大类的有效程序被成功验证。这两种方法都与区域验证相关，并且可以由标准验证器处理（事实上，我们的系统使用Soot [21]，它通过内联2消除了子例程）。与这项工作更相关的是一般的证明携带代码方法[17]，其中可执行代码伴随着正确性证明。对于字节码2这是可能的，因为子例程在JVM中不允许递归[16]§4。8 .第八条。2S. 切勒姆河Rugina/Electronic Notes in Theoretical Computer Science 141（2005）183201验证，这个想法已经被用来在字节码中包含证书，以加速验证[18，14]。更确切地说，证书在控制流连接点提供类型不变，从而用单次类型检查取代基于队列的类型推断。我们的系统还遵循携带证明的代码范式：与字节码一起提供的区域信息是区域操作的内存安全性的证明。8结论我们已经