Westley Weimer

EECS Department, University of California, Berkeley

Technical Report No. UCB/CSD-03-1247

, 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. <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.

---

BibTeX citation:

@techreport{Weimer:CSD-03-1247,
    Author= {Weimer, Westley},
    Title= {The CCured Type System and Type Inference},
    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