蔡军，邹鹏 ，马金鑫，何骏

(1.装备学院 复杂电子系统仿真实验室，北京101416; 2.中国信息安全测评中心，北京100085)

21 世纪是网络时代，信息网络已经成为全球经济中最重要的基础设施，与此同时，网络安全问题成为潜藏在我们每一个人身边的现实威胁，软件漏洞是网络安全问题的根源之一，大部分网络攻击都是基于软件漏洞来实施的.例如2014 年9 月发现的“ShellShock”漏洞，被称为是历来发现的最严重和最普遍的软件漏洞之一，利用这一漏洞，远程攻击者可能在受影响的系统上执行任意代码，其危害性震撼全球.因此，软件漏洞检测在网络安全领域受到了越来越多的关注.

本文主要研究面向二进制程序的动态漏洞检测方法.目前主流的动态漏洞检测方法包括模糊测试、动态符号执行和动态污点分析3 种方法.模糊测试的基本思想是:构造大量畸形输入，交给目标程序执行，如果程序产生异常(崩溃、挂起等)，就有可能存在一个潜在的漏洞;动态污点分析追踪用户输入在程序执行过程中的传播，通过检查软件中的安全敏感操作的输入数据是否为污点数据来检测漏洞.以上两种方法都有各自的优缺点，模糊测试使用简单但是随机性太强，动态污点分析能够精确分析漏洞成因但是只能分析当前已经执行到的程序路径，使用这两种方法的共同缺点是难以获得较高的代码覆盖率.代码覆盖率是软件在测试中执行到的代码量占软件代码总量的比率.理论上，如果软件在某次测试中能达到百分之百的代码覆盖率，就能发现其所有漏洞.与模糊测试、动态污点分析相比，动态符号执行在提高软件测试代码覆盖率方面具有很大的优势，成为漏洞检测技术的研究热点和发展趋势.

本文针对现有动态符号执行方法在通过约束求解生成测试用例时，生成的测试用例存在大量重复或近似重复的问题，提出了一种基于禁忌搜索(Tabu Search，TS)的动态符号执行方法，并实现了一个相应的工具原型SwordSE.SwordSE 的核心思想为:①以Valgrind VEX［1］中间表示作为符号执行的基础，通过动态插桩来实现符号引入、符号传播和约束收集;②使用Simple Theorem Prover(STP)［2］约束求解器求解路径约束来生成测试用例，通过约束分析和求解缓存来提高求解效率;③以禁忌搜索算法作为路径搜索算法，减少重复测试和避免循环，提高路径搜索效率.

1 概 述

1.1 禁忌搜索算法

禁忌搜索算法是一种亚启发式(meta-heuristic)随机搜索算法，它从一个初始可行解出发，选择一系列的特定搜索方向(移动)作为试探，选择实现让特定的目标函数值变化最多的移动.为了避免陷入局部最优解，禁忌搜索采用禁忌表(tabu list)对已经进行的优化过程进行记录和选择，指导下一步的搜索方向［3-5］.

禁忌搜索算法的特征由禁忌对象和长度、候选集和评价函数、停止规则和一些计算信息组成.具体可描述为［6］:

步骤1 初始化禁忌表H =∅，选定一个初始解xnow.

步骤2 满足停止规则时，停止计算，输出结果;否则，在xnow的邻域N(xnow)中选出满足不受禁忌的候选集Can_N(xnow);在Can_N(xnow)中选一个评价值最佳的解xnext，xnow:=xnext;更新历史记录H，重复步骤2.

1.2 动态符号执行

动态符号执行以符号输入代替实际输入，以符号表达式代表程序变量，在模拟程序执行过程中遇到分支时收集约束条件，通过求解约束条件并自动生成测试用例来遍历程序中的所有可达路径［7-9］.从2005 年最早出现至今，已经涌现出了一些优秀的动态符号执行工具，本文对它们做了一个对比分析，重点比较它们采用的路径搜索算法.如表1 所示，可以看出，各个工具采用的路径搜索算法不尽相同，DART 和CUTE 的算法最简单，仅仅使用了深度优先算法，S2E 的算法相对复杂，综合使用了深度优先、广度优先和随机算法.总的来说，动态符号执行的路径搜索算法正朝着智能化、多样化的方向发展，另外一个趋势是由面向源码向直接面向二进制程序发展.

表1 典型动态符号执行工具对比Table 1 Contrast of typical dynamic symbolic execution tools

2 SwordSE 的设计和实现

