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

Abstract: 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.

Key words: integer overflow, field-sensitive flow-sensitive pointer analysis, taint analysis, static symbolic execution