Abstract
This paper describes a new static analysis to show the absence of memory errors, especially string buffer overflows in C programs. The analysis is specifically designed for the subset of C that is found in critical embedded software. It is based on the theory of abstract interpretation and relies on an abstraction of stores that retains the length of string buffers. A transport structure allows to change the granularity of the abstraction and to concisely define several inherently complex abstract primitives such as destructive update and string copy. The analysis integrates several features of the C language such as multi-dimensional arrays, structures, pointers and function calls. A prototype implementation produces encouraging results in early experiments.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aitel, D.: The advantage of block-based protocol analysis for security testing. Technical report, Immunity, Inc. (2002)
Baratloo, A., Singh, N., Tsai, T.: Transparent run-time defense against stack smashing attacks. In: Proceedings of the USENIX Annual Technical Conference 2000 (2000)
Biondi, P.: Scapy, http://www.secdev.org/projects/scapy/
Chess, B.: Improving computer security using extended static checking. In: IEEE Symposium on Security and Privacy (2002)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the 4th ACM Symposium on Principles of Programming Languages. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics 81(1) (1979)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cowan, C., et al.: StackGuard: Automatic adaptive detection and prevention of buffer-overflow attacks. In: Proceedings of the 7th USENIX Security Symposium. USENIX Association (1998)
Dor, N., Rodeh, M., Sagiv, M.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation. ACM Press, New York (2003)
Eichin, M.W., Rochlis, J.A.: With microscope and tweezers: An analysis of the internet virus of november 1988. In: Proceedings of the 1989 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos (1989)
Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software 19(1) (2002)
Ganapathy, V., Jha, S., Chandler, D., Melski, D., Vitek, D.: Buffer overrun detection using linear programming and static analysis. In: Proceedings of the 10th ACM Conference on Computer and Communications Security. ACM Press, New York (2003)
Haugh, E., Bishop, M.: Testing C programs for buffer overflow vulnerabilities. In: Proceedings of the Network and Distributed System Security Symposium, The Internet Society (2003)
Jung, Y., Kim, J., Shin, J., Yi, K.: Taming false alarms from a domain-unaware C analyzer by a bayesian statistical post analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 203–217. Springer, Heidelberg (2005)
Larochelle, D., Evans, D.: Statically detecting likely buffer overflow vulnerabilities. In: Proceedings of the 10th USENIX Security Symposium (2001)
Leroy, X., Doliguez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system release 3.06, documentation and user’s manual. Institut National de Recherche en Informatique et en Automatique (INRIA) (2002)
Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy software. ACM Transactions Programming Languages and Systems 27(3) (2005)
Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, p. 213. Springer, Heidelberg (2002)
One, A.: Smashing the stack for fun and profit. Phrack 7(49) (1996)
Ruwase, O., Lam, M.S.: A practical dynamic buffer overflow detector. In: Network and Distributed System Security Symposium, The Internet Society (2004)
Siff, M., Chandra, S., Ball, T., Kunchithapadam, K., Reps, T.: Coping with type casts in C. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999. LNCS, vol. 1687, p. 180. Springer, Heidelberg (1999)
Simon, A., King, A.: Analyzing string buffers in C. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, p. 365. Springer, Heidelberg (2002)
Sutton, M., Greene, A.: The art of file format fuzzing. In: Black Hat USA 2005 (2005)
Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation. ACM Press, New York (2004)
Viega, J., Bloch, J.T., Kohno, Y., McGraw, G.: ITS4: A static vulnerability scanner for C and C++ code. In: 16th Annual Computer Security Applications Conference. IEEE Computer Society Press, Los Alamitos (2000)
Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Proceedings of the Network and Distributed System Security Symposium, The Internet Society (2000)
Wilander, J., Kamkar, M.: A comparison of publicly available tools for static intrusion prevention. In: 7th Nordic Workshop on Secure IT Systems (2002)
Wilander, J., Kamkar, M.: A comparison of publicly available tools for dynamic buffer overflow prevention. In: Network and Distributed System Security Symposium, The Internet Society (2003)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)
Xie, Y., Chou, A., Dawson, R.E.: ARCHER: using symbolic, path-sensitive analysis to detect memory access errors. In: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering. ACM, New York (2003)
Yi, K.: Yet another ensemble of abstract interpreter, higher-order data-flow equations, and model checking. Technical Memorandum 2001-10, Research on Program Analysis System, National Creative Research Center, Korea Advanced Institute of Science and Technology (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Allamigeon, X., Godard, W., Hymans, C. (2006). Static Analysis of String Manipulations in Critical Embedded C Programs. In: Yi, K. (eds) Static Analysis. SAS 2006. Lecture Notes in Computer Science, vol 4134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11823230_4
Download citation
DOI: https://doi.org/10.1007/11823230_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37756-6
Online ISBN: 978-3-540-37758-0
eBook Packages: Computer ScienceComputer Science (R0)