SwordSE 是在开源动态符号执行工具Fuzzgrind［15］的基础上设计实现的，其工作流程如图1所示.种子输入是提供给目标程序的初始输入，分为两类:一类是文件，一类是命令行参数.符号引入、符号传播和约束收集这3 个步骤借助Valgrind 插桩平台完成，约束求解这一步骤借助STP求解器完成.给定一个种子输入和一个目标程序，SwordSE 就会自动搜索程序的不同执行路径，并为每一条执行路径生成一个测试用例，如果在某条执行路径上有异常，就将相应的测试用例保存到一个专门的文件夹中.SwordSE 的设计目标是在尽可能短的时间内找到尽可能多的没有重复的路径，获得尽可能高的代码覆盖率.

图1 SwordSE 工作流程Fig.1 Workflow of SwordSE

2.1 基于Valgrind VEX 的约束收集

Valgrind 是运行在Linux 系统上的一个开源的动态二进制插桩平台，它使用VEX 中间表示(Intermediate Representation，IR)来实施代码分析和插桩.使用中间表示的好处有两点:①中间表示是体系结构无关的，对于不同的指令体系表示是一致的;②中间表示将复杂的二进制指令转换成了简单的中间表达形式，相比直接分析二进制指令，分析中间表示要简单得多.SwordSE 收集的路径约束就是由中间表示构成的公式，下面详细介绍约束收集过程.

2.1.1 符号引入

符号引入是将用户输入符号化的过程.SwordSE 当前支持两类输入的符号化:一类是文件类输入，一类是命令行输入，两类输入均以字节为单位进行符号化，即一个字节对应一个符号变量.

对于文件类输入，通过编写回调函数，调用“VG_(needs_syscall_wrapper)”函数插桩文件相关系统调用来引入符号，首先插桩open 系统调用，如果打开的是指定的输入文件，则将其文件描述符fd 加入到感兴趣的描述符集合中;接下来插桩read 系统调用，如果读取的是感兴趣的描述符集合中的文件，则引入符号，即为每一个读入的字节指派一个符号变量，并将这个字节在内存中的存放地址加入到受依赖的地址集合.最后还要插桩close 系统调用，如果有打开的文件被关闭了，就将其对应的fd 从感兴趣的描述符集合中删除.另外，还需要对mmap 系统调用做类似于read 的插桩，因为有些程序是通过mmap 读入文件数据的.

对于命令行输入，则调用“VG_(track_pre_thread_first_insn)”函数来插桩线程，捕捉传递给线程的命令行参数及参数的存放地址.每个参数是一个字符串，SwordSE 为字符串的每一个字节(字符)指派一个符号变量，并将其存放地址加入到受依赖的地址集合.SwordSE 不能同时将文件和命令行设为符号，要么符号化文件输入，要么符号化命令行输入.

2.1.2 符号传播

符号传播是根据程序执行语义，追踪程序变量对输入的依赖，将程序变量由上一步引入的符号变量的表达式来表示.符号传播也是通过插桩回调函数来实现，SwordSE 直接在VEX IR 上做插桩，插桩的基本单位为中间表示超级块(Intermediate Representation Super Block，IRSB).一 个IRSB 可以代表1 ～50 条汇编指令，它是一个单入口多出口的代码块.每个IRSB 由3 个部分组成:一个变量类型列表，指明了这个IRSB 中出现的所有临时变量的类型;一个IR 语句序列，代表一条或多条汇编指令;一个跳转语句，在IRSB 的末尾，指示这个IRSB 执行完后下一个要执行的IRSB 的地址(在IRSB 的中间可能还会有条件跳转语句).图2 是IRSB 的一个示例，可以看出这个IRSB 中有3 个临时变量t0、t1、t2，类型均为I32(32 位整型);有6 条IR 语句(编号为1 ～6)，其中第1 ～5 条语句就是一个IR 语句序列，代表了一条汇编指令(这个IRSB 是一个小型的IRSB，大的IRSB 由上百条的语句序列构成，可以代表50 条汇编指令);最后一条IR 语句(第6 条)就是一个跳转语句，是每个IRSB 末尾都要有的语句，可以是返回跳转(return)，也可以是条件跳转(if).

IRSB 主要由IR 语句(statement)组成，而IR语句又由IR 表达式(expression)构成.语句有Ist_IMark，Ist_Put，Ist_Store，Ist_Exit 等12 种类型;表达式也有Iex_Triop，Iex_Binop，Iex_Unop 等12 种类型.符号传播的过程就是插桩每个IRSB，逐条分析IRSB 中的语句(有的语句类型还需进一步分析构成它们的表达式类型，如Ist_WrTmp 语句)，根据语句类型及构成它们的表达式类型插桩相应的回调函数，记录它们对符号变量进行的操作.

