University of Illinois Urbana-Champaign

Runtime Verification of C Memory Safety

Rosu, Grigore; Schulte, Wolfram; Serbanuta, Traian Florin

Content Files
Runtime Verification of C Memory Safety.pdf

Permalink

https://hdl.handle.net/2142/11533

Description

Title
Runtime Verification of C Memory Safety
Author(s)
  • Rosu, Grigore
  • Schulte, Wolfram
  • Serbanuta, Traian Florin
Issue Date
2009-03
Keyword(s)
programming languages
Date of Ingest
2009-04-23T16:03:29Z
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."
Type of Resource
text
Genre of Resource
Technical Report
Permalink
http://hdl.handle.net/2142/11533
Copyright and License Information
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections

Research and Tech Reports - Computer Science PRIMARY