Marple: a demand-driven path-sensitive buffer overflow detector

ABSTRACT

Despite increasing efforts in detecting and managing software security vulnerabilities, the number of security attacks is still rising every year. As software becomes more complex, security vulnerabilities are more easily introduced into a system and more difficult to eliminate. Even though buffer overflow detection has been studied for more than 20 years, it is still the most commonly exploited vulnerability. In this paper, we develop a static analyzer for detecting and helping diagnose buffer overflows with the key idea of categorizing program paths as they relate to vulnerability. We combine path-sensitivity with a demand-driven analysis for precision and scalability. We first develop a vulnerability model for buffer overflow and then use the model in the development of the demand-driven path-sensitive analyzer. We detect and identify categories of paths including infeasible, safe, vulnerable, overflow-input-independent and don't-know. The categorization enables priorities to be set when searching for root causes of vulnerable paths. We implemented our analyzer, Marple, and compared its performance with existing tools. Our experiments show that Marple is able to detect buffer overflows that other tools cannot, and being path-sensitive with prioritization, Marple produces only 1 false positive out of 72 reported overflows. We also show that Marple scales to 570,000 lines of code, the largest benchmark we had.

REFERENCES

• 1: Personal communication with John Lin from Microsoft.
• 2: Polyspace. http://www.polyspace.com.
• 3: T. Ball and J. R. Larus. Program flow path. Microsoft Technical Report MSR-TR-99-01, 1999.
• 4: Rastislav Bodík , Rajiv Gupta , Mary Lou Soffa, Refining data flow information using infeasible paths, Proceedings of the 6th European SOFTWARE ENGINEERING conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.361-377, September 22-25, 1997, Zurich, Switzerland
• 5: W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software: Practice and Experience, 2000.
• 6: CERT. http://www.cert.org/.
• 7: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 8: Evelyn Duesterwald , Rajiv Gupta , Mary Lou Soffa, A demand-driven analyzer for data flow testing at the integration level, Proceedings of the 18th international conference on Software engineering, p.575-584, March 25-29, 1996, Berlin, Germany
• 9: Evelyn Duesterwald , Rajiv Gupta , Mary Lou Soffa, A practical framework for demand-driven interprocedural data flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.6, p.992-1030, Nov. 1997 [doi>10.1145/267959.269970]
• 10: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 11: Brian Hackett , Manuvir Das , Daniel Wang , Zhe Yang, Modular checking for buffer overflows in the large, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134319]
• 12: Y. Hamadi. Disolver: A Distributed Constraint Solver. Technical Report MSR-TR-2003-91, Microsoft Research.
• 13: Nevin Heintze , Olivier Tardieu, Demand-driven pointer analysis, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.24-34, June 2001, Snowbird, Utah, United States
• 14: Wei Le , Mary Lou Soffa, Refining buffer overflow detection via demand-driven path-sensitive analysis, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.63-68, June 13-14, 2007, San Diego, California, USA [doi>10.1145/1251535.1251546]
• 15: V. Benjamin Livshits , Monica S. Lam, Tracking pointers with path and context sensitivity for bug detection in C programs, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 16: S. Lu, Z. Li, F. Qin, L. Tan, P. Zhou, and Y. Zhou. Bugbench: Benchmarks for evaluating bug detection tools. In Proceedings of Workshop on the Evaluation of Software Defect Detection Tools, 2005.
• 17: Microsoft Game Studio MechCommander2. http://www.microsoft.com/games/mechcommander2/.
• 18: Microsoft Phoenix. http://research.microsoft.com/phoenix/.
• 19: Microsoft Prefast. http://www.microsoft.com/whdc/devtools/tools/prefast.mspx.
• 20: M. Orlovich and R. Rugina. Memory leak analysis by contradiction. In Static Analysis, 13th International Symposium, 2006.
• 21: SecurityTeam. http://www.securiteam.com/.
• 22: E. Spafford. A failure to learn from the past. http://citeseer.ist.psu.edu/spafford03failure.html.
• 23: D. Wagner, J. S. Foster, and E. A. B. hand Alexander Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of Network and Distributed System Security Symposium, 2000.
• 24: Yichen Xie , Andy Chou , Dawson Engler, ARCHER: using symbolic, path-sensitive analysis to detect memory access errors, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 25: Misha Zitser , Richard Lippmann , Tim Leek, Testing static analysis tools using exploitable buffer overflows from open source code, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Algorithms, Experimentation, Security, Verification