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://www2.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://www2.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://www2.eecs.berkeley.edu/Pubs/TechRpts/2003/5327.html
%F Weimer:CSD-03-1247