静态缺陷检测中的误报消除技术研究

作者：赵云山; 宫云战; 周傲; 王前; 周虹伯

来源：Z201209003, 2012, (09): 1822-1831.

• 误报
• 数据流分析
• 抽象解释
• 约束求解
• 符号执行 false positive
• dataflow analysis
• Abstract interpretation
• constraint solving
• symbolic execution

误报率是衡量静态缺陷检测工具的重要指标.在对比分析了各种误报消除技术的基础上,提出了一种前向数据流分析结合逆向约束搜索技术的误报消除方法:前向数据流分析的保守数据流解可以用于缺陷状态迭代,并得到初始的缺陷检测结果;根据缺陷发生处的数据流特征,逆向搜索可能导致缺陷发生的约束条件,该约束条件可以作为通用约束求解器的输入判断缺陷的可满足性,从而对初始的缺陷检测结果进行精化.同时,在数据流分析过程中引入符号执行技术,不仅提高了数据流分析的精度,且便于约束表示及转化,提高了约束搜索的效率.对SPECCPU2000中11个工程的对比实验表明,前向数据流分析与逆向约束搜索相结合的误报消除方法在增加了有限开销...

• 单位
  网络与交换技术国家重点实验室; 北京邮电大学