图2 IRSB 示例Fig.2 An example of IRSB

2.1.3 约束收集

在上一步符号传播的过程中，记录了对符号变量的操作，并保存在一个数据结构DEP 中，如图3 所示，在DEP 中，value 记录了符号变量的存放地址，buf 记录了对符号变量的操作.SwordSE为每个符号变量维持一个这样的数据结构.在程序运行过程中，会产生很多临时变量，SwordSE 为每个临时变量也维持一个DEP.

图3 DEP 数据结构Fig.3 DEP data structure

约束收集就是在遇到if 条件跳转语句(Ist_Exit 语句)时，插入分析代码，检查条件表达式的值是否受输入影响，这个值也是一个临时变量，因此只需检查这个临时变量的DEP 中的buf 是否为空，如果不为空，则将当前指令地址和buf 中的内容以一定格式输出到一个文件中，这个buf 就是一个由IR 表示的路径约束公式.图4 是一个简单的路径约束示例，可以看出这条路径仅受符号输入“input(0)”(即输入的第1 个字节)影响.

图4 IR 表示的路径约束示例Fig.4 An example of path constraint represented by IR

对输出的文件进行分析，查找所有的“depending on input”语句，将if 后面的约束公式提取出来，存放到一个集合中，这个集合就是路径约束集合PC.

2.2 基于STP 求解器的约束求解

上一步进行了约束收集，得到一个用VEX IR表示的约束公式集合PC，接下来就要用求解器［18-22］对PC 中的约束公式逐个求解.

SwordSE 基于以下两点选择STP 作为约束求解器:①STP 开源且代码量不大，且支持多种输入格式;②STP 适合于求解位向量，而SwordSE 产生的约束公式正好是位向量.

求解过程分为两步:①将IR 表示的约束公式集合PC 里的公式全部转换为STP 支持的输入格式，得到新的公式集合pc.例如，图4 中的路径约束转换为STP 格式后如图5 所示;②对pc 里的公式逐个取反求解，生成新的输入.

图5 图4 中的路径约束对应的STP 格式Fig.5 STP format of path constraint showed in Fig.4

2.3 基于禁忌搜索的路径搜索

第2.1 ～2.2 节实现了一个基本的动态符号执行功能，即给定一个种子输入，能够通过符号约束收集求解生成新的子输入(也叫测试用例)，这些测试用例能够驱使程序走不同于种子输入的执行路径.

在程序执行过程中，会遇到很多的分支节点(条件跳转语句)，由此产生了不同的程序执行路径，如图6 所示，①②④⑧、①③⑥、①②⑤○11○14、①②⑤⑩○12○16○17都是程序执行路径，程序分支节点越多，路径数量就越大.SwordSE 的目的就是要在尽可能短的时间内找到通向程序漏洞的路径.

图6 程序执行路径Fig.6 Program execution paths

动态符号执行一次执行只遍历程序的一条路径，一个测试用例就代表了程序的一条路径，这样在路径遍历时，就需要遵循一定的路径搜索算法，如表1 所示.路径搜索算法的好坏直接影响路径搜索的效率.

Fuzzgrind 采用的路径搜索算法是代搜索.该算法将种子输入的执行路径作为第1 代路径，收集路径约束得到路径约束集合pc，然后对pc 中的约束逐个取反，通过约束求解生成第1 代测试用例;然后按照深度优先的原则从已生成的测试用例中选择一个作为第2 代路径的种子输入，生成第2 代测试用例，接着按照同样的方法生成第3代测试用例，依次类推，所有新生成的测试用例都将作为种子输入，直到找出所有可能的程序路径时停止搜索.

事实上，在对Fuzzgrind 做了大量测试后，发现它在生成测试用例时，生成了大量重复和近似重复的测试用例，而且很容易陷入局部邻域搜索，导致路径搜索效率很低.出现这个问题的原因主要在于种子输入的选择上，Fuzzgrind 将所有生成的测试用例按照深度优先的原则依次作为种子输入，这样存在两个问题:①两个相邻代的种子之间差异可能很小甚至相同，由此找到的不同路径很少;②将所有生成的测试用例都作为种子输入，导致迭代的次数过多，甚至是陷入循环.

