Abstract
C is the most widely used imperative system’s implementation language. While C provides types and high-level abstractions, its design goal has been to provide highest performance which often requires low-level access to memory. As a consequence C supports arbitrary pointer arithmetic, casting, and explicit allocation and deallocation. These operations are difficult to use, resulting in programs that often have software bugs like buffer overflows and dangling pointers that cause security vulnerabilities. We say a C program is memory safe, if at runtime it never goes wrong with such a memory access error. Based on standards for writing “good” C code, this paper proposes strong memory safety as the least restrictive formal definition of memory safety amenable for runtime verification. We show that although verification of memory safety is in general undecidable, even when restricted to closed, terminating programs, runtime verification of strong memory safety is a decision procedure for this class of programs. We verify strong memory safety of a program by executing the program using a symbolic, deterministic definition of the dynamic semantics. A prototype implementation of these ideas shows the feasibility of this approach.
This is a preview of subscription content, log in via an institution to check access.
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
Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. In: POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 128–139. ACM, New York (2002)
Hastings, R., Joyce, B.: Purify: Fast detection of memory leaks and access errors. In: Proceedings of the Winter USENIX Conference, January 1992, pp. 125–136 (1992)
Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 89–100. ACM, New York (2007)
Berger, E.D., Zorn, B.G.: Diehard: probabilistic memory safety for unsafe languages. In: PLDI 2006: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pp. 158–168. ACM, New York (2006)
Novark, G., Berger, E.D., Zorn, B.G.: Exterminator: Automatically correcting memory errors with high probability. Commun. ACM 51(12), 87–95 (2008)
Harbison, S.P., Steele, G.L.: C: A Reference Manual, 5th edn. Prentice Hall, Englewood Cliffs (2002)
Roşu, G.: K: A Rewriting-Based Framework for Computations – Preliminary version. Technical Report UIUCDCS-R-2007-2926, University of Illinois (2007)
Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theor. Computer Science 373(3), 213–237 (2007)
Şerbănuţă, T.F., Roşu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Inf. and Comp. (to appear, 2009), http://dx.doi.org/10.1016/j.ic.2008.03.026
Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)
Walicki, M., Meldal, S.: Algebraic approaches to nondeterminism: An overview. ACM Comput. Surv. 29(1), 30–81 (1996)
Rosu, G., Schulte, W.: Matching logic. Technical Report UIUCDCS-R-2009-3026, University of Illinois at Urbana-Champaign (2009)
Rogers Jr., H.: Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge (1987)
K-Maude web page, http://fsl.cs.uiuc.edu/index.php/K-Maude
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roşu, G., Schulte, W., Şerbănuţă, T.F. (2009). Runtime Verification of C Memory Safety. In: Bensalem, S., Peled, D.A. (eds) Runtime Verification. RV 2009. Lecture Notes in Computer Science, vol 5779. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04694-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-04694-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04693-3
Online ISBN: 978-3-642-04694-0
eBook Packages: Computer ScienceComputer Science (R0)