王瑞鹏, 张 旻, 黄 晖, 沈 毅

(国防科技大学电子对抗学院，合肥，230037)

随着信息化程度的不断提高，信息系统被广泛应用于金融、医疗、国防、工控等重要领域。高度信息化带来便利的同时也对网络空间安全提出了更高的要求。漏洞是威胁网络空间安全的重要因素，其中格式化字符串漏洞是一种常见的软件漏洞，它由Tymm Twillman首次发现于1999年[1]，其主要成因是程序未对来自外部的输入内容做出严格过滤，导致格式化控制符参数能够被外部输入所影响[2]，进而对信息系统产生较大威胁。例如CVE-2012-0809漏洞[3]，该漏洞可以提升Linux用户的权限，危害较大。因此对格式化字符串漏洞的挖掘和验证意义十分重大。

现有的自动化漏洞挖掘方法能够挖掘到大量的软件漏洞[4-8]，但不能对产生漏洞的可利用性进行验证。因此，漏洞自动验证技术在近些年成为了软件安全领域的一个研究热点。在漏洞自动验证领域，符号执行技术的准确性和可靠性使其成为自动化程序分析的重要工具。目前基于符号执行的自动化漏洞自动验证系统有很多，如AEG[9]、Mayhem[10]、CRAX[11]等，其中AEG系统利用到了源码信息，其余系统都在二进制程序层面对漏洞进行自动验证。上述的系统都期望解决通用的漏洞自动验证，其漏洞验证模型中包含针对多种不同漏洞类型的验证方式，同时存在很多文献[12～17]针对特定漏洞或特定的漏洞验证方法，如黄钊等人的FSVDTG[12]主要针对格式化字符串漏洞进行漏洞验证方法研究，方皓[13]等人主要针对Return-to-dl-resolve漏洞验证方法进行研究。……