Runtime verification of c memory safety

Grigore Roşu, Wolfram Schulte, Traian Florin Şerbǎnuţǎ

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationRuntime Verification - 9th International Workshop, RV 2009, Selected Papers
Pages132-151
Number of pages20
DOIs
StatePublished - 2009
Event9th International Workshop on Runtime Verification, RV 2009 - Grenoble, France
Duration: Jun 26 2009Jun 28 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5779 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Workshop on Runtime Verification, RV 2009
Country/TerritoryFrance
CityGrenoble
Period6/26/096/28/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Runtime verification of c memory safety'. Together they form a unique fingerprint.

Cite this