一种面向源代码的整数溢出缺陷静态检测方法  

A source code oriented static detection method for integer overflow defects

作　　者：黄晖[1] 陆余良[1] 刘林涛[1] 赵军[1] 

机构地区：[1]解放军电子工程学院,安徽合肥230037

出　　处：《中国科学技术大学学报》2015年第7期601-607,共7页JUSTC

摘　　要：受限于不完备的函数调用图分析和路径可达性分析,当前静态整数溢出检测工具存在较为严重的误报情况.为解决这一问题,以源代码中外部输入可控的整数溢出缺陷的自动挖掘为目标,给出一种综合调用图分析、静态污点分析和静态符号执行的检测方法.提出一种域敏感的流敏感指针分析方法构建目标程序调用图的"高估计",应用静态污点-sink传播分析确定潜在的外部输入可控的整数溢出缺陷程序点,最后应用静态符号执行技术通过判定缺陷约束的可满足性对误报情况进行约减.实验验证了方法在实际整数溢出缺陷检测和误报情况约减方面的应用有效性.Limited by incomplete call graph analysis and path feasibility analysis ,current static integer overflow defect detection methods generally return results with high false positives . To reduce this inefficiency ,aiming at automatic exploration of the external input triggering integer overflow defects ,a new source code oriented detection method was proposed combining call graph analysis , static taint analysis and static symbolic execution ,in which a field‐sensitive and flow‐sensitive pointer analysis method was proposed for constructing an over‐approximation of the target program’s real call graph ,with a static taint‐sink propagation analysis carried out for calculating the potential external input reachable integer overflow defects , on which flow‐sensitive static symbolic execution is conducted to reduce the false positives introduced by the detection system through justifying the satisfiability of the corresponding defect constraint . Experiments prove the effectiveness of the methodin real‐world integer overflow defect detection and false alarm reduction .

关 键 词：整数溢出 域敏感流敏感指针分析 污点分析 静态符号执行 

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