Method for precisely detecting buffer overflow vulnerabilities in C programs
-
摘要: C程序中的缓冲区溢出漏洞是影响系统安全性的严重问题,利用工具有效地检测并消除出这一漏洞,可以大大提高系统的安全性.针对现有工具在检测缓冲区溢出漏洞上的不足,提出了一种利用模型检测技术对C语言代码中潜在的缓冲区溢出漏洞进行精确检测的新方法.该方法首先将对缓冲区漏洞的检测转化为对程序某个位置可达性的判定,再使用模型检测工具对可达性进行验证.使用这一方法建立了一个精确检测C程序中缓冲区溢出漏洞的原型系统,并使用该原型系统进行了试验.结果表明该方法可以较为精确地检测并定位出代码中的漏洞.Abstract: Buffer overflow (BO) vulnerability in C programs is one of the most crucial threats to the security of a system. Using tools to detect and eliminate this kind of vulnerability in programs will give the system sufficient ability to maintain security environment. For the scarcity of accuracy in detecting BO vulnerabilities, current bug-hunting tools can not precisely detect BO vulnerabilities. A new method was proposed, which uses model checking, to precisely detect potential BO in C programs. This method converts detecting BO vulnerabilities to verifying the reachability of certain position in programs and uses model checking tool to do the verification job. Using this method, a prototype system has been developed and been tested with some benchmarks. The early results show that this method can precisely detect BO vulnerabilities in C programs.
-
Key words:
- buffer overflow /
- security vulnerabilities /
- static analysis /
- model checking
-
[1] Cowan C, Wagle P, Pu C, et al. Buffer overflows: attacks and defenses for the vulnerability of the decade DARPA Information Survivability Conference and Expo (DISCEX). Hilton Head, SC: IEEE Computer Society Press, 2000:154-163 [2] Necula G C, McPeak S, Weimer W. CCured: typesafe retrofitting of legacy code ACM SIGPLAN-SIGACT Conference on the Principles of Programming Languages (POPL). Portland: ACM Press, 2002:128-139 [3] Shankar U, Talwar K, Foster J S, et al. Detecting format string vulnerabilities with type qualifiers Proc of the 10th USENIX Security Symposium, 2001 [4] Zitser M. Securing software: an evaluation of static source code analyzers . Massachusetts: Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2003 [5] Henzinger T A, Jhala R, Majumdar R, et al. Lazy abstraction Proc of the 29th Annual Symp on Principles of Programming Languages (POPL) . New York:ACM, 2002:58-70 [6] Beyer D, Henzinger T A, Jhala R, et al. Checking memory safety with blast Proc of the FASE 2005. LNCS 3442.Heidelberg: Springer-Verlag, 2005,3442:2-18
点击查看大图
计量
- 文章访问数: 2587
- HTML全文浏览量: 153
- PDF下载量: 2305
- 被引次数: 0