Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

The CCured Type System and Type Inference

Westley Weimer

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-03-1247
December 2003

http://www.eecs.berkeley.edu/Pubs/TechRpts/2003/CSD-03-1247.pdf

We present CCured, a type and run-time check system that bring safety to the C programming language. CCured includes a type system for C programs that classifies pointers according to their usage and instructs a source-to-source translator to extend the program with run-time checks in order to guarantee memory safety. We show that the type system is sound in the presence of these run-time checks. CCured can be used on existing C programs thanks to a simple pointer-kind inferencer; on many programs this inferencer discovers that over 80% of the pointers are type-safe.

A significant contribution of our work with CCured is a notion of physical subtyping that is expressive enough to capture common C programming paradigms, is sound in the presence of pointer arithmetic and is suited for simple type inference.

This report formalizes the semantics of CCured and presents experimental evidence that such a combination of static analysis and run-time checking for C can make real system software like Apache modules, Linux device drivers, and network server software memory-safe with a reasonable performance cost and can find programming errors in instances where some existing tools like Purify cannot.


BibTeX citation:

@techreport{Weimer:CSD-03-1247,
    Author = {Weimer, Westley},
    Title = {The CCured Type System and Type Inference},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2003},
    Month = {Dec},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2003/5327.html},
    Number = {UCB/CSD-03-1247},
    Abstract = {We present CCured, a type and run-time check system that bring safety to the C programming language. CCured includes a type system for C programs that classifies pointers according to their usage and instructs a source-to-source translator to extend the program with run-time checks in order to guarantee memory safety. We show that the type system is sound in the presence of these run-time checks. CCured can be used on existing C programs thanks to a simple pointer-kind inferencer; on many programs this inferencer discovers that over 80% of the pointers are type-safe. <p>A significant contribution of our work with CCured is a notion of physical subtyping that is expressive enough to capture common C programming paradigms, is sound in the presence of pointer arithmetic and is suited for simple type inference. <p>This report formalizes the semantics of CCured and presents experimental evidence that such a combination of static analysis and run-time checking for C can make real system software like Apache modules, Linux device drivers, and network server software memory-safe with a reasonable performance cost and can find programming errors in instances where some existing tools like Purify cannot.}
}

EndNote citation:

%0 Report
%A Weimer, Westley
%T The CCured Type System and Type Inference
%I EECS Department, University of California, Berkeley
%D 2003
%@ UCB/CSD-03-1247
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2003/5327.html
%F Weimer:CSD-03-1247