本文主要研究面向二进制程序的动态漏洞检测方法.目前主流的动态漏洞检测方法包括模糊测试、动态符号执行和动态污点分析3种方法.模糊测试的基本思想是:构造大量畸形输入,交给目标程序执行,如果程序产生异常(崩溃、挂起等),就有可能存在一个潜在的漏洞;动态污点分析追踪用户输入在程序执行过程中的传播,通过检查软件中的安全敏感操作的输入数据是否为污点数据来检测漏洞.以上两种方法都有各自的优缺点,模糊测试使用简单但是随机性太强,动态污点分析能够精确分析漏洞成因但是只能分析当前已经执行到的程序路径,使用这两种方法的共同缺点是难以获得较高的代码覆盖率.代码覆盖率是软件在测试中执行到的代码量占软件代码总量的比率.理论上,如果软件在某次测试中能达到百分之百的代码覆盖率,就能发现其所有漏洞.与模糊测试、动态污点分析相比,动态符号执行在提高软件测试代码覆盖率方面具有很大的优势,成为漏洞检测技术的研究热点和发展趋势.
本文针对现有动态符号执行方法在通过约束求解生成测试用例时,生成的测试用例存在大量重复或近似重复的问题,提出了一种基于禁忌搜索(Tabu Search,TS)的动态符号执行方法,并实现了一个相应的工具原型SwordSE.SwordSE的核心思想为:①以Valgrind VEX[1]中间表示作为符号执行的基础,通过动态插桩来实现符号引入、符号传播和约束收集;②使用Simple Theorem Prover(STP)[2]约束求解器求解路径约束来生成测试用例,通过约束分析和求解缓存来提高求解效率;③以禁忌搜索算法作为路径搜索算法,减少重复测试和避免循环,提高路径搜索效率.
1 概 述1.1 禁忌搜索算法禁忌搜索算法是一种亚启发式(meta-heuristic)随机搜索算法,它从一个初始可行解出发,选择一系列的特定搜索方向(移动)作为试探,选择实现让特定的目标函数值变化最多的移动.为了避免陷入局部最优解,禁忌搜索采用禁忌表(tabu list)对已经进行的优化过程进行记录和选择,指导下一步的搜索方向[3, 4, 5].
禁忌搜索算法的特征由禁忌对象和长度、候选集和评价函数、停止规则和一些计算信息组成.具体可描述为[6]:
步骤1 初始化禁忌表H=,选定一个初始解xnow.
步骤2 满足停止规则时,停止计算,输出结果;否则,在xnow的邻域N(xnow)中选出满足不受禁忌的候选集Can_N(xnow);在Can_N(xnow)中选一个评价值最佳的解xnext,xnow:=xnext;更新历史记录H,重复步骤2.
1.2 动态符号执行动态符号执行以符号输入代替实际输入,以符号表达式代表程序变量,在模拟程序执行过程中遇到分支时收集约束条件,通过求解约束条件并自动生成测试用例来遍历程序中的所有可达路径[7, 8, 9].从2005年最早出现至今,已经涌现出了一些优秀的动态符号执行工具,本文对它们做了一个对比分析,重点比较它们采用的路径搜索算法.如表 1所示,可以看出,各个工具采用的路径搜索算法不尽相同,DART和CUTE的算法最简单,仅仅使用了深度优先算法,S2E的算法相对复杂,综合使用了深度优先、广度优先和随机算法.总的来说,动态符号执行的路径搜索算法正朝着智能化、多样化的方向发展,另外一个趋势是由面向源码向直接面向二进制程序发展.
表 1 典型动态符号执行工具对比Table 1 Contrast of typical dynamic symbolic execution tools
| 工具名 | 时间 | 面向源码/二进制 | 是否开源 | 路径搜索算法 |
| DART[10] | 2005年 | 源码 | 否 | 深度优先 |
| CUTE[11] | 2005年 | 源码 | 否 | 深度优先 |
| EXE[12] | 2006年 | 源码 | 否 | 深度优先、最佳优先 |
| KLEE[13] | 2008年 | 源码 | 是 | 覆盖率优化,随机 |
| SAGE[14] | 2008年 | 源码 | 否 | 代搜索 |
| Fuzzgrind[15] | 2009年 | 二进制 | 是 | 代搜索 |
| S2E[16] | 2011年 | 二进制 | 是 | 深度优先、广度优先、随机 |
| Fuzzball[17] | 2012年 | 二进制 | 是 | 决策树 |
表选项
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).
 |