针对上述问题，SwordSE 采用了禁忌搜索算法，禁忌搜索是一种全局逐步寻优算法，正好能解决上述问题，这是因为:①禁忌搜索通过建立评价函数，选择评价好的子输入作为种子输入，而不是将所有的子输入作为种子输入，减少了迭代次数;②禁忌搜索通过建立禁忌表，避免了重复搜索，避免了循环.SwordSE 通过使用禁忌搜索算法，能够在单位时间内找到更多的没有重复的路径，大大提高了路径搜索效率，进而提高了漏洞检测效率.下面具体描述算法的实现.

2.3.1 建立评价函数

建立评价函数的目的是为选择合适的子输入作为新的种子输入提供依据.SwordSE 以程序执行到的IRSB 的数量来作为子输入的评价值，如式(1)所示.评价值越大，说明该子输入执行到的IRSB 的数量越多.

要计算IRSB 的数量，只需写一个简单的Valgrind tool，对IRSB 进行插桩，设定一个全局变量N，每执行一个IRSB，就将N 加1.

2.3.2 建立候选集

SwordSE 通过约束求解从一个种子输入派生出多个子输入，候选集Can_N(xnow)是这些子输入的一个子集，如式(2)所示，候选集里的元素是将要作为种子的子输入.

候选集的建立过程如下:首先，对每一个子输入进行异常检测，查看将它们作为目标程序的输入时是否会导致程序异常，如果导致程序异常，就将该子输入保存在crash 文件夹;接下来，对每个子输入依据评价函数进行评价，然后进行去重处理，对评价值相同的多个子输入，只保留一个进入候选集.

建立候选集后，对其按评价值进行排序，选取评价值最大的子输入作为下一代种子输入，如式(3)所示.每动态符号执行一次，候选集就更新一次，每次动态符号执行的种子输入都是当前候选集中未作过种子的且评价值最大的子输入.

2.3.3 建立禁忌表

禁忌表H 记录的是已经作过种子的测试用例的评价值，如式(4)所示.如果新找到的测试用例的评价值已经在禁忌表中或者与禁忌表中的某一项十分接近(十分接近指数值相差很小，小于一个预先设定的差值上限，例如差值上限为3 表示数值相差在3 以内)，则该测试用例不能被选入候选集，从而避免了重复.

2.3.4 建立停止规则

理论上，利用动态符号执行技术可以找出所有的程序执行路径，但事实上到目前为止，受限于求解器的求解能力和符号模拟的精确程度，加之大型应用程序的路径数量相当庞大，国内外还没有哪一个动态符号执行工具能做到这一点.现有的工具都是力争在尽可能短的时间内找到尽可能多的路径，或者是直接寻找最有可能通向软件漏洞的路径，测试对象也基本都是小型程序.

SwordSE 的停止规则分为两种情况:①自动停止，即当搜索完目标程序的所有执行路径(再也找不到新的路径)时，自动停止搜索，适用于小型程序;②强制停止，即通过设定一些阈值，达到阈值后即停止搜索，阈值可以是约束公式的最大长度，也可以是禁忌表的最大元素个数等等，适用于中大型程序.

与Fuzzgrind 类似，SwordSE 提供一个配置文件“settings.cfg”来作为用户接口.用户可以通过编辑这个配置文件来设置第2.3.3 节提到的差值上限和本节提到的阈值等参数，配置文件的格式如图7 所示.例如要测试软件“gzip”，只需按照图7 的格式在配置文件中配置好各种参数，然后在命令行终端运行“./SwordSE.py gzip”即可开始测试.

图7 配置文件格式Fig.7 Format of configuration file

3 实验分析

本节对SwordSE 进行实验测试和性能评估，主要测试其两个方面的能力:①路径搜索能力，以经典的动态二进制符号执行工具Fuzzgrind 作为参照;②漏洞检测能力，看它能否自动检测出0day 漏洞.

测试环境为:Intel i5-4200M，CPU 主频为2.5 GHz，内存为4 G，操作系统为Ubuntu 12.04 32位系统.测试对象为运行在Linux 系统下的一些常用的小型应用软件.

3.1 路径搜索能力测试

主要测试在相同的时间内，针对同一个目标程序，SwordSE 和Fuzzgrind 两者谁找到的无重复路径更多.需要说明的是Fuzzgrind 并不能直接运行在Ubuntu 12.04 系统上，而只能运行在版本比较陈旧的Ubuntu 9.04 系统上，且依赖于较低版本的Valgrind.SwordSE 对Fuzzgrind 做了以下几个方面的改进:①将其匹配到较新的Valgrind 版本，使它能够在Ubuntu 12.04 上运行;②增加了更多的指令支持，使它能测试代码量更大的程序;③增加了命令行参数作为符号输入;④引入了禁忌搜索算法.

