CSSV: towards a realistic tool for statically detecting all buffer overflows in C

ABSTRACT

Erroneous string manipulations are a major source of software defects in C programs yielding vulnerabilities which are exploited by software viruses. We present C String Static Verifyer (CSSV), a tool that statically uncovers all string manipulation errors. Being a conservative tool, it reports all such errors at the expense of sometimes generating false alarms. Fortunately, only a small number of false alarms are reported, thereby proving that statically reducing software vulnerability is achievable. CSSV handles large programs by analyzing each procedure separately. To this end procedure contracts are allowed which are verified by the tool.We implemented a CSSV prototype and used it to verify the absence of errors in real code from EADS Airbus. When applied to another commonly used string intensive application, CSSV uncovered real bugs with very few false alarms.

REFERENCES

• 1: Todd M. Austin , Scott E. Breach , Gurindar S. Sohi, Efficient detection of all pointer and array access errors, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.290-301, June 20-24, 1994, Orlando, Florida, United States
• 2: Rastislav Bodík , Rajiv Gupta , Vivek Sarkar, ABCD: eliminating array bounds checks on demand, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.321-333, June 18-21, 2000, Vancouver, British Columbia, Canada
• 3: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 4: Brian Chess, Improving Computer Security Using Extended Static Checking, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.160, May 12-15, 2002
• 5: Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
• 6: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 7: C. Cowan, P. Wagle, C. Pu, S. Beattie, and J. Walpole. Buffer overflows: attacks and defenses for the vulnerability of the decade. In In Proc. of the DARPA Information Survivability Conference and Expo, 1999.
• 8: Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada
• 9: Manuvir Das , Ben Liblit , Manuel Fähndrich , Jakob Rehof, Estimating the Impact of Scalable Pointer Analysis on Optimization, Proceedings of the 8th International Symposium on Static Analysis, p.260-278, July 16-18, 2001
• 10: Alain Deutsch, Interprocedural may-alias analysis for pointers: beyond k-limiting, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.230-241, June 20-24, 1994, Orlando, Florida, United States
• 11: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 12: N. Dor. Statically Detecting All Buffer Overflows in C. PhD thesis, Univ. of Tel-Aviv, Israel, 2003. In preparation.
• 13: Nurit Dor , Michael Rodeh , Shmuel Sagiv, Cleanness Checking of String Manipulations in C Programs via Integer Analysis, Proceedings of the 8th International Symposium on Static Analysis, p.194-212, July 16-18, 2001
• 14: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 15: Rakesh Ghiya , Daniel Lavery , David Sehr, On the importance of points-to analysis and other memory disambiguation methods for C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.47-58, June 2001, Snowbird, Utah, United States
• 16: N. Halbwachs. Static Analysis of Linear Properties Invariantly Satisfied by the Numeric Variables of a program. PhD thesis, Grenoble University, 1979.
• 17: Nicolas Halbwachs , Yann-Erick Proy , Patrick Roumanoff, Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, v.11 n.2, p.157-185, Aug. 1997 [doi>10.1023/A:1008678014487 ]
• 18: Nevin Heintze , Olivier Tardieu, Ultra-fast aliasing analysis using CLA: a million lines of C code in a second, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.254-263, June 2001, Snowbird, Utah, United States
• 19: B. Jeannet. New polka library. Available at "http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html".
• 20: Brian W. Kernighan , Dennis M. Ritchie, The C programming language, Prentice Hall Press, Upper Saddle River, NJ, 1989
• 21: Priyadarshan Kolte , Michael Wolfe, Elimination of redundant array subscript range checks, ACM SIGPLAN Notices, v.30 n.6, p.270-278, June 1995
• 22: William Alexander Landi, Interprocedural aliasing in the presence of pointers, Rutgers University, New Brunswick, NJ, 1992
• 23: D. Larochelle and D. Evans. Statically detecting likely buffer overflow vulnerabilities. In 10th USENIX Security Symposium, 2001.
• 24: Gary T. Leavens , Albert L. Baker, Enhancing the Pre- and Postcondition Technique for More Expressive Specifications, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, p.1087-1106, September 20-24, 1999
• 25: Donglin Liang , Mary Jean Harrold, Efficient Computation of Parameterized Pointer Information for Interprocedural Analyses, Proceedings of the 8th International Symposium on Static Analysis, p.279-298, July 16-18, 2001
• 26: Alexey Loginov , Suan Hsi Yong , Susan Horwitz , Thomas W. Reps, Debugging via Run-Time Type Checking, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.217-232, April 02-06, 2001
• 27: Thomas J. Marlowe , Barbara G. Ryder, An efficient hybrid algorithm for incremental data flow analysis, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-196, December 1989, San Francisco, California, United States [doi>10.1145/96709.96728]
• 28: B. Miller, D. Koski, C. Lee, V. Maganty, R. Murthy, A. Natarajan, and J. Steidl. Fuzz revisited: A re-examination of the reliability of Unix utilities and services, 1995. Available at http://www.cs.wisc.edu/˜bart/fuzz/fuzz.html.
• 29: Carroll Morgan, Programming from specifications, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 30: Eugene M. Myers, A precise inter-procedural data flow algorithm, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.219-230, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567556]
• 31: Inc. Rational. Purify software. Available at "http://www.rational.com", 1995.
• 32: Microsoft Research. AST-toolkit. 2002.
• 33: Radu Rugina , Martin Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.182-195, June 18-21, 2000, Vancouver, British Columbia, Canada
• 34: Barbara G. Ryder , William A. Landi , Philip A. Stocks , Sean Zhang , Rita Altucher, A schema for interprocedural modification side-effect analysis with pointer aliasing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.2, p.105-186, March 2001 [doi>10.1145/383043.381532]
• 35: A. Simon and A. King. Analyzing string buffers in c. In International Conference on Algebraic Methodology and Software Technology, 2000.
• 36: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 37: D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Symp. on Network and Distributed Systems Security, 2000.
• 38: G. Yorsh. CoreC: A Simplifier for C, 2002. http://www.cs.tau.ac.il/˜gretay/GFC.htm.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability; Validation

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions; Assertions
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis; Operational semantics

General Terms:
Algorithms, Experimentation, Languages, Reliability, Security, Verification

Keywords:
abstract interpretation, buffer overflow, contracts, error detection, static analysis