| 图 2 IRSB示例Fig. 2 An example of IRSB |
| 图选项 |
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.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, 19, 20, 21, 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所示,①②④⑧、①③⑥、①②⑤ B11 B14 、①②⑤⑩ B12 B16 B17 都是程序执行路径,程序分支节点越多,路径数量就越大.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没有“MaxDiff”和“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
| 被测软件名称及版本 | 测试5 min找到的路径数 | 测试10 min找到的路径数 | ||
| SwordSE | Fuzzgrind | SwordSE | Fuzzgrind | |
| gzip 1.4 | 450 | 161 | 920 | 258 |
| aplay 1.0.25 | 96 | 47 | 189 | 78 |
| php 4.4.5 | 390 | 210 | 578 | 320 |
| swfdump 0.9.2 | 158 | 112 | 330 | 194 |
| zip 3.0 | 397 | 209 | 685 | 237 |
| bzip2 1.0.6 | 414 | 307 | 793 | 551 |
| jpeg2swf 0.9.2 | 393 | 353 | 834 | 799 |
表选项
3.2 漏洞检测能力测试这一部分实验主要测试SwordSE的0day漏洞检测能力.截至目前为止,SwordSE在实验中已经发现了4个0day漏洞(这些漏洞用原始版本的Fuzzgrind不可发现),包括两个整数溢出漏洞、一个整数除0漏洞和一个双重释放漏洞(double free),具体如表 3所示.
表 3 SwordSE已检测到的0day漏洞Table 3 0day vulnerabilities detected by SwordSE
| 软件名称版本 | 输入文件格式 | 可执行文件大小/KB | 漏洞类型 |
| wav2swf 0.9.2 | wav | 261.1 | 整数除0 |
| png2swf 0.9.2 | png | 150.4 | 整数溢出 |
| swfdump 0.9.2 | swf | 749.5 | 整数溢出 |
| tiff2pdf 3.9.5 | tiff | 147.0 | 双重释放 |
表选项
以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漏洞,体现了较强的漏洞自动化检测能力.
参考文献
| [1] | Armour-Brown C,Borntraeger C,Fitzhardinge J,et al.Valgrind[EB/OL].[S.l.,s.n.][2015-05-15].http://valgrind.org/. |
| Click to display the text | |
| [2] | Ganesh V,Hansen T.STP constraint solver[EB/OL].[S.l.,s.n.](2015-04-02)[2015-05-15].http://stp.github.io/. |
| Click to display the text | |
| [3] | Glover F.Tabu search—Part I[J].ORSA Journal on Computing,1989,1(3):190-206. |
| Click to display the text | |
| [4] | Glover F.Tabu search—Part II[J].ORSA Journal on Computing,1990,2(1):4-32. |
| Click to display the text | |
| [5] | 百度百科.禁忌搜索算法[EB/OL].[S.l.,s.n.][2015-05-15].http://baike.baidu.com/link?url=JqehYmMCAMqByyTSESOHM4_qjLUmbDLbM7L3iX2ZSu5vQRFpQgWXDR2Q2CDAR-qdgQfD4OR-zYq5e3EvEUT_Ta. Baidu encyclopedia.Tabu search algorithm[EB/OL].[S.l.,s.n.][2015-05-15].http://baike.baidu.com/link?url=JqehYmMCAMqByyTSESOHM4_qjLUmbDLbM7L3iX2ZSu5vQRFpQg-WXDR2Q2CDAR-qdgQfD4OR-zYq5e3EvEUT_Ta. |
| Click to display the text | |
| [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). |
| Cited By in Cnki (6) | |
| [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. |
| Click to display the text | |
| [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. |
| Click to display the text | |
| [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. |
| Click to display the text | |
| [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. |
| Click to display the text | |
| [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. |
| Click to display the text | |
| [15] | Sogeti ESEC Lab.Fuzzgrind[EB/OL].[S.l.,s.n.][2015-05-15].http://esec-lab.sogeti.com/pages/fuzzgrind.html. |
| Click to display the text | |
| [16] | Chipounov V,Kuznetsov V,Candea G.S2E:A platform for in-vivo multi-path analysis of software systems[J].ACM SIGARCH Computer Architecture News,2011,39(1):265-278. |
| Click to display the text | |
| [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. |
| Click to display the text | |
| [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. |
| Click to display the text | |
| [19] | Goldberg E,Novikov Y.BerkMin:A fast and robust SAT-solver[J].Discrete Applied Mathematics,2007,155(12):1549-1561. |
| Click to display the text | |
| [20] | Hamadi Y,Jabbour S,Sais L.ManySAT:A parallel SAT solver[J].Journal on Satisfiability Boolean Modeling & Computation,2009,6(4):245-262. |
| Click to display the text | |
| [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. |
