本文研究和分析了现阶段的3种主要网络程序结构及其典型漏洞,同时,对C/S结构下网络程序的漏洞检测技术进行了研究。在这一基础上提出了一种基于程序建模的网络程序漏洞检测技术,并利用该技术实现了一套网络程序漏洞检测系统。该技术对不同I/O模型下的网络程序进行关键函数提取并进一步构建程序模型,通过API函数挂钩的方式引入符号变元,对程序模型进行符号执行,通过程序模型识别和关键函数插桩的方式对程序二进制代码进行分析。当程序执行异常时得到触发异常位置的符号约束集,通过约束求解得到触发异常的具体输入和异常点,实现对目标网络程序漏洞的检测。
1 网络程序漏洞检测技术 1.1 网络程序结构及其典型漏洞分析 网络程序主要存在3种结构类型:C/S结构、B/S结构和P2P结构。这3种结构分别有着自身的优缺点,根据网络环境和用户使用需求的不同,程序开发者采用的结构也不同,且三者之间相互联系,并没有严格意义上的区分[2]。
C/S结构下的网络程序由客户端和服务器端共同组成,通过将网络任务合理地分配到网络程序的双端,达到降低系统开销、充分利用双端软硬件条件的目的[3-4]。C/S结构下网络程序的双端建立连接后会一直保持连接状态,任何一方都可以实时地向对方发送信息或文件。如微信、QQ等即时通信软件,通过安装在电脑上的客户端向腾讯的服务器发送数据,而腾讯的服务器也可以实时向本地的客户端回复信息和文件请求。该架构下的大量工作在客户端进行,服务器端作为中介节点执行保存、转发功能,双端信息交互有着实时转发、一对一通信、点对点单线传输的特性,现阶段如QQ、微信、迅雷、快播、暴风影音等众多商业软件都采用该结构。C/S结构下的网络程序,除了协议解析和对数据提取模块外,客户端和服务器端在本地运行过程中的原理和普通二进制程序基本相同,因此,其本身存在的漏洞也以典型的二进制程序漏洞为主,如堆栈等缓冲区溢出漏洞、格式化字符串漏洞等。
B/S结构是在C/S结构的基础上变化、改进而来,主要是为满足互联网用户通过浏览器浏览、查询信息的需求。B/S结构下网络程序的客户端一般以浏览器的形式存在,客户端仅实现部分逻辑运算和信息处理,而将大部分的运算和需求处理交付给服务器端实现。该架构用于支持多人访问的门户网站或论坛,如搜狐、新浪、微博等,该类情况下无需信息的实时性,但需要其长期有效[5]。B/S结构下网络程序的服务器端为网站服务器,但客户端浏览器的结构和功能得到简化,由于HTML等网络编程语言的特性,导致网站本身(服务器端)和浏览器(客户端)存在的漏洞以典型的web漏洞为主,如SQL注入,XSS跨站脚本漏洞,CSRF跨站请求伪造,文件上传等。
P2P结构是一种最新提出的网络程序结构形式,目的是适应点对点网络中程序开发的需求,该结构最大的优点是分布性和共享性[6]。但由于取消了服务器端的存在,网络用户以服务器端和客户端的双重身份出现在网络中,导致了网络可信性的下降和网络资源的丢失。同时,由于客户端高度分散难以管理的缺点,导致现今互联网上并不存在纯P2P结构的网络程序,在应用过程中P2P结构网络常和前两种结构混合使用,除了搭载在各个客户节点的客户端外,一般仍会布置一台或多台中心服务器,用来保存核心资源起到维持网络的作用。根据混合结构的不同,该结构下网络程序中存在的漏洞也同样以C/S结构和B/S结构本身的漏洞为主。
1.2 网络程序漏洞检测方法 现阶段,研究人员针对不同结构下的网络程序漏洞已进行了相关研究,并基于各项研究形成了一些相关工具。文献[7]就针对B/S结构下的浏览器端漏洞挖掘进行了研究,其通过特征提取的方式制定漏洞模板,并利用此类模板进行漏洞检测,其对于XSS和SQL注入等web漏洞有较好的检测效果,特别是在可视化方面实现较好。文献[8]同样针对XSS和SQL注入等web漏洞进行挖掘,不同的是其采用了Fuzzing技术,通过构造大量随机输入的方式执行目标程序寻找漏洞点,该挖掘方法的效果较为直接,针对挖掘到的漏洞也能很好地提供相关信息和触发POC。文献[9]在Fuzzing技术的基础上提出了一种结合了动态污点分析的漏洞检测技术,针对C/S架构下的网络程序二进制漏洞进行检测,实验证明该方法针对协议漏洞有较好的效果。文献[10]提出了一种基于QEMU虚拟机的二进制程序离线动态污点分析方法,该技术通过硬件虚拟化的方式提高了污点分析过程中的执行效率。文献[11]使用符号执行技术对B/S结构下浏览器端存在的Use-After-Free漏洞进行检测并实现了一套检测工具,该工具针对Use-After-Free漏洞进行了模型分析和开发,因此针对性更强。
1.3 符号执行技术 作为一种重要的漏洞检测手段,符号执行技术将具体的输入值替换为符号变元,通过监控数据流的方式记录程序的执行轨迹,并实时收集与符号变元相关的路径约束条件,当一条路径执行完毕后,系统会恢复到上一分支节点探索新的执行路径。通过对程序进行全路径分析的方式寻找触发程序崩溃的位置,求解从程序起始点到达该点的路径约束集,就能够同时得到漏洞点和触发该漏洞的POC输入[12-14]。
早期的符号执行技术主要采取了静态分析的方式,这主要是受限于计算机系统软硬件的性能,该方式在不运行程序的前提下通过程序代码分析的方式获得执行约束,能够极大地降低系统消耗,但由于缺少程序执行过程的动态信息导致分析过程的代码覆盖不够准确[15-16]。之后研究人员针对该问题提出了动态符号执行思想,通过真实运行目标程序的方式检测漏洞存在点,该方式提高了漏洞发现的准确率,但随着程序规模的扩大出现了路径爆炸的问题,特别是随着路径复杂度的提升路径约束的复杂度也随之提升,受限于约束求解器的性能,导致符号执行技术一直没有得到更好的应用和发展。随着2009年选择符号执行的提出,该问题得到了一定程度上的解决。该技术的思想核心首先是对执行位置和区域的“选择”,如图 1所示,通过选择符号执行技术将符号执行区域限制在网络程序的核心函数调取部分,而针对非程序核心或者一般性程序代码区域进行具体执行过程,这样,有效地降低了系统运行开支,同时降低了符号约束求解过程的复杂度。
图 1 选择符号执行技术 Fig. 1 Technology of selective symbolic execution |
图选项 |
S2E系统由瑞士洛桑理工大学的Chipounov等[13]开发,该系统基于选择符号执行技术构建系统框架,提供了基本的功能性插件模块。例如,开发者能够通过Selection Plugins类插件制定注入符号值的位置和选择执行的路径,当OS Event Monitor类插件中的Module Execution Detector截取到系统对目标函数的调用时,会发送信号给执行插件,此时系统会跳转执行定义好的行为或者启动符号执行过程。
本文原型系统采用了选择符号执行技术,系统基于S2E符号执行平台进行开发,其中QEMU虚拟机为待测试程序提供了模拟运行环境,并为运行提供全系统的执行监控;LLVM提供二进制翻译,将二进制代码翻译为可供符号执行引擎使用的中间级代码;KLEE进行符号执行。同时,针对不同种类的网络程序进行架构抽取并建立函数模型。与以往的技术相比创新点主要体现在3个方面:一是针对目标程序进行全系统模拟,能够更好地发现目标程序存在的真实漏洞,而选择符号执行技术能够将符号执行的区域集中在敏感区域,有效地降低了符号执行的路径爆炸问题;二是建立了不同类型网络程序模型,通过目标识别的方式调取不同模块,检测的针对性更强;三是抽取程序运行过程中的关键函数进行函数挂钩和挂钩执行语义定制,通过监控符号执行的过程记录符号约束表达式,针对出现的程序崩溃进行约束求解,能够直接定位到程序漏洞点和触发漏洞的具体输入。
2 基于函数挂钩的符号化数据引入 S2E平台对自身框架代码进行了开源,并提供了5种功能性插件供给开发者进行调用,该5类插件分别为:系统事件监控插件、执行跟踪插件、选择性插件、分析类插件和其他类插件,插件间能够相互调用。通过开发功能性插件的方式对该平台进行针对性开发,通过lua脚本操作原型系统的执行状态和执行情况。
2.1 基于API函数挂钩的执行语义定制 原型系统在执行区域选择、执行语义定制和符号化数据引入的环节上,采用了系统API函数挂钩的技术。通过在函数调用的起始点和返回点挂钩,首先可以得到系统函数服务提供过程的具体执行语义信息,其次通过截取函数调用的信号,可以控制符号变元引入的位置,间接控制了具体执行和符号执行的实际切换位置。
如图 2所示,基于选择符号执行技术思想,原型系统在QEMU虚拟机环境下正常启动目标程序开始具体执行。当程序执行到目标区域的起始位置时,Windows Monitor会捕获到操作系统对挂钩的系统API函数调用,同时将信号发送给模型模块中的执行插件,执行插件中记录了与目标位置相对应的执行语义。当目标区域执行完毕,程序执行到结束位置时,系统会截取到结束位置API函数的调用信号,当该函数执行结束时会触发返回点的函数执行语义跳出符号执行过程。
图 2 选择符号执行系统运行过程 Fig. 2 Operational process of selective symbolic execution system |
图选项 |
2.2 协议指导下字节流形式的符号变元引入 符号变元的引入通过“系统插件+lua脚本”的方式实现,根据不同的通信协议设置了符号变元的引入规则,其中定制的原型系统插件提供变元引入的具体操作,lua脚本制定了符号变元引入的具体规则。网络中数据以字节流的形式传播,与一般程序接收的输入不同,网络程序除了接收消息之外,还会接收传输的文件等,但无论是消息信息或文件数据,这些内容都是以网络字节流的形式传输,因此本系统选择通过字节流的方式引入符号变元。图 3所示是lua脚本中基于TCP协议的符号变元引入策略。
图 3 符号变元引入策略 Fig. 3 Symbolic variable introduction policies |
图选项 |
2.3 约束求解 原型系统基于STP约束求解器进行约束求解。首先,在执行的过程中会对每个执行分支节点的约束条件进行收集,2条相反路径的约束会通过取反的方式分别记录在2条不同路径的约束条件集中,新约束条件通过取并集的方式添加。STP约束求解器提供了符号变元的构造器和在此基础上的一阶逻辑中各种表达式的构造器、符号公式的可满足性判定器以及反例求解器。该求解器基于整数和位向量理论进行开发和编写,能够满足大多数网络程序执行路径的约束求解要求。
3 网络程序模型分析与构建 网络程序模型的组成包括开发者定义的个人函数以及调用的内核API函数。在Windows平台下,网络程序运行的过程中主要调取的是winsock函数库,特别是在XP系统之后,微软已将winsock2作为内核函数库写入了操作系统本身。从最原始的阻塞模型,到之后的select模型、WSAAsycSelect模型、Overlapped模型、IOCP模型,不同程序模型调用winsock库中函数种类以及顺序的不同决定了不同模型下网络程序的运转方式。本文原型系统针对不同网络程序模型开发了针对性执行子模块,基于模型识别的方式对不同模型下的网络程序进行漏洞检测。
3.1 阻塞模型 阻塞模型即最早的一类网络程序模型,该类模型基于Winsock API函数实现服务器和客户端之间的通信。该模型运行过程中采用单线程的方式。在本次连接通信未完成、连接未断开前,新的客户端只能不断地发出连接请求,等待新的连接。当正在进行的服务过程结束、本次连接断开后,服务器端才接受新的连接请求并提供服务。
图 4为阻塞模型下的通信模型及通信过程,通过关键函数抽取的方式本文建立了网络程序的阻塞模型。
图 4 阻塞通信模型 Fig. 4 Blocking communication model |
图选项 |
针对模型中的关键函数进行挂钩,并针对挂钩后函数,定制特殊的执行语义,当系统执行到模型的节点函数时将触发定制的操作,启动符号执行过程。如图 5所示,针对程序运行过程中数据接收、处理的关键函数的调用点和返回点进行挂钩,从而实现针对该模型下网络程序的漏洞检测,提高检测过程和实际程序代码的贴合率。
图 5 阻塞通信模型执行模块部分代码 Fig. 5 Part of execution module code of blocking communication model |
图选项 |
3.2 select模型 select类网络程序是网络程序发展过程中实现的第1种非阻塞网络程序,该类程序基于单进程实现,但其在阻塞类程序的基础上实现了多套接字管理。通过程序分析发现,在该类程序中select函数负责了套接字的申请、分配和调度,因此在模型建立过程中重点对select及其附属函数进行执行监控和漏洞检测。定制select_call_hook()的挂钩语义对readfds(检查可读性)、writefds(检查可写性)、exceptfds(检查错误)等敏感变量进行符号化,通过收集该符号变元在执行过程中的路径约束,监控该变量的传播过程。针对执行过程中涉及权限检查的部分进行重点监控,因为该部分往往是程序代码的高危区域之一。针对select函数执行点进行挂钩如下:
int select
(
??????int nfds,
??????fd_set* readfds,
??????fd_set* writefds,
??????fd_set* exceptfds,
??????const struct timeval* timeout
);
如图 6所示,当有网络事件发生时,socket函数会建立对应的套接字处理接口,select函数会修改对应套接字接口的相关属性,将套接字句柄添加到对应的属性集合之中,从而赋予新的套接字接口新的权限。据此分析,程序代码在该位置存在多次调用和反复的修改,在执行点挂钩的基础上,通过定制select_ret_hook()的挂钩语义,检查select函数的返回值和该值的传递路径,判断是否存在脆弱节点。
图 6 select模型执行过程 Fig. 6 select model execution process |
图选项 |
3.3 IOCP模型 IOCP类程序基于多线程并行处理器完成网络程序客户端的服务请求,该类网络程序运行后会预先创造提供服务的线程池,与在接受请求时创建线程相比效率更高,Apache等高性能商业服务器程序均采用该架构进行开发。通过模型分析发现,在运行过程中,该类网络程序采取两类线程并行的方式:主线程负责监听和创造任务线程,并完成接口关联等操作;任务线程负责处理用户请求,为用户提供服务。任务线程处理请求过程中为接收用户数据申请的缓冲区,该类内存空间操作往往是程序代码存在漏洞的高危区域,需要重点进行程序运行监控和代码分析,具体如下:
……
#define BUFFER_SIZE 1024
typedef struct _PER_HANDLE_DATA
{
?????SOCKET s;
?????sockaddr_in addr;
} PER_HANDLE_DATA, *PPER_HANDLE_DATA;
typedef struct _PER_IO_DATA
{
?????OVERLAPPED ol;
?????char buf[BUFFER_SIZE];
?????int nOperationType;
} PER_IO_DATA, *PPER_IO_DATA;
……
针对该类网络程序进行建模,抽取了从服务连接建立到终止过程中的关键函数,同时作为该模型核心,对GetQueuedCompletionStatus()函数的执行点进行挂钩,并定制特殊的函数执行语义。事件发生后I/O系统会向完成端口对象发送完整消息通知,GetQueuedCompletionStatus()函数会按照顺序优先级的方式读取队列封包,通信过程每一个连接的相关输入和参数见下文代码,此时针对如lpNumberOfBytes等危险区域或变量进行执行监视,则有可能得到触发程序崩溃的漏洞点。
BOOL GetQueuedCompletionStatus
(
HANDLE CompletionPort,
LPDWORD lpNumberOfBytes,
PULONG_PTR lpCompletionKey,
LPOVERLAPPED* lpOverlapped,
DWORD dwMilliseconds
);
4 多模型网络程序漏洞检测系统 本文提出了一种基于程序建模的网络程序漏洞检测技术,并利用该技术实现了一套多模型网络程序漏洞检测系统。系统共分为4个模块:目标模型识别模块、网络程序模型模块、网络程序漏洞检测模块、漏洞记录模块。图 7所示为该原型系统的架构。
图 7 系统原型架构 Fig. 7 System prototype architecture |
图选项 |
检测过程主要分为以下5步:
1) 目标程序传入检测系统后,目标模型识别模块会对目标程序所属的网络程序类型进行判断,并从网络程序模型模块中调用相应模型的子模块。同时,将目标程序传入检测运行环境中(QEMU虚拟机)。
2) 网络程序模型模块会将对应模型子模块的调用信号发送给网络程序漏洞检测模块,同时启动漏洞检测过程。
3) 针对目标程序进行检测,并记录不同路径的约束条件,如果碰到程序崩溃则记录到达对应崩溃点的约束条件集。
4) 将能够到达崩溃点的约束集交给约束求解器进行求解,将结果发送给漏洞记录模块。
5) 漏洞记录模块记录崩溃点的相关信息和导致崩溃的具体输入。
该系统基于S2E框架进行开发,采用了模块化的组成方式,最初版本的系统仅包含阻塞类模型,通过后期开发已经拓展到了4种主流模型。原型系统采用“系统-功能模块-子模块”的三级结构设置。系统会判定程序所属的模型,并根据模型种类调用相应模型的漏洞检测子模块进行漏洞检测过程,调用记录模块对相应的脆弱点进行分类和记录,全系统能够针对目标网络程序实现自动化的漏洞检测过程。
5 实验分析 本文以QEMU虚拟机下WindowsXP-SP3操作系统为测试环境进行实验,实验环境配置如表 1所示。
表 1 实验环境配置 Table 1 Experimental environment configuration
节点 | 操作系统 | 主机型号 | 内存 |
Server | WindowsXP-SP3 | Intel? Core i7-5820 K 3.3 GHz CPU | 4 GB |
Client | WindowsXP-SP3 | Intel? Core i7-5820K 3.3 GHz CPU | 4 GB |
表选项
实验过程分为两部分进行,首先针对每种类型的网络程序编写了较为简单的测试用例,并针对各类测试用例进行试验。实验结果证明原型系统可以稳定运行,并针对不同类型的网络程序进行漏洞检测。
其次,从CVE漏洞库中选择了2个已知漏洞作为实验对象,这2个漏洞均存在于商业化网络程序Tftpd32中,该程序软件基于TCP通信协议开发,能够实现数据文件的发送和接收, 结果如表 2所示。
表 2 实验结果 Table 2 Experimental result
软件 | 漏洞编号 | 漏洞类型 |
Tftpd32 | CVE-2006-6141 | 远程缓冲区溢出漏洞 |
Tftpd32 | CVE-2013-6809 | 格式化字符串漏洞 |
表选项
如图 8所示,通过QEMU监视器可以看到,系统能够识别操作系统版本,并定位到Tftpd32运行过程中需要调用的系统函数,实现对程序调用函数的挂钩和监控。此时,启动客户端程序和服务器端建立连接,并向服务器发送数据。可以发现服务器端接收到网络数据后会触发挂钩函数的语义内容,系统针对本次输入启动选择性符号执行过程。
图 8 实现函数挂钩 Fig. 8 Function hook realization |
图选项 |
如图 9所示,服务器端针对符号执行过程的路径约束进行收集,对分支节点的自身状态进行保存。同时,向客户端发送指令,要求其保存对应执行节点下的状态信息。
图 9 服务器端符号执行过程 Fig. 9 Symbolic execution process of server |
图选项 |
通过客户端的QEMU监视器可以看到以服务器端为中心的漏洞检测过程。通过图 10可看出,系统执行到了服务器端程序某一路径的终点需要回溯到上一分支节点,此时,服务器端通过指令成功使客户端恢复到了相同节点状态。
图 10 客户端状态保存及回置 Fig. 10 Client state savinges and restoringes |
图选项 |
通过稳定的实验测试过程,系统能够检测到针对Tftpd32的2款漏洞。为了验证系统的稳定性,在平台上对测试目标进行了500次重复试验验证,其中464次实验正确探索到了2种程序缺陷所在的执行位置,25次实验探测到了CVE-2006-6141缺陷所在位置,11次执行产生了误报,反馈了无异常点的信息,整体性能较稳定。误报率和漏报率较低。
6 结论 1) 系统针对网络程序各模型的漏洞检测进行了可行性拓展,能够适应现阶段约85%的网络程序目标,针对另外2种模型的适配也在进一步开发之中。
2) 相比于本文中提到的几款漏洞检测系统,本系统对C/S架构下网络程序漏洞检测的针对性更强,代码覆盖率更高,通过对不同模型网络程序的针对性开发,目标区域函数代码的覆盖率可以提高到90%以上。
3) 针对目标程序所属模型的判断虽然增加了系统的开销,但在后期的检测过程中可以提高检测效率和漏洞发现的准确率。
4) STP约束求解器为本系统提供了符号化支撑和求解,该求解器能够针对非浮点数计算类指令进行求解分析。
5) 漏洞信息的记录和导出采取了文本记录的方式,随着实验的推进,实验目标和漏洞信息不断增多,在后期的开发中将结合数据库技术思想添加数据管理模块,对漏洞信息进行数据库管理。
为提高本系统的实用性和检测效果,下一步开发将重点进行网络程序模型的探索和构建,进一步增强该系统的普适性,同时,进行针对大型网络程序软件的检测实验。
参考文献
[1] | 高瑞, 周彩兰, 朱荣. 网络应用程序漏洞挖掘技术研究[J]. 现代电子技术, 2018, 41(3): 115-119. GAO R, ZHOU C L, ZHU R. Research on vulnerability mining technology of network application program[J]. Modern Electronics Technique, 2018, 41(3): 115-119. (in Chinese) |
[2] | 刘红梅. 基于C/S和B/S体系结构应用系统的开发方法[J]. 计算机与现代化, 2007(11): 52-54. LIU H M. Development of application system based on C/S and B/S architecture[J]. Computer and Modernization, 2007(11): 52-54. DOI:10.3969/j.issn.1006-2475.2007.11.019 (in Chinese) |
[3] | 薛卫萍, 陈文生. 基于C/S结构的即时通信系统的设计与实现[J]. 信息通信, 2015(3): 113-114. XUE W P, CHEN W S. Design and implementation of real-time communication system based on C/S structure[J]. Information & Communications, 2015(3): 113-114. DOI:10.3969/j.issn.1673-1131.2015.03.076 (in Chinese) |
[4] | 洪学海, 朱彤. 基于C/S体系结构应用系统的研究与开发[J]. 物探化探计算技术, 1999, 21(1): 59-65. HONG X H, ZHU T. Research and development of C/S architecture application system[J]. Computer Techniques for Giophysical and Geochenical Explopation, 1999, 21(1): 59-65. DOI:10.3969/j.issn.1001-1749.1999.01.011 (in Chinese) |
[5] | LI P, MA Z, YANG H, et al. Research and design of power quality account management system based on B/S architecture[J]. Electrical Engineering, 2017(10): 110-114. |
[6] | 金海, 廖小飞. P2P技术原理及应用[J]. 中兴通讯技术, 2007, 13(6): 1-5. JIN H, LIAO X F. Pinciples and application of P2P technology[J]. ZTE Communications, 2007, 13(6): 1-5. DOI:10.3969/j.issn.1009-6868.2007.06.001 (in Chinese) |
[7] | 伊玮珑.基于B/S结构的web漏洞检测系统的设计[D].哈尔滨: 哈尔滨理工大学, 2015. YIN W L.Design of web vulnerabilities detection system based on browser/server structure[D].Harbin: Harbin University of Science & Technology, 2015(in Chinese). |
[8] | 杨丁宁, 肖晖, 张玉清. 基于Fuzzing的ActiveX控件漏洞挖掘技术研究[J]. 计算机研究与发展, 2012, 49(7): 1525-1532. YANG D N, XIAO H, ZHAN Y Q. Vulnerability detection in ActiveX controls based on Fuzzing technology[J]. Journal of Computer Research and Development, 2012, 49(7): 1525-1532. (in Chinese) |
[9] | 吴小伟.基于动态污点分析的网络程序漏洞挖掘方法[D].武汉: 华中科技大学, 2012. WU X W.A network software vulnerabilities discovery method based on dynamic taint analysis[D].Wuhan: Huazhong University of Science and Technology, 2012(in Chinese). |
[10] | 王江.基于QEMU的二进制程序离线动态污点分析方法研究[D].北京: 北京理工大学, 2016. WANG J.Research on offline dynamic taint analysis of binary program based on QEMU[D].Beijing: Beijing Institute of Technology, 2016(in Chinese). |
[11] | 冯震, 聂森, 王轶骏, 等. 基于S2E的Use-After-Free漏洞检测方案[J]. 计算机应用与软件, 2016, 33(4): 273-276. FENG Z, NIE S, WANG Y J, et al. Use-After-Free vulnerabilities detection scheme based on S2E[J]. Computer Applications and Software, 2016, 33(4): 273-276. DOI:10.3969/j.issn.1000-386x.2016.04.064 (in Chinese) |
[12] | CHIPOUNOV V, KUZNETSOV V, CANDEA G. S2E:A platform for in-vivo multi-path analysis of software systems[J]. ACM SIGPLAN Notices, 2011, 47(4): 265-278. |
[13] | CHIPOUNOV V, GEORGESCU V, ZAMFIR C, et al.Selective symbolic execution[C]//The Workshop on Hot Topics in System Dependability, 2009: 1286-1299. |
[14] | CADAR C, SEN K. Symbolic execution for software testing:Three decades later[J]. Communications of the ACM, 2013, 56(2): 82-90. DOI:10.1145/2408776 |
[15] | SONG J S, KIM H, PARK S. Enhancing conformance testing using symbolic execution for network protocols[J]. IEEE Transactions on Reliability, 2015, 64(3): 1024-1037. DOI:10.1109/TR.2015.2443392 |
[16] | PISTOIA M, CHANDRA S, FINK S J, et al. A survey of static analysis methods for identifying security vulnerabilities in software systems[J]. IBM Systems Journal, 2007, 46(2): 265-288. DOI:10.1147/sj.462.0265 |