Abstract
All practical C programs use structures, arrays, and/or strings. At runtime, such objects are mapped into consecutive memory locations, hereafter referred to as buffers. Many software defects are caused by buffer overflow — unintentional access to memory outside the intended object. String manipulation is a major source of such defects. According to the FUZZ study, they are the cause of most UNIX failures.
We present a new algorithm for statically detecting buffer overflow defects caused by string manipulations in C programs. In many programs, our algorithm is capable of precisely handling destructive memory updates, even in the presence of overlapping pointer variables which reference the same buffer at different offsets. Thus, our algorithm can uncover defects which go undetected by previous works. We reduce the problem of checking string manipulation to that of analyzing integer variables.
A prototype of the algorithm has been implemented and applied to statically uncover defects in real C applications, i.e., errors which occur on some inputs to the program. The applications were selected without a priori knowledge of the number of string manipulation errors. A significant number of string manipulation errors were found in every application, further indicating the extensiveness of such errors. We are encouraged by the fact that our algorithm reports very few false alarms, i.e., warnings on errors that never occur at runtime.
This research was supported by a grant from the Ministry of Science, Israel and by the RTD project IST-1999-20527 “DAEDALUS” of the European FP5 programme.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
T. Austin, S. Breach, and G. Sohi. Efficient detection of all pointer and array access errors. In SIGPLAN Conf. on Prog. Lang. Design and Impl., 1994.
Compaq Systems Research Center. Compaq extended static checker for Java. Available at http://research.compaq.com/SRC/esc/, 2000.
P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. 2nd. Int. Symp on Programming, Paris, Apr. 1976.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Symp. on Princ. of Prog. Lang., pages 238–252, New York, NY, 1977. ACM Press.
P. Cousot and N. Halbwachs. Automatic discovery of linear constraints among variables of a program. In ACM Symp. on Princ. of Prog. Lang., 1978.
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.
Edison Design Group. C++ front end. Available at http://www.edg.com/.
N. Halbwachs, Y. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.
B. Jeannet. New polka library. Available at http://www-verimag.imag.fr/~bjeannet/newpolka-english.html.
B. W. Kernighan and D. M. Ritchie. The C programming language. Prentice-Hall, Englewood Cliffs, NJ 07632, USA, 1988.
D. Larochelle and D. Evans. Statically detecting likely buffer overflow vulnerabilities. In To appear in 10th USENIX Security Symposium, 2001.
A. Loginov, S. Yong, S. Horwitz, and T. Reps. Debugging via run-time type checking. In Proc. of Fundamental Approaches to Softw. Eng. (FASE), 2001.
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.
Rational Inc. Purify software. Available at http://www.purify.com, 1995.
Reliable Systems. Icontract-design by contract. Available at http://www.reliable-systems.com/, 1999.
E. Spafford. The internet worm: Crisis and aftermath. In Communications of the ACM, June 1989. 165, pages 678–687, June 1989.
SUIF. Suif compiler system. Available at http://suif.stanford.edu/.
D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Symposium on Network and Distributed Systems Security (NDSS’00) San Diego, CA, Feb. 2000.
D. Weise. Personal communication. Nov. 2000.
S. Yong, S. Horwitz, and T. Reps. Pointer analysis for programs with structures and casting. In SIGPLAN Conf. on Prog. Lang. Design and Impl., 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dor, N., Rodeh, M., Sagiv, M. (2001). Cleanness Checking of String Manipulations in C Programs via Integer Analysis. In: Cousot, P. (eds) Static Analysis. SAS 2001. Lecture Notes in Computer Science, vol 2126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47764-0_12
Download citation
DOI: https://doi.org/10.1007/3-540-47764-0_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42314-0
Online ISBN: 978-3-540-47764-8
eBook Packages: Springer Book Archive