基于符号执行的二进制代码漏洞发现  

Vulnerability Finding Using Symbolic Execution on Binary Programs

作　　者：牛伟纳[1] 丁雪峰[2] 刘智[1] 张小松[1] 

机构地区：[1]电子科技大学计算机科学与工程学院,成都611731 [2]四川大学信息管理中心,成都610065

出　　处：《计算机科学》2013年第10期119-121,138,共4页Computer Science

基　　金：四川省科技计划支撑项目(2012GZ0001);上海市科研计划项目(11511505300)资助

摘　　要：软件漏洞是安全问题的根源之一,fuzzing(模糊测试)是目前漏洞发现的关键技术,但是它通过随机改变输入无法有效地构造出测试用例,也无法消除测试用例的冗余性。为了克服传统fuzzing测试的缺点、有效生成测试输入且无需分析输入格式,针对二进制程序设计并实现了基于符号执行的漏洞发现系统SEVE。将程序的输入符号化,利用动态插桩工具建立符号变量的传播关系;在分支语句处收集路径约束条件,最后用解析器求解之并将其作为新的测试用例。用mp3和pdf软件进行了实验,结果表明,该系统有效地提高了漏洞发现的效率与自动化程度。Software vulnerability is one main source of computer safety issues, and the key technology of vulnerabilities finding is fuzzing（fuzzy test）which is based on randomly changing the input, however, it cannot construct test cases ef- fectively and eliminate the redundancy of test cases. In order to overcome the shortcomings of traditional fuzzing test, ef- fectively generate test inputs and do not need to analyze the input format, we designed and implemented vulnerability found system（called SEVE）based on symbolic execution for binary program. SEVE makes the inputs symbolic and uses dynamic instrumentation tools to establish the propagation relationship of the symbolic variable, collect path constraints in branch statement, uses interpreter to solve these path constraints to obtain test cases. Experimental results which are based on rap3 and pdf software show that the system can improve the efficiency and the degree of automation of vulner-ability discovery.

关 键 词：漏洞 二进制程序 符号执行 插桩 路径约束 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]