基于目标制导符号执行的静态缓冲区溢出警报自动确认技术

• 作者: 周严 李宣东 李游 王林章 高凤娟 鲍铁匀
• 来源期刊: 信息安全学报
• 学科: 工学
• 关键词: 符号执行 缓冲区溢出 警报确认 目标制导
• 年，卷（期）: 2016,（2）
• 页码范围: 46-60
• 页数: 15页
• 分类号: TP309.1
• 字数: 14879字
• 语种: 中文
• DOI: 10.19363/j.cnki.cn10-1380/tn.2016.02.005

摘要

缓冲区溢出漏洞是一类严重的安全性缺陷。目前存在动态测试和静态分析技术来检测缓冲区溢出缺陷：动态测试技术的有效性取决于测试用例的设计,而且往往会引入执行开销；静态分析技术及自动化工具已经被广泛运用于缓冲区溢出缺陷检测中,然而静态分析由于采取了保守的策略,其结果往往包含数量巨大的误报,需要通过进一步人工确认来甄别误报,但人工确认静态分析的结果耗时且容易出错,严重限制了静态分析技术的实用性。符号执行技术使用符号代替实际输入,能系统地探索程序的状态空间并生成高覆盖度的测试用例。本文提出一种基于目标制导符号执行的静态缓冲区溢出警报确认方法,使用静态分析工具的输出结果作为目标,制导符号执行确认警报。我们的方法分为3步：首先在过程间控制流图中检测静态分析警报路径片段的可达性,并将可达的警报路径片段集合映射为用于确认的完整确认路径集合；其次在符号执行中通过修剪与溢出缺陷疑似语句无关的路径,指导符号执行沿特定确认路径执行；最后在溢出缺陷疑似语句收集路径约束并加入溢出条件,通过约束求解的结果,对静态分析的警报进行分类。基于上述方法我们实现了原型工具 BOVTool,实验结果表明在实际开源程序上BOVTool能够代替人工减少检查59.9%的缓冲区溢出误报。