| 摘要: |
| 缓冲区溢出漏洞是一类严重的安全性缺陷。目前存在动态测试和静态分析技术来检测缓冲区溢出缺陷:动态测试技术的有效性取决于测试用例的设计,而且往往会引入执行开销;静态分析技术及自动化工具已经被广泛运用于缓冲区溢出缺陷检测中,然而静态分析由于采取了保守的策略,其结果往往包含数量巨大的误报,需要通过进一步人工确认来甄别误报,但人工确认静态分析的结果耗时且容易出错,严重限制了静态分析技术的实用性。符号执行技术使用符号代替实际输入,能系统地探索程序的状态空间并生成高覆盖度的测试用例。本文提出一种基于目标制导符号执行的静态缓冲区溢出警报确认方法,使用静态分析工具的输出结果作为目标,制导符号执行确认警报。我们的方法分为3步:首先在过程间控制流图中检测静态分析警报路径片段的可达性,并将可达的警报路径片段集合映射为用于确认的完整确认路径集合;其次在符号执行中通过修剪与溢出缺陷疑似语句无关的路径,指导符号执行沿特定确认路径执行;最后在溢出缺陷疑似语句收集路径约束并加入溢出条件,通过约束求解的结果,对静态分析的警报进行分类。基于上述方法我们实现了原型工具BOVTool,实验结果表明在实际开源程序上BOVTool能够代替人工减少检查59.9%的缓冲区溢出误报。 |
| 关键词: 符号执行 缓冲区溢出 警报确认 目标制导 |
| DOI：10.19363/j.cnki.cn10-1380/tn.2016.02.005 |
| 投稿时间：2015-11-22修订日期：2015-12-23 |
| 基金项目:本课题得到国家自然科学基金(Nos.91318301,61321491,61472179)资助。 |
|
| Automatically Validating Static Buffer Overflow Warnings based on Guided Symbolic Execution |
| BAO Tieyun,GAO Fengjuan,ZHOU Yan,LI You,WANG Linzhang,LI Xuandong |
| State Key Laboratory of Novel Computer Software Technology, Nanjing University, Nanjing 210023, China;Jiangsu Novel Software Technology and Industrialization, Nanjing 210023, China;Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China |
| Abstract: |
| Buffer overflow vulnerability is a kind of serious security defect. Currently there are dynamic and static approaches to detect buffer overflow. The effectiveness of Dynamic tools depends on design of test case, and they often introduce execution overhead. Static program analysis techniques have been widely used in buffer overflow detection, which often report a large number of false warnings. Manual validating the results of static analysis is time consuming and error- prone, which severely limits the usefulness of static analysis tools. Symbolic execution is a promising software testing and analysis technology, which systematically explore execution space of test program and generates test cases with high coverage. In this paper we propose a novel approach for automatic buffer overflow warnings validating based on symbolic execution.Our approach is consist of three steps:firstly detect the reachability of statements in static analysis path segment in inter procedural control flow graph and map the static path segment sets to complete path sets which are used to be validated; secondly guide the symbolic execution so that we only focus on the execution paths that cover the buffer overflow warnings generated by static program analysis through pruning useless path; finally construct warning path constraints according to buffer overflow vulnerability models at suspicios statements and classify results depend on the output of constraint solver. Based on the proposed technique we implemented a prototype tool BOVTool and our experimental results on real open source programs show that the percentage of false warnings which do not need to be manually validated is 59.9% on average. |
| Key words: symbolic execution buffer overflow warning validating target guided |
