Practical and effective symbolic analysis for buffer overflow detection

ABSTRACT

Although buffer overflow detection has been studied for more than 20 years, it is still the most common source of security vulnerabilities in systems code. Different approaches using symbolic analysis have been proposed to detect this vulnerability. However, existing symbolic analysis techniques are either too complex to scale to millions of lines of code (MLOC), or too simple to effectively handle loops and complex program structures.

In this paper, we present a novel symbolic analysis algorithm for buffer overflow detection that applies simple rules to solve relevant control and data dependencies. Our approach is path-sensitive and effectively handles loops and complex program structures. Scalability is achieved by using a simple symbolic value representation, filtering out irrelevant dependencies in symbolic value computation and computing symbolic values on demand.

Evaluation of our approach shows that it is both practical and effective:the analysis runs over 8.6 MLOC of the OpenSolaris^TM Operating system/Networking (ON)codebase in 11 minutes and finds hundreds of buffer overflows with a false positive rate of less than 10%.

References

1. S. Anand, C. S. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to Java pathfinder. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 134--138, Braga, Portugal, March 2007.
2. D. Babic and A. J. Hu. Calysto: scalable and precise extended static checking. In Proceedings of the 30th International Conference on Software Engineering, pages 211--220. ACM Press, 2008.
3. J. Birch, R. van Engelen, K. Gallivan, and Y. Shou. An empirical evaluation of chains of recurrences for array dependence testing. In Proceedings of the 15th international conference on Parallel Architectures and Compilation Techniques, pages 295--304. ACM Press, 2006.
4. W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software--Practice & Experience, 30:775--802, 2000.
5. C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th symposium on Operating Systems Design and Implementation, pages 209--224. USENIX Association, 2008.
6. S. Christey and R. A. Martin. Vulnerability type distributions in CVE. Technical report, The MITRE Corporation, May 2007. Version 1.1.
7. C. Cifuentes, C. Hoermann, N. Keynes, L. Li, S. Long, E. Mealy, M. Mounteney, and B. Scholz. BegBunch: Benchmarking for C bug detection tools. In Proceedings of the 2009 international workshop on Defects in large software systems, July 2009.
8. C. Cifuentes and B. Scholz. Parfait -- designing a scalable bug checker. In Proceedings of the ACM SIGPLAN Static Analysis Workshop, pages 4--11, 12 June 2008.
9. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th symposium on Principles of Programming Languages, pages 238--252. ACM Press, 1977.
10. P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The ASTRÉE analyser. In Proceedings of the 2005 European Symposium on Programming, pages 21--30. Springer, April 2005.
11. R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 13(4):451--490, October 1991.
12. D. Evans and D. Larochelle. Improving security using extensible lightweight static analysis. IEEE Software, pages 42--51, January/February 2002.
13. 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 2002 conference on Programming Language Design and Implementation, pages 234--245. ACM Press, 2002.
14. V. Ganapathy, S. Jha, D. Chandler, D. Melski, and D. Vitek. Buffer overrun detection using linear programming and static analysis. In Proceedings of the 10th conference on Computer and Communications Security, pages 345--354. ACM Press, 2003.
15. B. Hackett, M. Das, D. Wang, and Z. Yang. Modular checking for buffer overflows in the large. In Proceeding of the 28th International Conference on Software Engineering, pages 232--241. ACM Press, 2006.
16. J. C. King. Symbolic execution and program testing. Communications of ACM, 19(7):385--394, 1976.
17. W. Le and M. L. Soffa. Marple: a demand-driven path-sensitive buffer overflow detector. In Proceedings of the 16th international symposium on Foundations of Software Engineering, pages 272--282. ACM Press, 2008.
18. LLVM. Low Level Virtual Machine. http://www.llvm.org, detail on website.
19. LLVM/Clang Static Analyzer. http://clang.llvm.org/StaticAnalysis.html. Last accessed: 1 December 2008.
20. S. Nagarakatte, J. Zhao, M. M. Martin, and S. Zdancewic. Softbound: highly compatible and complete spatial memory safety for C. In Proceedings of the 2009 conference on Programming Language Design and Implementation, pages 245--258. ACM Press, 2009.
21. K. J. Ottenstein, R. A. Ballance, and A. B. MacCabe. The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages. In Proceedings of the 1990 conference on Programming Language Design and Implementation, pages 257--271. ACM Press, 1990.
22. M. Y. Patrice Godefroid and D. Molnar. Automated whitebox fuzz testing. In Proceedings of the 11th Network and Distributed System Security Symposium, pages 159--169, 2008.
23. C. S. Păsăreanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In Proceedings of the International Symposium on Software Testing and Analysis, pages 15--26. ACM Press, 2008.
24. R. Rugina and M. Rinard. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In Proceedings of the 2000 conference on Programming Language Design and Implementation, pages 182--195. ACM Press, 2000.
25. O. Ruwase and M. S. Lam. A practical dynamic buffer overflow detector. In Proceedings of the 11th Network and Distributed System Security Symposium, pages 159--169, 2004.
26. J. Seward and N. Nethercote. Using valgrind to detect undefined value errors with bit-precision. In Proceedings of the annual conference on USENIX Annual Technical Conference, pages 2--2. USENIX Association, 2005.
27. Uno Tool Synopsis. http://spinroot.com/uno/. Last accessed: 26 October 2007.
28. J. Van Meggelen, J. Smith, and L. Madsen. Asterisk: the future of telephony, 2nd edition. O'Reilly, 2007.
29. D. Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of the 7th Network and Distributed System Security Symposium, pages 3--17, 2000.
30. D. A. Wheeler. SLOC Count User Guide. http://www.dwheeler.com/sloccount/. Last accessed: 16 March 2009.
31. Y. Xie and A. Aiken. Saturn: A scalable framework for error detection using boolean satisfiability. ACM Transactions on Programming Languages and Systems, 29(3):16, 2007.
32. Y. Xie, A. Chou, and D. Engler. Archer: using symbolic, path-sensitive analysis to detect memory access errors. In Proceedings of the 11th international symposium on Foundations of Software Engineering, pages 327--336. ACM Press, 2003.

Index Terms

• Computing methodologies

  • Symbolic and algebraic manipulation

• Software and its engineering

  • Software creation and management

    • Software verification and validation

• Theory of computation

  • Models of computation

    • Abstract machines

  • Semantics and reasoning

    • Program reasoning

      • Abstraction