Nurit Dor
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.
- T.M. Austin, S.E. Breach, and G.S. Sohi. Efficient detection of all pointer and array access errors. In SIGPLAN Conf. on Prog. Lang. Design and Impl. ACM Press, 1994.]] Google Scholar
Digital Library
- R. Bodik, R. Gupta, and V. Sarkar. ABCD: eliminating array bounds checks on demand. In SIGPLAN Conf. on Prog. Lang. Design and Impl., 2000.]] Google ScholarDigital Library
- D.R. Chase, M. Wegman, and F. Zadeck. Analysis of pointers and structures. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 296--310, New York, NY, 1990. ACM Press.]] Google ScholarDigital Library
- B. Chess. Improving computer security using extended static checking. In IEEE Symposium on Security and Privacy, 2002.]] Google ScholarDigital Library
- J. Choi, M. Gupta, M.J. Serrano, V.C. Sreedhar, and S.P. Midkiff. Escape analysis for java. In Conf. on Object-Oriented Prog. Syst. Lang. and App., pages 1--19, 1999.]] Google ScholarDigital Library
- P. Cousot and N. Halbwachs. Automatic discovery of linear constraints among variables of a program. In Symp. on Princ. of Prog. Lang., 1978.]] Google ScholarDigital Library
- 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.]]Google ScholarCross Ref
- M. Das. Unification-based pointer analysis with directional assignments. In SIGPLAN Conf. on Prog. Lang. Design and Impl., 2000.]] Google ScholarDigital Library
- M. Das, B. Liblit, M. Fähndrich, and J. Rehof. Estimating the impact of scalable pointer analysis on optimization. In Static Analysis Symp., 2001.]] Google ScholarDigital Library
- A. Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 230--241, New York, NY, 1994. ACM Press.]] Google ScholarDigital Library
- E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.]] Google ScholarDigital Library
- N. Dor. Statically Detecting All Buffer Overflows in C. PhD thesis, Univ. of Tel-Aviv, Israel, 2003. In preparation.]]Google Scholar
- N. Dor, M. Rodeh, and M. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In Static Analysis Symp., 2001.]] Google ScholarDigital Library
- C. Flanagan, K. Rustan, and M. Leino. Houdini, an annotation assistant for Esc/java. In Formal Methods for Increasing Software Productivity, volume 2021 of Lecture Notes in Computer Science, 2001.]] Google ScholarDigital Library
- R. Ghiya, D. Lavery, and D. Sehr. On the importance of points-to analysis and other memory disambiguation methods for c programs. In SIGPLAN Conf. on Prog. Lang. Design and Impl., 2001.]] Google ScholarDigital Library
- N. Halbwachs. Static Analysis of Linear Properties Invariantly Satisfied by the Numeric Variables of a program. PhD thesis, Grenoble University, 1979.]]Google Scholar
- N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157--185, 1997.]] Google ScholarDigital Library
- N. Heintze and O. Tardieu. Ultra-fast aliasing analysis using cla: A million lines of c code in a second. In SIGPLAN Conf. on Prog. Lang. Design and Impl., 2001.]] Google ScholarDigital Library
- B. Jeannet. New polka library. Available at "http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html".]]Google Scholar
- B. W. Kernighan and D. M. Ritchie. The C programming language. Prentice-Hall, Englewood Cliffs, NJ 07632, USA, 1988.]] Google ScholarDigital Library
- P. Kolte and M. Wolfe. Elimination of redundant array subscript range checks. ACM SIGPLAN Notices, 30(6):270--278, 1995.]] Google ScholarDigital Library
- W. Landi. Interprocedural Aliasing in the Presence of Pointers. PhD thesis, Dept. of Comp. Sci., Rutgers Univ., 1991.]] Google ScholarDigital Library
- D. Larochelle and D. Evans. Statically detecting likely buffer overflow vulnerabilities. In 10th USENIX Security Symposium, 2001.]] Google ScholarDigital Library
- G. Leavens and A. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In Formal Methods, 1999.]] Google ScholarDigital Library
- D. Liang and M. J. Harrold. Efficient computation of parameterized pointer information for interprocedural analyses. In Static Analysis Symp., 2001.]] Google ScholarDigital Library
- A. Loginov, S. Yong, S. Horwitz, and T. Reps. Debugging via run-time type checking. In Proc. of Fundamental Approaches to Softw. Eng. (FASE), April 2001.]] Google ScholarDigital Library
- T.J. Marlowe and B. G. Ryder. An efficient hybrid algorithm for incremental data flow analysis. In Symp. on Princ. of Prog. Lang., 1990.]] Google ScholarDigital Library
- 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.]]Google Scholar
- C. Morgan. Programming from Specifications. Prentice-Hall, Engelwood N.J, 1990.]] Google ScholarDigital Library
- E.W. Myers. A precise inter-procedural data flow algorithm. In Symp. on Princ. of Prog. Lang., 1981.]] Google ScholarDigital Library
- Inc. Rational. Purify software. Available at "http://www.rational.com", 1995.]]Google Scholar
- Microsoft Research. AST-toolkit. 2002.]]Google Scholar
- R. Rugina and M.C. Rinard. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In SIGPLAN Conf. on Prog. Lang. Design and Impl., 2000.]] Google ScholarDigital Library
- B. G. Ryder, W. A. Landi, P. A. Stocks, S. Zhang, and R. Altucher. A schema for interprocedural modification side-effect analysis with pointer aliasing. ACM Transactions on Programming Languages and Systems, 23(2):105--186, 2001.]] Google ScholarDigital Library
- A. Simon and A. King. Analyzing string buffers in c. In International Conference on Algebraic Methodology and Software Technology, 2000.]] Google ScholarDigital Library
- B. Steensgaard. Points-to analysis in almost-linear time. In Symp. on Princ. of Prog. Lang., pages 32--41, 1996.]] Google ScholarDigital Library
- 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.]]Google Scholar
- G. Yorsh. CoreC: A Simplifier for C, 2002. http://www.cs.tau.ac.il/˜gretay/GFC.htm.]]Google Scholar
Index Terms
- CSSV: towards a realistic tool for statically detecting all buffer overflows in C
Recommendations
CSSV: towards a realistic tool for statically detecting all buffer overflows in C
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 ...
ARCHER: using symbolic, path-sensitive analysis to detect memory access errors
Memory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both ...
ARCHER: using symbolic, path-sensitive analysis to detect memory access errors
ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineeringMemory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both ...
Comments