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

False Positive Elimination in Static Defect Detection

作　　者：赵云山[1] 宫云战[1] 周傲[1] 王前[1] 周虹伯[1] 

机构地区：[1]北京邮电大学网络与交换技术国家重点实验室,北京100876

出　　处：《计算机研究与发展》2012年第9期1822-1831,共10页Journal of Computer Research and Development

基　　金：国家"八六三"高技术研究发展计划基金项目(2012AA010101;2009AA012404);国家自然科学基金项目(91018002)

摘　　要：误报率是衡量静态缺陷检测工具的重要指标.在对比分析了各种误报消除技术的基础上,提出了一种前向数据流分析结合逆向约束搜索技术的误报消除方法:前向数据流分析的保守数据流解可以用于缺陷状态迭代,并得到初始的缺陷检测结果;根据缺陷发生处的数据流特征,逆向搜索可能导致缺陷发生的约束条件,该约束条件可以作为通用约束求解器的输入判断缺陷的可满足性,从而对初始的缺陷检测结果进行精化.同时,在数据流分析过程中引入符号执行技术,不仅提高了数据流分析的精度,且便于约束表示及转化,提高了约束搜索的效率.对SPECCPU2000中11个工程的对比实验表明,前向数据流分析与逆向约束搜索相结合的误报消除方法在增加了有限开销的同时有效地消除了部分误报,且与同类工具相比具有更好的可扩展性.False positive ratio is a key factor for measuring the performance of static defect detection tools. Based on the analysis of a series of false positive elimination techniques, we put forward a defect detection method which combines the strength of forward dataflow analysis and backward constraint query techniques. The forward dataflow analysis generates a conservative dataflow solution, which could help reporting an initial defect detection result. According to the dataflow feature of the initial defect location, by querying the potential constraints that might cause defects, the satisfiability of the initial defects could be determined by the collection of queried constraints, with the help of a general purpose constraint solver. So the initial ＂coarse granularity＂ detection result is refined. In addition, introducing the symbolic execution technique during dataflow analysis not only improves the precision of dataflow analysis, but also facilitates the constraint representation and betters the constraint querying efficiency. The comparative experiments on 11 benchmarks from SPEC CPU2000 show that our method efficiently eliminates parts of the false positives with an acceptable overhead increase, and several comparisons between similar tools reveal the scalability of our method.

关 键 词：误报 数据流分析 抽象解释 约束求解 符号执行 

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