GDSL：一种解释机器语言的领域特定语言（DSL）

可在www.sciencedirect.com在线获取理论计算机科学电子笔记289（2012）53-64www.elsevier.com/locate/entcsGDSL：一种解释机器语言亚历山大·塞普1 朱利安·克兰茨1 阿克塞尔西蒙1，2慕尼黑工业大学85748Garching，德国摘要可执行代码的分析需要从字节（或字）序列和它们的语义规范中重构指令。解决这个问题的大多数前端只支持单一的体系结构，绑定到特定的编程语言，或者难以维护。在这项工作中，我们提出了一个领域特定的语言（DSL）称为GDSL（通用解码器规范语言），指定主指令解码器和指令到语义的翻译我们通过说明其在英特尔x86平台上的使用来激发其设计一个编译器，生成C代码，对手手工制作的解码器实现。保留字：可执行分析，二进制分析，指令译码器，程序语义1介绍可执行代码的分析已经成为程序分析中的一个最近的焦点，以解决恶意软件，闭源软件的分析，并解决编译器引起的错误。从组成程序的输入（字节）序列重构汇编指令是进行这些分析的第一步。第二步是将每个语句映射到可以是值、定时或能量语义等的含义，这取决于分析的目的。这两个方面通常通过编写特定于体系结构的解码器和转换器来解决，以分析的实现语言表达某些内部表示。我们工作的目标是建立一个基础设施，指定解码器和翻译语义使用域特定语言（DSL），可以编译成现有的分析工具的编程语言。为此，我们提出GDSL和激励其设计的任务，指定解码器的英特尔x86。1Email：fi r stname. 我是一个女孩。你好。De2这项工作得到DFG Emmy Noether方案SI 1579/1的支持。1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.11.00654A. Sepp等人理论计算机科学电子笔记289（2012）53创建DSL来指定汇编指令的解码器和语义的动机是Dagstuhl研讨会上关于可执行代码分析的讨论这里，人们意识到，许多研究小组使用特定于体系结构的解码器和手写的语义解释来实现原型分析。除了重复工作之外，这些方法通常是不完整的，它们绑定到一个体系结构，并且难以维护，因为它们的指令表示是针对特定项目的。在存在稳步增加的指令集和需要适应分析新的目标，如包含在恶意软件中的虚拟机，可维护性和简单的解码器规范是越来越重要。为此，期望对指令进行逻辑分组，或者当转换多个处理器的指令时，在所有的相位上进行分组，从而实现这种逻辑分组然而，为了效率起见，解码器必须基于来自输入序列的下一个值（以操作码为中心的分派）做出决定虽然像lex这样的经典扫描器生成器可以将以助记符为中心的规范转换为以操作码为中心的解码器，但它允许并鼓励重叠模式。请考虑以下lex scanner规范：维 海 莱|Do|switch| 加 西 埃{printf （ “keyword%s“ ，yytext）;}[a-zA-Z][a-zA-Z0-9]*{printf（“ident%s“，yytext）;}这里，关键字和标识符的模式是重叠的：in-put while匹配两个规则。 在这种情况下，lex使用在规范文件中首先出现的规则。因此，返回一个关键字。重叠模式在扫描仪规格中是理想的，因为它们提高了可读性和简洁性。然而，在指令解码器中，重叠模式是不希望的，因为规则被写入的顺序开始起作用，这反过来又排除了以助记符为中心的规范。因此，DSL的maintenance解码器规格，阳离子必须提供一个简洁的方式写非重叠模式，以准确匹配的指令。另一个挑战是用于指定参数的指令的非恒定位的处理由于参数位经常遵循重复出现的模式，因此需要一种抽象机制来保持规范的简洁。例如，Intel x86指令中的mod/rm-byte遵循许多操作码，并决定使用哪个寄存器。图1显示了英特尔手册的摘录，其中第一列显示了一起构成一条指令的两个字节。第二个字节/r是mod/rm-字节，它确定哪个8位寄存器r8和哪个指针r/m8代表。在我们的解码器规范语言中，我们定义了函数r/m83和r8来生成指令的参数。mod/rm-byte的内容由名为/r的子解码器读取，该子解码器将读取的字节存储在内部解码器状态中。该子解码器可以在解码器中重新用于ADD和ADD：valmain[0x00/r]=binopADDr/m8r8valmain[0x28/r]=binopSUBr/m8r83我们允许/作为标识符的一部分，以适应英特尔命名法。A. Sepp等人理论计算机科学电子笔记289（2012）5355操作码指令描述00/r28/r添加r/m8、r8r/m8，r8把r8加到r/m8上。r/m8减去r8。图1.一、英特尔x86手册中的两个典型说明在这里，解码器main被声明为读取0x00（resp. 0x 28），然后运行子解码器/r。binop函数是一个简单的包装器，它执行函数r/m8和r8（访问/r存储的值），并将结果应用于传入的构造函数（这里是ADD和NULL）。通过使用子解码器（例如通过内部状态进行通信的/r），我们的主解码器非常接近英特尔手册图1中的规格。由于我们的DSL是一种类似ML的函数式语言，它足够强大，可以描述解码器的所有部分，甚至是在其他解码器框架中经常手工编码的r/m8和r8这种全面的方法使用户能够添加/r的原始设计中没有预料到的指令。总之，GDSL对现有方法的改进如下：• 它的抽象机制使得能够定义指令解码器，该指令解码器非常接近于在解码器框架的模型中使用的系统，甚至通过解码器框架的最终用户来确保可实现性• 我们的规范在编译过程中进行了类型检查，并检测到重叠模式这确保了所得到的解码器的高保真度，尤其是在解码器的模型中的预处理中。• DSL足够灵活，可以适应各种架构。由于其通用性，可以将本地指令转换为一些抽象语义，这将使二进制分析工具能够分析使用我们的框架描述的任何架构的代码• 我们提供了一个原型编译器，生成C代码，这是有竞争力的其他解码器。通过编写新的后端，可以将规范翻译为其他语言或用于其他目的（例如测试生成）。在下一节介绍了GDSL的设计之后，3通过详细说明Intel前缀的解码来说明其表达能力第4节介绍了我们的实施之前的评价。第5节介绍了相关的工作。2通用语言概述本节通过演示各种语法结构的使用来讨论GDSL的设计一般的想法是，解码器规范是一个可执行的功能程序，消费的输入序列，并产生一个堆包含- ING抽象语法树（AST），代表公认的指令。在堆中的AST被处理之后，堆可以被重新用于解码下一条指令，从而避免了对垃圾收集器或为每条指令分配内存的需要56A. Sepp等人理论计算机科学电子笔记289（2012）53∗∗∗- 是 的联系我们.Σ∗ΣDecl：：=granularity=num粒度lsbfirst∗| 导出ID为0。ΣΣΣ| typeid=类 型 的 con|类型的con| typeid=类型| validid=Expr| valid[TokPat]=Expr| valid[TokPat]|Expr=Expr类型：：=int||num||ID| {field：Type，field：Type}∗TokPat：：=hex-num| ID|'BitPat'BitPat：：= BitStr.BitStr服务器|| ID@BitStr|BitStr| id：numBitStr：：=0|1|..Σ∗Expr：：=Pat：Expr的case Expr |患者：Expr| ifExprthenExprelseExpr| letvalid=ExprinExpr| Expr Expr| num. | 'BitStr'| ID|con| {field=Expr，field=Expr}（一）（二）（三）（四）（五）（六）（七）（八）（九）（十）（十一）（十二）（十三）（十A. Sepp等人理论计算机科学电子笔记289（2012）53571粒度82exportmain3typeinstr=ADD 关于{op 1：op，op 2：op}45valbinopconsgiveOp1giveOp2=do6个操作和1个giveOp1;7个操作和2个-giveOp2;8return（cons {op1=operand1，op2=operand2}）9端部1011val/r[12update@{mod=mod，reg/opcode=reg，rm=rm}13val/0[14update@{mod=mod，reg/opcode=15valr/m8=dosimilarforr8，r/m16，r16，.. .16r-query$rm;17重新设置（caserof ' 00 0 '：重新设置A L| '00 1 '：R e g B L）月18日结束1920valmain[0x80/0]=binopADDr/m8imm821valmain[0x 00/r]=binopADDr/m8r822valmain[0x01/r]|$opndsz=binopADDr/m16r1623|$rexw=binopADDr/m64r6424|otherwise=binopADDr/m32r32图三. 英特尔ADD指令的解码规范。类型op =寄存器的Reg|记住{尺寸 ：int，reg ：op} | Imm8 of[8].在这里，Mem构造函数的参数是一个记录，而Imm8采用一个8位的位向量，写[8]。位 向量和int是唯一的基本数据类型，单例位向量充当布尔值。复杂类型的缩写可以在第4行的语法结构中引入。产品5、6和7分别介绍了函数、解码器和带保护的解码器函数和解码器的不同之处在于，函数接受参数并且只有一个定义，而解码器从隐式输入流中读取，并且具有相同名称的定义相互补充考虑图3中截取的解码器。这里，第5行和第15行的binop和r/m8分别是带3个参数和不带参数的相反，第11、13和20行定义了解码器，如果方括号中的标记序列与当前输入匹配，则对解码器的右手侧进行评估可以通过三种方式指定令牌（Production10）：或者作为十六进制数（参见main的第一令牌），作为对另一个解码器的调用main的第二令牌）或作为位模式（如在/R和/0解码器中使用的反过来，位模式被包含在记号中，并由Productions11、12和13给出：• 字符串0，1，. （比照000 in /0）;点充当一个字符串;一组位串可以58A. Sepp等人理论计算机科学电子笔记289（2012）53通过使用竖条将它们分开来指定，例如 00| 01| 10• 如上所述，前导变量由@分隔;变量绑定到输入中的实际位;例如，/0可能已写入val/0[update@{mod=mod，reg/opcode=reg，rm=rm}• 以位为单位的宽度的变量;符号v：3是v@.的语法糖;例子是解码器/r和/o在解码器中使用该被调用的解码器的等式进行解码的“calling”的机制是，在出现被调用的解码器的模式的地方替换该被调用的解码器的模式，并且该被调用的解码器的主体被前置到解码器的右手侧。例如，main [0x 80/0]在内部翻译如下：valmain[0x80update@{mod=mod，reg/opcode=端在内联子解码器之后，使用consume原语从输入流中读取一个token：valmain=doopco de-consumecase opcodeof<0 x80：做\r-consumecase（\ r 00111000 >> 3）of000： do&update@{mod=，reg/opcode=...0 × 00 ：......在该平移期间，检测重叠图案对于大于8位的令牌大小，生成嵌套的case语句。函数和解码器的主体由Expr产生式给出。在这里，生产15，。. .，18给出了在函数语言中找到的标准构造，其中第18行中的Expr Expr表示函数应用。我们的语言允许使用记录创建复合值，记录是绑定到值的字段名称的集合。产品19允许构建新记录（在图3的第8行中使用）。foo字段的值是使用$foo提取的，它本身就是一个函数。 因此，$foo {foo=7}的计算结果为7。类似地，@{foo=x}是一个获取记录并将字段foo设置为x的函数。例如@{bar为了允许内部状态，每个解码器都是一个monad，这是从纯函数语言Haskell借用的概念[1]。monad是一种抽象类型，包含从输入状态到输出状态的函数和结果。monad的动机是将对状态进行操作的计算链接在一起，而不需要语言中的副作用产品21详细说明了do语句，它将一元操作串在一起，其结果可以绑定到一个标识符。do语句的结果是最后一个动作的结果。产生式22呈现了我们语言的三个一元动作：更新f将f应用于A. Sepp等人理论计算机科学电子笔记289（2012）5359内部状态（通常是记录更新）;查询f返回将f应用于内部状态的结果（通常是记录字段选择器）;返回x，返回x作为结果。除了query，内部状态也可以使用guards访问：$opndsz，$rexw的第一个guard，以及第22行中计算为'1'的其他值，守卫是以内部状态为参数的函数。因此，opndsz和rexw是内部状态的记录字段，否则是一个总是返回“1”的函数。3解码x86前缀解码x86指令的一个挑战是正确处理前缀：它们要么用于修改后续指令，要么是后续操作码的一部分（所谓的强制前缀）。在后一种情况下，在强制前缀和实际操作码之间允许使用其他前缀。例如，两个指令序列：67 f3 45 0f7e d1和f3 67 45 0f 7e d1编码movq xmm 10，xmm 9，其中67是ADDRSZ前缀，f3是REPNE前缀，但在这里用作强制性前缀以用于op代码0f7e。更重要的是，45不是一个数据，而是一个mod/rm字节。令人困惑的是，REX前缀必须紧接在操作码之前，否则将被忽略。某些指令，如mulss、mulsd和mulpd共享相同的操作码，这里是0f59，但有不同的强制前缀，分别是f2、f3和66。因此，前缀出现的顺序变得很重要。此外，虽然f2和f3的最后一次出现确定强制前缀，但是如果f2和f3不能启动指令，则出现66仅被识别为强制前缀。正确的解码器识别：66 f3f2 0f 59 ffmulsd xmm7，xmm7必填前缀：0xf266 f2f3 0f 59 ff毛丝xmm7，xmm7必填前缀：0xf3660f 59 ffmulpd xmm7，xmm7必填前缀：0x66f266 0f 59 ffmulsd xmm7，xmm7必填前缀：0xf2在GDSL中，根据最后一个相关的前缀，通过使用不同的解码器可以轻松地处理强制性前缀。我们解码前缀如下：val prefixes [0x66]=p/66 valprefixes [0 xf2 ]=p/ f2 valprefixes[0xf3]=p/f3valprefixes[]=mainval p/66 [0 x66]=p/66 valp/66 [0 xf2 ]= p/66/ f2 valp/66 [0 xf3 ]= p/66/f3valp/66[]=after/66mainvalp/f3[0x66]=p/66/f3 #f3dominates 66val p/f3 [0xf2]=p/f3/f2valp/ f3 [0 xf3]=p/ f3valp/f3[]=after/f3mainvalp/f3/f2[0x66]=p/66/f3/f2#f3/f2dominates 66valp/f3/f2[0 xf2]=p/f3/f2valp/ f3/ f2 [0 xf3]=p/ f2/ f3valp/f3/f2[]=after/f2（after/f3main）60A. Sepp等人理论计算机科学电子笔记289（2012）53...#p/ f2 ， p /66/ f2 ， p /66/ f3 ， p/ f2/f3 ，#p/66/f3/f2，p/66/f2/f3val /66 []=继续val/ f2[]= 继 续 val/ f3 []= 继续val /66 [0 x0f0 x59/r]= binop MULPD xmm xmm/m128 val/f2 [0x0f0 x59/r]= binop MULSD xmm xmm/m64 val/f3 [0 x0f0x59/r]= binop MULSS xmm xmm/m32 valmain[... ]=.. .导出到用户的入口点是前缀。当读取序列f3 f2 0 f 59 ff时，它发送到p/f3，p/f3本身读取f2并进入p/f3/f2。由于下一个字节0 f在p/f3/f2中没有匹配，因此执 行 /f2之 后 的 表 达 式 （ 在 /f3main之后）。after函数调用解码器/f2，如果失败，则继续（在/f3 main之后）。后一个表达式运行f3，如果这个解码器失败，则运行main。在我们的示例字节序列中，/f2解码器成功地消耗了剩余的字节0 f 59 ff并返回mulsd指令。通过构造前缀解码器，最多四个查找可能导致失败：一个前缀解码器，/66，/f2，/f3。因此，序列中至多一个字节被检查一次以上。注意，after和continue可以直接在GDSL中定义：valafterfstsnd=doupdate@{cont=snd};fstendvalcontinue=dodecoder- query $query; decoderend这里，after将其参数snd存储在解码器状态中并执行解码器fst。continue函数检索存储的解码器并分派给它。这就完成了前缀解码器的设计。4评价我们已经在GDSL中指定了英特尔x86指令集的相当一部分，以及用于较小架构（如MSP430）的解码器。在本节中，我们将比较Intel x86解码器的性能和正确性。4.1性能我们比较我们生成的代码与几个现有的disassem- bler项目的性能。表4显示了对.text段中包含671991条指令的二进制文件进行线性扫描反汇编的运行时。.text段的大小为3032027字节。二进制文件是我们早期的解码器之一，是一个静态链接的x86_64可执行文件，用于Linux。由于静态链接libc，它包含了 几 个 SSE 和 VEX 指 令 。 我 们 使 用 了 BeaEngine[2] 、 distorm[3] 、 IDAPro[4]、Debian软件包中附带的libopcodes[5]、metasm[6]、udis86[7]以及pintool软件包附带的xed2反汇编程序库[8我们在64位模式下在Linux上的IntelCore i7上运行了所有测试。BeaEngine和udis86解码指令数量的差异是由于错误解码的指令，随后由于不同的偏移导致解码进一步的错误指令。我们包含了metasm包，以完成与反汇编程序的比较A. Sepp等人理论计算机科学电子笔记289（2012）5361框架BeaEngine失真GDSLIDAProlibopcodesmetasmudis86xed2时间#仪器p/f2/f3 p/66/f2/f3REX238毫秒204毫秒673毫秒/309ms4m21s705ms672207671991671991/671991电话：+673965671991−√−−−−√−−√−√√√−√−−−−√−√−见图4。不同反汇编框架的评估。不是用C写的metasm包的结果较慢的一个可能原因同样，我们无法使用IDA Pro运行线性扫描反汇编。从表4中可以看出，GDSL生成的C代码在速度上相当，比最快的手写库慢3倍左右。然而，解码不太可能成为程序分析的瓶颈，因此我们认为性能是可以接受的。此外，进一步的（编译器）优化可以改善（缩短）生成的代码，这将有助于性能。例如，GDSL的高阶性质（部分应用的函数可以作为参数传递）需要一个称为闭包转换的过程[9]。内联后，大多数函数都是一阶的，可以更有效地调用[10]。此外，替换可用表达式将消除对位向量的许多冗余计算。4.2正确性由于解码包含前缀字节的字节序列的复杂性，我们比较了各种反汇编程序的正确性。表4有三个列，分别标记为p/f2/f3、p/66/f2/f3和REX，它们测试如第3节所述的各种前缀组合：p/f2/f3表示是否遵守f2和f3的顺序，p/66/f2/f3表示是否在读取f2或f3后额外地66失去其强制前缀状态，以及REX表示如果该前缀不是紧接在操作码之前，则是否正确地忽略该前缀。刻度表示正确的解码器。根据英特尔手册，添加任意前缀可能会导致某些指令的不可预测行为。我们创建了字节序列，根据手册，这些字节序列是不可预测的，并验证了Core i7处理器执行它们时，就好像没有多余的前缀一样。虽然它可以可以认为，对标记有不可预测行为的序列进行解码对于程序分析是不期望的，出于对齐的目的，GCC编译器例行地发出这样的序列，GCC编译器在NOP和RET指令的前面插入前缀作为一个例子，考虑以下发生在我们的测试二进制文件中的14字节填充序列：62A. Sepp等人理论计算机科学电子笔记289（2012）53666666662 e0 f1 f84000000000：nopWORDPTR cs：[rax+ rax *1+0 x0]这里，在nop操作码f1 f8之前，在段覆盖前缀2e之前有四个66前缀，此外，恶意软件可以添加虚假前缀作为附加的代码混淆技术。因此，解码器必须识别比手册推荐的更多的内容。相反，某些应用程序，如搜索gadget（字节序列，形成一个特定的指令），需要一个解码器只识别共同的所有处理器的指令。我们的GDSL语言可以使用保护来阻止某些指令被识别。某些方面，例如32位和64位模式之间的差异，可以使用不同的前缀解码器来实现（REX前缀是32位模式中的普通指令）。我们相信，解码器的开源实现很可能会收敛到在所有这些配置下都是正确的解码器。5相关工作英特尔x86指令的大多数解码器库生成或使用表将操作码映射到指令，然而，前缀和参数的解码通常是手工编码的[5，2，3，6]。一个值得注意的例外是SLED[11]，一种用于编码和解码的规范语言，它是一种类似于GDSL的综合规范SLED使用以操作码为中心的表指定助记符，从而为助记符分配固定值。除了助记符之外，还可以定义模式变量，将名称与位序列相关联。然后，助记符和模式变量用于定义指令。在这样的定义中，模式变量的字段可以使用约束进行专门化由于这些约束是相当通用的，因此不清楚它们可以在多大程度上检查所得到的指令定义是否重叠（即，约束的交集为空），并且因此不清楚可以避免必须按顺序测试约束以便找到匹配模式的频率。他们的方法类似于正则表达式匹配，但不允许重复。由于x86允许在许多但不是任意序列中使用多个相同的前缀，因此某些前缀指令很难指定。特别是，由于无法指定重复，因此很难使用SLED指定第4.2节中使用nop的填充示例。事实上，根据我们的理解，[11]中给出的x86规范不接受任何带有多余前缀的指令。即便如此，SLED解码和编码指令的能力要求规范是双向的，因此变得相对难以理解和维护。Fox等人采用了另一种方法[12]。在他们的工作中，他们描述了在HOL4证明系统中编码的完整ARMv7指令集的形式化模型[13]。该模型直接对单词序列进行操作，因为即使是解码逻辑也在证明系统中指定除了纯粹的解码逻辑，还提供了一个完整的语义的ARMv7指令集，其保真度对ARMv7实现证明。直接使用自写的解码器A. Sepp等人理论计算机科学电子笔记289（2012）5363HOL4证明系统是困难的，一个可证明正确的翻译到GDSL将是可取的。更远的是语义的规范，已经提出了许多中间表示[14，15，16]。GDSL的明确目标是还指定如何将处理器指令转换为描述其语义的中间表示使用公共框架可以帮助使各种中间表示在各种分析框架中可比较和可用最近，Reps et al.已经提出为每个处理器指令编译一个抽象的Transformer，以便获得更有效的分析[17]。未来的工作将解决我们的编译器的不同后端如何遵循此设置。我们的GDSL实现可以在https://bitbucket.org/mb0/gdsl上找到。它是用SML/NJ v110.74编写的，并在BSD许可证下发布。引用[1] S. Peyton Jones，Haskell 98 Language and Libraries：The Revised Report.剑桥大学出版社，2003年。[2]“http：//www. 是的。或G，2012年，version四、1rev172.[Online].网址：http://www.beaengine.org[3]“http：//www. 我的意思是。net/distorm/，2012年，version3.第三章。1 .一、[Online].网址：http://www.ragestorm.net/distorm/[4] 他说，“ P roDisassembl er，“http：// www. 他是X-R。我想知道，2012，versi on6. 0。十万一千零一[联机]。可用网址：http://www.hex-rays.com/idapro[5]“li b o p c o d e s，“http：// p a c k a ge s. Debian. Org/testing，2012，packag e b i nut il s-dev-2. 22比6 [On li ne]. 网址：http://packages.debian.org/testing[6]“http：//metatasm. cr0。或g/，2012年，retrevedon2012年5月25日。[Online].网址：http://metasm.cr0.org/[7]“http：//www. 我很高兴。net，2012年，version1.一、第七章[Online].网址：http://udis86.sourceforge.net[8]“x e d 2，“http：// www. 我不知道。Org，2012，versi on2. 11-49306 [Online]. 网址：http：//www.hkj.com我不知道。奥尔格[9] A. W. Appel ， Compiling with Continuations 。 New York ， New York ， USA ： CambridgeUniversity Press，1992.[10] A. Kenneddy，“与C o n t i n u a t e t i n u a tiNewYork，NewYork，USA：ACM，2007，pp. 177比190[11] N. 我的眼睛和M。F. Fernández，“M achi n e i n s t ru c t i o n s的特殊R e p r e s e n t a t i o n s“，P r o g r a mm i n g L a n g u a g e s n d S y s t e m s的T r a s a c t i o n s，v o l. 19岁，没有。第3页。492- 524，M a y 1997.[12] A. Fox和M。 O. Myren，“A T r u s t w o r t h y M o n d ic F o r m a l i z a t o n A r c t o n Mv 7 I n t r u c t o n A r c t o n A r c t o n t e n f e n f e n t e r a c t i v e r e m P r o v i n g，s er。 LNCS.Springer，2010，pp. 243-258[13] K. SLNDNDM。 N〇rrish，“A B r i e f O v e r v i e w of H O L 4“，in I n t e r n a t i o n a lC o n f e r e n c e o n n c o n t e r e m P r o v i n g in H i g h e r O r d e r L o g i c s，s e r。LNCS.Springer，2008，pp. 28比32[14] C. CifuntesanddS. 此外，所有“特别是M achi n e I n s t r u c t i n s的S e m m a n t i c ss”，均在所有工作流程中进行了修改。 我参加了98年的个人电脑展。王文 生 ， 王 文生 .[15] S. Bardin，P. 他是一个人，J。 Leroux，O. 李河 我是说，我是说，我是说。 Vincentnt，“The BI N C O A F r a m e w o r k for B i n ary C o d e A n aly s is“，in C o m p u t er A i d e V e ri f i c a t i o n，s er r. LNCS.Springer，2011，pp. 165-17064A. Sepp等人理论计算机科学电子笔记289（2012）53[16] A. Sepp，B. 我的天啊，我的天。 Simon，“通过E x t r a c t i n g R e l a t i n a l n a l n f orm a t i na t i n a l I n a r e n a r i n a r e n c e n R e v e r e n e r i n e r i n g，M. PinzgerandD. 你好，我是说。Limerick，Ireland：IEEE Computer Society，Oct. 2011年。[17] J.我是T。Reps， InInternationalC onfernceonC ompilerC on struction，ser. LNCS，vol. 4959Springer，2008，pp. 36比52