长期重写的JAVA字节码转换与安全策略的实现

理论计算机科学电子笔记190（2007）19-33www.elsevier.com/locate/entcsTom中的字节码重写Emilie Balland、Pierre-Etienne Moreau和Antoine ReillesUHP LORIA、INRIA LORIA和INPL LORIA{Emilie.Balland，Pierre-Etienne.Moreau，Antoine.Reilles}@loria.fr洛里亚校园科学，BP 239，54506V和UVre-l`es-NancyCedexFrance摘要在本文中，我们提出了一个长期重写的基础上操纵JAVA字节码库。我们定义了一个从字节码程序到代数项的映射，并使用TOM（JAVA的一个扩展，增加了模式匹配功能）来描述转换。TOM的一个独创性在于它提供了一种强大的策略语言来表达遍历树和控制如何应用转换规则。为了更有表现力，我们使用CTL公式作为条件，并展示了如何使用策略形式主义来确保它们的满足性。通过一些小例子，我们展示了如何以优雅的方式定义字节码分析和转换。特别是，我们概述了一个ClassLoader参数化的安全策略，限制文件访问的实现。关键词：术语重写，Java字节码，TOM，CTL1动机字节码转换是后期代码修改技术的一个示例，在编译后针对可执行程序传统的后期代码修改系统缺乏某些仅对源代码可用的有用信息然而，JAVA类文件保留了使这种方法可行的符号信息，从而实现了广泛的转换[6]。字节码转换包括添加或删除字段，方法或构造函数;更改超类，更改字段或方法的类型或签名，将方法调用重定向到新目标（例如调用安全方法），以及将新代码插入方法。这种方法可用于指定安全属性或使代码适应嵌入式JVM。有几个库用于操作Java字节码，其中SERP [12]，BCEL [1]和ASM [2]是最知名的。虽然它们功能强大，但可能需要深入了解API才能有效地使用它们。在本文中，我们建议引入一个抽象级别，基于术语和重写，使高级转换的定义和分析更容易。使用1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.05820E. Balland等人/理论计算机科学电子笔记190（2007）19代数视图的概念，我们已经扩展了ASM库，这样一个字节码程序可以被视为一个术语。这使我们能够在不知道API的情况下直接表达转换规则，从而减少用户的愿望和语言表达能力之间的差距。这种方法可以被认为类似于用于字节码转换的领域特定语言（DSL）在这篇文章中，我们考虑语言TOM，一个扩展，它增加了模式匹配和战略编程原语 现 有 的 语 言 ， 如 JAVA ， 我 们 展 示 了 如 何 可 以 扩 展 到 轻 松 地 表 达 字 节 码transformation。事实上，模式匹配与对象的结构直接相关，因此是一种非常自然的构造，通常在函数式语言中找到，用于识别模式和检索信息。此外，TOM提供了一种强大的策略语言，可用于控制规则应用程序。 规则和策略之间的关注点分离引入了良好的构造，并允许我们对转换进行推理。这提高了可重用性和表达性，从而有助于避免在实现复杂转换时引入编程错误。这两个特征特别适合于描述结构化实体的转换，例如树、术语或程序。在第2节介绍了TOM语言及其与ASM的连接之后，我们将在第3节说明为什么它易于表示字节码分析。本节所我们考虑一个简单的优化例子来概述我们的想法。特别是，我们引入TOM策略作为一种非常优雅的方式来表达时间属性， 方法的代码。在第4节中，我们给出了一个确保给定安全策略的字节码转换示例。2Java类作为Tom语言2.1表示JAVA字节码程序BCEL库已经被引入来修改JAVA字节码程序。 给定一个类，它在内存中提供一个对象表示。 ASM框架[2]是一个类似的工具，它使用不同的模型来避免一次在内存中构建字节码类的整个表示。ASM的设计基于事件驱动模型，并使用访问者设计模式来避免用对象表示访问过的结构。访问者从对应于ClassReader类的事件生成器接收结构的特定片段的事件，ClassReader类知道如何从现有类解析JAVA字节码，以及如何向底层访问者发送适当的事件。在我们的设置中，术语的概念是必不可少的，因为这是重写规则可以处理的唯一数据结构。 因此，我们开发了 GOM[8]，一个类型化树结构的生成器。给定一个代数签名，它生成一个在时间和空间上都有效的JAVA实现为了表示字节码程序，我们定义了一个代数签名，它允许我们用一个类型化的项来表示任何字节码程序。给定一个JAVA类，我们使用ASM读取内容并构建完整JAVA类的代数表示。这种方法类似于BCEL。这允许多通道E. Balland等人/理论计算机科学电子笔记190（2007）1921或全球分析。然而，通过使用散列consing技术，我们获得了一个数据结构与最大的共享，确保最小的内存占用。例如，为了将JAVA类表示为代数项，我们定义了以下签名：模块字节码importsintlong floatdouble String抽象语法TClass = Class（info：TClassInfo，fields：TFieldList，methods：TMethodList）...TMethodList = MethodList（TMethod*）TMethod = Method（info：TMethodInfo，code：TMethodCode）TMethodCode = MethodCode（instructions：TInstructionList，localVariables：TLocalVariableList，tryCatchBlocks：TTryCatchBlockList）...TInstructionList = InstructionList（TInstruction*）TInstruction = Nop（）|Iload（var：int）|Ifeq （标签：TLabel）| String，name：String，methodDesc：TMethodDescriptor）...真正的签名包含250多个不同的构造函数。由于篇幅有限，我们无法详细列出给定的签名表明类由构造函数Class表示，其中包含名称、包和导入等信息它还包含一个字段列表和一个方法列表。后者使用一个关联运算符MethodList编码，其arity不固定。如下所示，它用于对列表进行建模，并且对于描述列表中的一个或多个元素的搜索将是有用的类似地，指令列表由关联运算符InstructionList表示。 一个方法包含一个信息部分，代码部分。代码部分主要由局部变量和指令列表组成。每个字节码指令都由一个代数构造函数表示：Nop、Iload等。给定这个签名，GOM生成一个有效的JAVA实现（一个类对于每个构造函数），它允许我们表示和操作JAVA类的表示。如图1所示，给定JAVA类C，ASM用于 建立一个代数表示TC。利用Tom提供的基于表达规则的框架，这个术语可以被重写为另一个术语（TC'），该术语随后被从类C'中提取出来以用于新的J。2.2通过模式匹配TOM是一种语言扩展，它将模式匹配原语添加到现有的IM中，22E. Balland等人/理论计算机科学电子笔记190（2007）19菲尔兹菲尔兹代数对象C类方法场关于TomJavaC类新方术语TC术语TC'转换/分析通过战略改写AIC世界t世界Fig. 1. Tom中的字节码转换操作语言，如C和JAVA。模式匹配通常存在于函数语言和逻辑语言中，用于分析聚合数据的组成，并表示这些结构化数据的转换。 TOM系统的主要创新之处在于它的语言和数据结构独立性[7]。从实现的角度来看，它是一个编译器，它接受不同的宿主语言，其编译过程包括将匹配的构造翻译成底层的本机语言。由于GOM生成术语的JAVA实现，因此在下文中，我们将JAVA视为宿主语言。在实践方面，TOM提供了两个有趣的特性：一个“%match“构造用于匹配数据库，一个”“match”构造用于构建数据库。%match构造添加了类似于函数式语言的模式匹配功能。动作部分是用JAVA编写的，提供了灵活性。例如，考虑到前面给出的代数符号，我们可以用以下方式表示修改Istore或Iload的索引的函数：public int findDuplicate（intfindDuplicate，intnums）{%match（i）{Istore（x）-> {if}}请注意，使用"“来构建一个新的术语，例如Istore（newI），或者访问一个由诸如x之类的模式表示的可变实例。在允许Java表达式的情况下，不能使用“”除了语法匹配（ML）之外，该语言还提供了与中性元素的关联匹配（也称为列表匹配）。这对于对搜索空间的探索进行建模和执行基于列表的转换特别有用。例如，让我们考虑语句t为了说明列表匹配的表现力，我们首先定义一个函数，它检查Istore是否由一个指令列表执行这可以E. Balland等人/理论计算机科学电子笔记190（2007）1923表示如下：public booleanalert（）{%match（l）{instructionList（a*，Istore（index），b*）-> {return true;}}返回false;}在这个例子中，用 * 标注的列表变量被一个（可能是空的）列表实例化。因此，对于序列t，Istore（index）将在第一个位置找到，并且JAVA变量index将由 整 数 3 实 例 化 。 变 量 a 和 b 分 别 由 空 列 表 InstructionList （ ） 和InstructionList（Istore（2），Iload（3））实例化。非线性可用于搜索既存储又加载的变量public booleanalert（）{%match（l）{ InstructionList（_*，Istore（index），_*，Iload（index），_*）->{返回true;}}返回false;}请注意，index的多次使用是为了强制找到的Iload对应于先前的Istore。还请注意使用_*来表示匿名变量。当应用于t时，答案是3字节码分析与转换作为转换的一个例子，我们希望消除程序中不必要考虑以下字节码程序：Istore（3）;Istore（2）;Iload（3）;Istore（2）;Iload（2）我们希望检测控制流程图中的每个存储，以便在另一个存储之前没有具有相同索引的加载指令。在前面的例子中，第一个指令Istore（2）可以被删除。在[5]中，D. 莱西介绍了一个原始的方法来描述变换-基于重写和计算树逻辑的程序的分类[3]（CTL）。这种形式主义启发我们使用TOM工具来表示CTL公式。在这一节中，我们将介绍TOM提供的策略语言，并展示如何将任何CTL公式转换为策略表达式。 策略语言的求值机制为我们提供了一个检查CTL公式是否为真的过程：一个不失败的终止策略确保CTL公式是24E. Balland等人/理论计算机科学电子笔记190（2007）19¬∧∧¬真的3.1用于字节码分析的与通常的逻辑运算符如或一样，CTL公式可以由时态运算符组成。 这些操作符由一个路径操作符和一个状态操作符组成[4]。• 路径运算符声明公式φ是否应该对系统的所有可能的执行路径（Aφ）或仅对至少一个执行路径（Eφ）成立这些操作符是CTL特有的。• 状态运算符来自LTL（线性时态逻辑），并陈述关于路径未来的事实：XφGφFφ 这意味着 φJ将在未来得到验证例如，代码中的不变量由CTL公式AG（p）表示，其中p是我们希望始终验证的谓词。 致命属性可以用A和F的组合来定义。例如，对于一个方法，我们可以验证它总是返回一个结果，如果它不是一个void方法。这意味着，如果谓词IsReturn 验 证 了 一 条 指 令 的 类 型 为 Return ， 则 对 应 的 CTL 公 式 为 AF（IsReturn）。再次考虑我们的初始示例，未使用存储的搜索可以被转换为公式IsStore（i）AX（AU（IsLoad（i），IsStore（i），其中IsLoad（i）是谓词，如果控制流图的当前节点对应于Load（i）（类似于IsStore（i）），则该谓词为真。这个例子表明CTL公式是定义字节码分析的一种简单方法。我们将解释TOM语言是如何非常适合于定义这样的规范的。事实上，战略可以清楚地解释的CTL公式。3.2从CTL公式到策略表达式在重写社区中，策略的概念已经被引入来以一种优雅的方式描述如何应用一组规则。它们将高阶特征添加到一阶项重写规则中。一个基本的策略可以是一个转换规则，身份（什么都不做），或者失败（总是失败）：它们是基本的成分。 在我们的系统中，基本策略是类型保持的，并且通过扩展默认策略来定义：%strategy（）extendsFail（）{访问说明{Istore（i）-> {return····E. Balland等人/理论计算机科学电子笔记190（2007）1925{}}}基本策略包含隐式%match： 当应用于节点时指令，如果模式与节点匹配，则执行转换。否则，将应用默认策略（示例中为在基本策略之上，可以构建更复杂的策略，涉及基本组合子，如Sequence（s1，s2），Choice（s1，s2），All（s），One（s）等，如[10，11]所示。基 本 组 合 子 可 以 分 为 两 类 ： 遍 历 组 合 子 （ All ， One ） 和 控 制 组 合 子（Sequence，Choice，Not等）。）.• Traffic combinators描述了如何在直接子项中重写当应用于项f（t1， . . . ，tn），All（s）返回f（tJ1， . ，tJn），其中tJi对应于s到ti的应用。 如果至少在以下方面失败，则全部失败一特岛One（s）类似于All（s），但s仅适用于一个子项ti。 它未能如果s不能应用于至少一个子项（即，当应用于常量时失败• 控制组合子描述了如何根据其结果组合不同的策略：Sequence（s1，s2）表示s1和s2的顺序组合：如果s1或者S2失败，否则它导致将S2应用于S1的结果。Choice（s1，s2）表示从左到右的选择：如果s1成功，则返回结果，否则应用s2。如果s失败，则Not（s）执行Identity，否则失败。如果（s1，s2，s3）从应用s1开始。如果成功，则返回s2，否则返回s3。用s1得到的结果只是作为条件表达式用于测试。通过结合初等策略和基本组合子，可以定义更高层次的结构。例如，定点运算 符 可 以 表 示 为 dyRepeat（s） =Δμx.Choice （ Sequence （ s， x ） ，Identity（）），其中μde-表示递归运算符（类似于ML中的rec），x是变量，s是策略的参数。这个策略会反复应用策略s，直到失败，然后返回失败前得到的最后一个结果，这样Repeat永远不会失败。3.3CTL公式的策略验证在CTL中有一个最小的操作符集所有CTL公式都可以转换为仅使用这些运算符。一个最小的运算符集是假的，EG，EU，EX。其他操作符可以用这个集合定义······26E. Balland等人/理论计算机科学电子笔记190（2007）19（2））EFφ=<$EU（真，<$φ）AXφ=<$EX（<$φ）AGφ=<$EF（<$φ）AFφ=<$EG（<$φ）AU（φ1，φ2）=<$EU（<$φ1，<$（φ1<$φ2））<$EG（<$φ）经典的策略操作符可以以一种有趣的方式组合，以获得时间策略别名。主要思想是将谓词p表示为基本策略s（由%策略定义），并将CTL操作符表示为策略别名。与使用像SPIN这样的模型检查器来验证方法代码上的时间公式不同，一个特定的策略被应用于指令列表。如果访问失败，则公式为假。否则，它被认为是真的。布尔值false和true由策略Fail和身份 如果我们只考虑算子的最小集合，它们可以被定义为：使用TOM策略组合子。我们考虑如下定义的策略的解释函数公式：<$false）失败<$p1<$p2） 选择（<$p1），<$p2））（<$p）非（<$p））（从（EG ）μx.序列（μp），If（One（Identity），One（x），Identity）（p1，p2）（μx.Choice（<$p2），Sequence（<$p1），One（x））欧盟EX（p）在3.1节中未使用的商店搜索的示例中，使用了三个谓词。 对于每一个，基本策略可以使用TOM的构造%策略来定义。为了表示索引，策略不能直接被一个整型变量参数化，因为整数是不可变的，我们需要在遍历过程中修改它的值一个解决方案是使用一个JavaScript包装器。IsLoad（w）仅当访问的项是Load类型并且其索引等于包装器w的索引时才成功。%strategyIsLoad（w：IntWrapper）extendsFail（）{访问指令{ c@（Iload| Lload| Flload| Dload|（i）->{if（w.intValue（）.equals（'i））return}}}（Ⅲ）E. Balland等人/理论计算机科学电子笔记190（2007）1927在这个例子中，@对应于一个注释机制，用于保持对匹配子项的引用。在这里，变量c是用redex实例化的，并在右侧部分使用。IsStore（w）的代码类似于IsLoad（w）。IsStore（w）仅当访问的项属于Store类型并且其索引等于包装器的索引时才W. IndexStore（w）仅当访问的术语是Store类型时才成功，并在包装器w中设置相应的索引。%strategy（w：IntWrapper）extendsFail（）{访问说明{ c@（Istore|莱斯托尔|Fstore|Dstore|（i）->{setValue（i）;return}}}我们现在可以用以下组合策略来定义我们的分析：IntWrapperw =new IntWrapper（0）;Strategy storeNotUsed ='And（IndexStore（w），AX（AU（Not（IsLoad（w）），IsStore（w）;/* 使用storeNotUsed删除ins中未使用的存储 */'BottomUp（If（storeNotUsed，Remove（），Identity（）. visit（ins）;其中ins是类型为InstructionList的变量，BottomUp是从叶子到根的遍历。这个遍历可以定义为Bot-tomUp（s）=Δμx.Sequence（All（x），s）。 由于基本策略Remove（）删除列表的第一条指令，因此执行此代码将删除所有未使用的存储指令。 你可以注意到storeNotUsed并没有被定义为一个基本策略（construction %strategy），而是被定义为组合。基于策略到目前为止，我们只是在指令列表上定义遍历，而没有考虑控制流程。 显然，使用策略作为时间公式只在控制流上下文中才有意义。 第一个想法是显式地构造从指令列表中的控制流程图，但在情况下的内存成本复杂的方法不能忽视。我们的建议是使用策略，以便在遍历指令列表期间模拟控制流程。以这种方式，不需要控制流程图的存储器表示。 在指令列表中，控件从一条指令转换到列表，我们不关心Goto指令或可能干扰控制流程的异常。在TOM语言中，规则和控件是完全分离的，因此表示控制流程图（CFG）的替代方案是使用控件来指示可能的后续指令。我们已经看到，在过去的28E. Balland等人/理论计算机科学电子笔记190（2007）19Istore_1 GotoIinc8 1 1双冲If_cmplt100 5Iconst_0ad_1产品展示为了将策略应用于儿童，存在两个通用同余运算符All和One。我们可以重新定义这两个组合子，使它们的行为就像子是CFG中的以下指令。例如，假设我们有下面的JAVA代码，以及相应的字节码：整数i=0;while（i<）{i++;}0 Iconst_0（）1 Istore_1（）2中文（简体）5 Iinc（1，1）8 Iload_1（）9中文（简体）11 If_icmplt（5）图二. 所有行为的例子All策略适用于CFG运行，完整定义见图3。例如，Goto指令相对于控制流程图（对应于标签的指令）具有一个子级If_XX指令有两个子指令：一个满足表达式，另一个不满足。 图2对应于上面的字节码程序的遍历。该策略通过映射进行参数化，该映射将以带标签的指令开始的指令的子列表与每个标签相关联为了简化，我们在All的定义中不考虑异常处理的情况，但它以类似的方式解决将来使用这种形式主义将每个字节码指令与相应的帧和当前状态的含义相关联可能会很有趣4通过字节码重写实现在本节中，我们将介绍一个字节码重写的应用程序，通过将方法调用重定向到新目标来实现安全的类加载。特别是，我们将强制使用安全的API进行文件访问。[9]中讨论了使用防御类加载而不是防御虚拟机这是通过定义一个ClassLoader来实现的，它将自动验证要加载的类的代码是否包含不安全的代码片段（在我们的示例中，E. Balland等人/理论计算机科学电子笔记190（2007）1929查找像newFileReader（nameFile）.read（）这样的语句，并将它们替换为对安全方法的调用我们的程序的核心是类SecureClassLoader，它是标准JAVAClassLoader的子类。这个类包含TOM代码。与前面的例子一样，我们定义了一个包含转换规则的策略%strategy（）extendsIdentity（）{访问TInstructionList {%strategyAll（s：Strategy，m：Map）extendsIdentity（）{访问TInstructionList { c@InstructionList（（转到|Jsr）（label），tail*）->{S. return（m.get（'label））;return}c@指令列表（（Ifeq|伊夫内|...）（label），tail*）-> { s.return（m.get（'label））;S. returnreturn}c@InstructionList（（TableSw| LookupSw）[labels=LabelList（_*，label，_*）]，tail*）-> {S. return（m.get（'label））;}c@InstructionList（（TableSw| LookupSw）[dft=default]，tail*）->{ s. return（m. getName（'））;S. returnreturn}c@InstructionList（（Ireturn|...| Return（））（label），尾*）->{return}//默认情况：访问下一条指令。instructionList（_，tail*）-> { s. return}}}图3.第三章。字节码CFG专用的所有策略30E. Balland等人/理论计算机科学电子笔记190（2007）19/* 匹配 新 FileReader（nameFile）.read（）*/instructionList（before*，New（“java/io/FileReader”），Dup（），Aload（number），pokespecial[owner=“java/io/FileReader”，name=”init>"]，pokevirtual[owner=“java/io/FileReader”，name=“read”]，Pop（），* ）->{/* 将其替换为新的SecureAccess（nameFile）.sread（）*/返回‘InstructionList(before*,Aload（number），pokespecial（“SecureAccess”，”init>”），pokevirtual（“SecureAccess”，“sread”），Pop（），after*）;}}}*之前 和* 之后的变量由一个指令列表实例化的变 星 之 间 的 条 款 （ 新 （ … ） ， Dup （ ） ， . ） 是 与 新 FileReader（nameFile）.read（）语句的字节码表示相对应的Gom术语。 我们用对应于SecureAccess类的sread方法的指令来替换它们。这个规则显然不能捕获所有语义上等价的序列，例如当FileReader的实例化和对read的调用被一些代码分开时。这种情况可以通过使用EF策略在控制流程之后搜索读调用使用TOM列表匹配，我们将此策略应用于给定类的所有方法publicTClass fileError（TClass aclass）{ TMethodListmethods = aclass.getmethods（）; TMethodListsecureMethods =%match（方法）{ MethodList（_*，x，_*）->{TInstructionList ins =‘TopDown(FindFileAccess()).apply(ins);'x.getcode（）.setinstructions（secureInstList）;E. Balland等人/理论计算机科学电子笔记190（2007）1931TMethod secureMethod =}}returna. setMethods（）;}getmethods和setmethods方法在TOM库中定义，用于获取和设置给定TClass的方法。同样getcode和set-code，应用于一个项的排序TMethod，get和set代码，而getinstruction和setinstruction，应用于一个项的排序TMethodCode，get和set代码指令。TopDown是一个高级策略，它遍历从根，并使用第3节中描述的基本策略的组合定义为TopDown（s）=Δμx.Sequence（s，All（x））。transform方法将调用fileVerifypublic byte[] transform（Stringfile）{ BytecodeReader br =new BytecodeReader（file）; TClass c = br.getTClass（）;Creturn（c）;BytecodeGeneratorBG=newBytecodeGenerator（）;returnbg.toBytecode（c）;}此方法演示了图1中描述的转换过程。Af-在 从 作 为 参 数 给 出 的 类 文 件 中 获 取 TClass 类 型 的 GOM 项 之 后 ， 我 们 使 用BytecodeReader进行转换，并返回由BytecodeGenerator生成的与转换后的类对应的字节数组。在我们的自定义类加载器SecureClassLoader中，我们重新定义的唯一方法是loadclass。我们的转换在调用标准ClassLoaderdefineClass方法之前应用于字节码，该方法将字节数组转换为类的实例：public Stringname（String name）抛出ClassNotFoundException {transform（name）;Class sClass = defineClass（name，scode，0，scode.length）;returnloadClass（name）;}使用这个类加载器，我们可以确保没有类使用未经检查的文件。访问方法可以被加载，但在加载时将被转换为使用安全包装类。 为了简单起见，我们只提出了搜索 新的FileReader（nameFile）.read（）模式。 分析控制流图是必要的，以发现FileReader的创建，然后调用方法read（）。32E. Balland等人/理论计算机科学电子笔记190（2007）195结论我们已经提出了一个库，使字节码转换的战略重写。这个库允许我们将JAVA类看作一个代数项，由字节码的树表示形式形成。 转换可以被描述为重写规则，使用策略来控制它们的应用程序和探索字节码表达式。此外，我们还演示了如何使用这些策略来检查方法的控制流程图。 这种技术的一个特点是，不需要在内存中建立控制流图，以遍历它。然后，我们表明，它是可能的编码验证的时间逻辑条件在这个控制流图使用策略操作符。最后，我们说明了使用这个库的类的防御性我们定义了一个特定的类加载器，它将经典的I/O函数重定向到安全的API来访问文件。类加载器使用字节码重写来确保JVM中只加载安全的类这种转换是以一种抽象和简洁的方式定义的，从而通过减少要描述的转换和实际代码之间的差距来提高我们可以放置在代码中的信心。这项工作是第一次尝试用更抽象的方法来表达字节码转换。下一步将是更好地整合语言中时间属性[5]条件下重写规则的定义，并将这些技术应用于程序分析。确认我们真诚地感谢Jeremie Delaitre在TOM中进行的字节码重写的初始开发，以及Pauline Kouzmenko在安全加载方面所做的工作。我们也要感谢匿名推荐人的宝贵意见和建议。引用[1] BCEL，字节码工程库，http://jakarta.apache.org/bcel/。[2] Bruneton ， E'. ， R.Lenglet 和 T.Coupayye ， ASM ： 一 种实 现 自 适 应 系 统 的 代 码 操 作 工 具 ， in ：ProceedingingsoftheASF（ACMSIGOPSFrance）Jorn'eesCom posants2002：Syste`emes`acomposantsadaptables et extensibles（Adaptable and extensible component systems），2002.[3] Clarke，E.M.，E. A. Emerson和A.P. Sistla，使用时序逻辑规范自动验证有限状态并发系统，ACMTrans.Program。8（1986），pp. 244-263。[4] Huth，M.和M.Ryan，[5] Lacey，D.，“使用时序逻辑规范的程序转换”，博士。牛津大学计算机实验室（2003）。[6] Lindholm，T.和F. Yellin，[7] Moreau，P. E、 C. Ringeissen和 M. Vittek，一个 多目 标语言 的模 式匹配 算法 ， 在：G。Hedin，editor，12th Conference on Construction，Warsaw（Poland），LNCS2622（2003），pp.61比76E. Balland等人/理论计算机科学电子笔记190（2007）1933[8] Reilles，A.，Canonical abstract syntax trees，in：Proceedings of the 6th International Workshop onRewriting Logic and its Applications，2006.[9] Rudys，A. 和D. Wallach，Enforcing Java Run-Time Properties Using Bytecode Rewriting，in：2002年软件安全国际研讨会论文集[10] Visser，E.，Z.-即：A. Benaissa和A.Tolmach，Building program optimizers with rewriting strategies，in ： Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming（1998），pp.13比26[11] 维瑟，J.，访问者组合和遍历控制，在：第16届ACM SIGPLAN会议上面向对象编程，系统，语言和应用程序（2001年），pp。270-282。[12] 怀特，A.， Serp，http://serp.sourceforge.net/。