Yichen Xie
ABSTRACT
Memory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both variables and memory sizes. It evaluates known values using a constraint solver at every array access, pointer dereference, or call to a function that expects a size parameter. Accesses that violate constraints are flagged as errors. Those that are exploitable by malicious attackers are marked as security holes.Memory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both variables and memory sizes. It evaluates known values using a constraint solver at every array access, pointer dereference, or call to a function that expects a size parameter. Accesses that violate constraints are flagged as errors. Those that are exploitable by malicious attackers are marked as security holes.We carefully designed ARCHER to work well on large bodies of source code. It requires no annotations to use (though it can use them). Its solver has been built to be powerful in the ways that real code requires, while backing off on the places that were irrelevant. Selective power allows it to gain efficiency while avoiding classes of false positives that arise when a complex analysis interacts badly with statically undecidable program properties. ARCHER uses statistical code analysis to automatically infer the set of functions that it should track --- this inference serves as a robust guard against omissions, especially in large systems which can have hundreds of such functions.In practice ARCHER is effective: it finds many errors; its analysis scales to systems of millions of lines of code and the average false positive rate of our results is below 35%. We have run ARCHER over several large open source software projects --- such as Linux, OpenBSD, Sendmail, and PostgreSQL --- and have found errors in all of them (118 in the case of Linux, including 21 security holes).
- K.Ashcraft and D. R. Engler. Using programmer-written compiler extensions to catch security holes. In IEEE Symposium on Security and Privacy Oakland, California, May 2002.]] Google Scholar
Digital Library
- R. Bodik, R. Gupta, and V. Sarkar. ABCD: Eliminating array bounds checks on demand. In SIGPLAN Conference on Programming Language Design and Implementation pages 321--333, June 2000.]] Google ScholarDigital Library
- W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software: Practice and Experience 30(7):775--802, June 2000.]] Google ScholarDigital Library
- B. Chess. Improving computer security using extended static checking. In IEEE Symposium on Security and Privacy Oakland, California, May 2002.]] Google ScholarDigital Library
- Microsoft Corporation. AST Toolkit. http://research.microsoft.com/sbt/.]]Google Scholar
- N. Dor, M. Rodeh, and M. Sagiv. CSSV: towards a realistic tool for statically detecting all buffer overflows in c. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation pages 155--167. ACM Press, June 2003.]] Google ScholarDigital Library
- D. R. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of Operating Systems Design and Implementation (OSDI), September 2000.]] Google ScholarDigital Library
- D. R. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as deviant behavior: A general approach to inferring errors in systems code. In Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles 2001.]] Google ScholarDigital Library
- C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In Symposium of Formal Methods Europe pages 500--517, March 2001.]] Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation pages 234--245. ACM Press, 2002.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Proceedings of the 29th Annual Symposium on Principles of Programming Languages, June 2002.]] Google ScholarDigital Library
- D. Freedman, R. Pisani, and R. Purves. Statistics WW Norton & Co., third edition, September 1997.]]Google Scholar
- S. Hallem, B. Chelf, Y. Xie, and D. R. Engler. A system and language for building system-specific, static analyses. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation Berlin, Germany, June 2002.]] Google ScholarDigital Library
- R. Hastings and B. Joyce. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Winter USENIX Conference, December 1992.]]Google Scholar
- Intrinsa. A technical introduction to PREfix/Enterprise. Technical report, Intrinsa Corporation, 1998.]]Google Scholar
- R. W. M. Jones and P. H. J. Kelly. Backwards-compatible bounds checking for arrays and pointers in C programs. In Automated and Algorithmic Debugging pages 13--26, May 1997.]]Google Scholar
- W. Landi, B. G. Ryder, and S. Zhang. Interprocedural modification side effect analysis with pointer aliasing. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, pages 56--67. ACM Press, 1993.]] Google ScholarDigital Library
- D. Larochelle and D. Evans. Statically detecting likely buffer overflow vulnerabilities. In 10th USENIX Security Symposium, August 2001.]] Google ScholarDigital Library
- G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of c programs. In International Conference on Compiler Construction, March 2002.]] Google ScholarDigital Library
- G. C. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. In Symposium on Principles of Programming Languages, pages 128--139, January 2002.]] Google ScholarDigital Library
- W. Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. In Supercomputing, pages 4--13, November 1991.]] Google ScholarDigital Library
- B. Schneier. Risks to cybersecurity. Congressional Testimony by Federal Document Clearing House, June 2003.]]Google Scholar
- M. N. Velev and R. E. Bryant. Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. Journal of Symbolic Computation, special issue on Integration of Automated Reasoning and Computer Algebra Systems, 2002.]] Google ScholarDigital Library
- D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In The 2000 Network and Distributed Systems Security Conference. San Diego, CA, February 2000.]]Google Scholar
Index Terms
- ARCHER: using symbolic, path-sensitive analysis to detect memory access errors
Recommendations
ARCHER: using symbolic, path-sensitive analysis to detect memory access errors
Memory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both ...
Protecting C programs from attacks via invalid pointer dereferences
Writes via unchecked pointer dereferences rank high among vulnerabilities most often exploited by malicious code. The most common attacks use an unchecked string copy to cause a buffer overrun, thereby overwriting the return address in the function's ...
Protecting C programs from attacks via invalid pointer dereferences
ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineeringWrites via unchecked pointer dereferences rank high among vulnerabilities most often exploited by malicious code. The most common attacks use an unchecked string copy to cause a buffer overrun, thereby overwriting the return address in the function's ...
Comments