因此，这一部分的实验，重点是比较引入禁忌搜索算法后的SwordSE 和未引入禁忌搜索算法的Fuzzgrind(移植到Ubuntu 12.04 上 后的Fuzzgrind)的路径搜索效率.

实验过程如下:选取7 款软件作为待测软件，在配置文件中设置好各种参数，其中SwordSE 的“MaxCons”均设置为200，“MaxDiff”均设置为1，“MaxH”均设置为无限大;Fuzzgirnd 没有“Max-Diff”和“MaxH”参数，“MaxCons”也均设置为200.对于同一款软件，给定相同的种子输入，开启两个命令行终端，同时开始运行SwordSE 和Fuzzgrind，并计时，每隔一段时间查看两者产生的测试用例的数目，并检查是否有重复的测试用例产生.

表2 记录了在使用SwordSE 和Fuzzgrind 测试7 款软件时，测试时间分别为5 min 和10 min 时两者找到的路径数目.从表2 可以看出，在相同的时间内，SwordSE 找到的路径数目明显多于Fuzzgrind.通过对二者产生的测试用例进行检查，发现SwordSE 生成的测试用例没有重复而Fuzzgrind 生成的测试用例存在较多重复.此外，在实验中还观察到SwordSE 在达到阈值后能自动停止，而Fuzzgrind 有时会陷入局部循环搜索(即循环往复的生成重复的测试用例)而停不下来.综上所述，SwordSE 的路径搜索效率明显优于Fuzzgrind.

表2 SwordSE 和Fuzzgrind 路径搜索能力比较Table 2 Comparison of SwordSE and Fuzzgrind’s path searching ability

3.2 漏洞检测能力测试

这一部分实验主要测试SwordSE 的0day 漏洞检测能力.截至目前为止，SwordSE 在实验中已经发现了4 个0day 漏洞(这些漏洞用原始版本的Fuzzgrind 不可发现)，包括两个整数溢出漏洞、一个整数除0 漏洞和一个双重释放漏洞(double free)，具体如表3 所示.

表3 SwordSE 已检测到的0day 漏洞Table 3 0day vulnerabilities detected by SwordSE

以wav2swf 0.9.2 整数除0 漏洞为例进行分析.种子输入为一个正常的wav 音频文件yujian.wav，大小为172 KB，触发漏洞的测试用例为第558个测试用例558.wav，对两者的十六进制格式进行比较，发现它们的前19 个字节完全不同，其他字节均相同，如图8 所示.

图8 yujian.wav 与558.wav 前48 个字节Fig.8 The first 48 bytes of yujian.wav and 558.wav

漏洞现象如图9 所示，当以558.wav 作为wav2swf 0.92 的输入时，软件发生异常终止，系统提示发生了“浮点数例外(核心已转储)”.通过进一步跟踪调试，找到该漏洞的起因是发生了整数除0 异常，558.wav 的第33 个和第34 个字节代表的数值“0x0000”被作为了除数.

图9 wav2swf 0.9.2 整数除0 漏洞现象Fig.9 Phenomenon of wav2swf 0.9.2 integer division by zero vulnerability

4 结 论

本文提出了一种基于禁忌搜索的动态符号执行方法，并实现了一个相应的工具原型SwordSE.该方法充分利用了禁忌搜索算法的全局逐步寻优能力，有效避免了重复路径搜索和局部循环搜索问题，大大提高了路径搜索效率.SwordSE 不依赖于软件源码，直接面向二进制程序，支持将文件和命令行参数这两类输入作为符号来实施动态符号执行，实验表明，相比现有动态符号执行方法，SwordSE 能够在相同的时间内找到更多的无重复测试用例，且在实验中已经发现了4 个0day 漏洞，体现了较强的漏洞自动化检测能力.

References)

［1］ Armour-Brown C，Borntraeger C，Fitzhardinge J，et al.Valgrind［EB/OL］.［S.l.，s.n.］［2015-05-15］.http:∥valgrind.org/.

［2］ Ganesh V，Hansen T.STP constraint solver［EB/OL］.［S.l.，s.n.］(2015-04-02)［2015-05-15］.http:∥stp.github.io/.

