Title: Putting the Checks into Checked C
Advisors: Ras Bodik and Dan Grossman
Abstract:
Checked C is an extension to C that aims to provide a route for
programmers to upgrade their existing C programs to a safer language
without losing the low-level control they enjoy. The first origin of
unsafe code that Checked C is addressing is spatial memory safety,
such as buffer overruns and out-of-bounds memory accesses.
Checked C addresses these memory safety problems by adding new pointer
and array types to C, and a method for annotating pointers with
expressions denoting the bounds of the objects they reference in
memory. To ensure memory safety, the Checked C compiler uses a mixture
of static and dynamic checks over these additions to the C language.
This talk concerns these Dynamic Checks, and the
algorithms and infrastructure required to support them, including: the
soundness property Checked C is aiming to preserve, propagation rules
for bounds information, and the code generation algorithm for the
checks themselves. This talk includes an evaluation of these dynamic
bounds checks, their overhead, and their interaction with a
state-of-the-art optimizer.