收稿日期: 2009-03-31
修回日期: 2009-06-09
网络出版日期: 2010-01-15
Detection method for memory overrun in multi-loop programs
Received date: 2009-03-31
Revised date: 2009-06-09
Online published: 2010-01-15
王嘉捷 , 蒋凡 , 张涛 . 一种多重循环程序内存访问越界检测方法[J]. 中国科学院大学学报, 2010 , 27(1) : 117 -126 . DOI: 10.7523/j.issn.2095-6134.2010.1.015
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.
[1] Larochelle D, Evans D. Statically detecting likely buffer overflow vulnerabilities //Proceedings of 10th conference on USENIX Security Symposium. 2001.
[2] Godefroid P, Klarlund N, Sen K. DART: Directed automated random testing //ACM Sigplan Notices. 2005, 40: 213-223.
[3] Sen K, Agha G. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools //Proceedings of Conference on Computer Aided Verification. 2006, 4144: 419- 423.
[4] Cadar C, Ganesh V, Pawlowski P, et al. EXE: Automatically generating inputs of death
[J]. ACM Transactions on Information and System Security, 2008,12: 1-38.
[5] Horwitz S, Reps T. The use of program dependence graphs in software engineering //Proceedings of International Conference on Software Engineering. 1992: 392- 411.
[6] Van Engelen R. The CR# algebra and its application in loop analysis and optimization . Technical Report TR- 041223. Department of Computer Science, Florida State University, 2004.
[7] Van Engelen R, Birch J, Shou Y, et al. A unified framework for nonlinear dependence testing and symbolic analysis //Proceedings of the ACM International Conference on Supercomputing (ICS). 2004: 106-115.
[8] Cytron R, Ferrante J, Rosen B, et al. An efficient method of computing static single assignment form //Proceedings of 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1989.
[9] Microsoft Research. Microsoft Phoenix Academic Program . . http://research.microsoft.com/phoenix/
[10] Microsoft Research. Z3: New High-performance Theorem Prover . . http://research.microsoft.com/projects/z3/
[11] Sourceforge. Cppcheck: A tool for static C/C+ + code analysis . . http://cppcheck.wiki.sourceforge.net/
/
| 〈 |
|
〉 |