［3］ Glover F.Tabu search—Part I［J］.ORSA Journal on Computing，1989，1(3):190-206.

［4］ Glover F.Tabu search—Part II［J］.ORSA Journal on Computing，1990，2(1):4-32.

［5］百度百科.禁忌搜索算法［EB/OL］.［S.l.，s.n.］［2015-05-15］.http:∥baike.baidu.com/link?url=JqehYmMCAMqByyTSESOHM4_qjLUmbDLbM7L3iX2ZSu5vQRFpQgWXDR2Q2CDAR-qdgQfD4ORzYq5e3EvEUT_Ta.Baidu encyclopedia.Tabu search algorithm［EB/OL］.［S.l.，s.n.］［2015-05-15］.http:∥baike.baidu.com/link?url = JqehYmMCAMqByyTSESOHM4_qjLUmbDLbM7L3iX2ZSu5vQRFp Qg-WXDR2Q2CDAR-qdgQfD4OR-zYq5e3EvEUT_Ta.

［6］ 邢文训，谢金星.现代优化计算方法［M］.第2 版.北京:清华大学出版社，2005:51-58.

Xing W X，Xie J X.Modern optimization methods［M］.2nd ed.Beijing:Tsinghua University Press，2005:51-58.

［7］ Cadar C，Godefroid P，Khurshid S，et al.Symbolic execution for software testing in practice:Preliminary assessment［C］∥Proceedings of the 33rd International Conference on Software Engineering.New York:ACM，2011:1066-1071.

［8］ Avgerinos T，Rebert A，Cha S K，et al.Enhancing symbolic execution with veritesting［C］∥Proceedings of the 36th International Conference on Software Engineering.New York:ACM，2014:1083-1094.

［9］ 王铁磊.面向二进制程序的漏洞挖掘关键技术研究［D］.北京:北京大学，2011.

Wang T L.Research on binary-executable-oriented software vulnerability detection［D］.Beijing:Peking University，2011(in Chinese).

［10］ Godefroid P，Klarlund N，Sen K.Dart:Directed automated random testing［C］∥Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation.New York:ACM，2005:213-223.

［11］ Sen K，Marinov D，Agha G.Cute:A concolic unit testing engine for C［C］∥Proceedings of the Joint 10th European Software Engineering Conference and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering.New York:ACM，2005:263-272.

［12］ Cadar C，Ganesh V，Pawlowski P M，et al.EXE:Automatically generating inputs of death［J］.ACM Transactions on Information and System Security，2008，12(2):10.

［13］ Cadar C，Dunbar D，Engler D R.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs［C］∥Proceedings of the 8th USENIX Symposium on Operating System Design and Implementation.Berkeley，CA:USENIX，2008，8:209-224.

［14］ Godefroid P，Levin M，Molnar D.Automated whitebox fuzz testing［C］∥Proceedings of the 16th Annual Network and Distributed System Security Symposium.［s.l.］:The Internet Society，2008:151-166.

［15］ Sogeti ESEC Lab.Fuzzgrind［EB/OL］.［S.l.，s.n.］［2015-05-15］.http:∥esec-lab.sogeti.com/pages/fuzzgrind.html.

［16］ Chipounov V，Kuznetsov V，Candea G.S2E:A platform for invivo multi-path analysis of software systems［J］.ACM SIGARCH Computer Architecture News，2011，39(1):265-278.

［17］ Martignoni L，McCamant S，Poosankam P，et al.Path-exploration lifting:Hi-fi tests for lo-fi emulators［J］.ACM SIGARCH Computer Architecture News，2012，40(1):337-348.

［18］ Moskewicz M W，Madigan C F，Zhao Y，et al.Chaff:Engineering an efficient SAT solver［C］∥Proceedings of the 38th Annual Design Automation Conference.New York:ACM，2001:530-535.

［19］ Goldberg E，Novikov Y.BerkMin:A fast and robust SAT-solver［J］.Discrete Applied Mathematics，2007，155(12):1549-1561.

［20］ Hamadi Y，Jabbour S，Sais L.ManySAT:A parallel SAT solver［J］.Journal on Satisfiability Boolean Modeling＆Computation，2009，6(4):245-262.

［21］ de Moura L，Bjørner N.Tools and algorithms for the construction and analysis of systems［M］.Berlin Heidelberg:Springer，2008:337-340.

［22］ Bouton T，de Oliveira D C B，Déharbe D，et al.Automated deduction-CADE-22［M］.Berlin Heidelberg:Springer，2009:151-156.