Runtime Verification of C Memory Safety

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

Permalink

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

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