CSSV

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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.