关键词: 软件缺陷检测, 静态分析, 符号执行, 循环分析, 递推链扩展代数

Abstract:

A detection method for memory overrun is presented to overcome multi-loop problems: (1)identifies suspicious defects and their dependent regions; (2)analyzes multi-loops by CR# algebra; (3)infers probability of triggering defect and path guide information; (4)detects defects based on symbolic execution; and (5)finds defects, trigger paths, and program input. A prototype tool has been implemented, and it found real defects in several open source softwares. The results show that the new method can avoid blind path traversal while preserving path-sensitive and bit-level detection precision, and improve efficiency and veracity of defect detection.

Key words: software defect detection, static analysis, symbolic execution, loop analysis, CR# algebra