Abstract

This paper presents Checked C, an extension to C designed to support spatial safety, implemented in Clang and LLVM. Checked C's design is distinguished by its focus on backward-compatibility, developer usability, and enabling highly performant code. Like past approaches to a safer C, Checked C employs a form of checked pointer whose accesses can be statically or dynamically verified. New to Checked C is the notion of a checked region. Inspired by the blame theorem from gradual typing, checked regions can be held blameless as the source of a safety violation, meaning it must have arisen from unchecked code. We formalize and prove this property using the Coq proof assistant. To assist programmers in migrating legacy code to Checked C, we have implemented a porting tool that introduces the use of checked pointers, where safe. Experiments on standard benchmarks and some legacy programs show that Checked C generates efficient code, and that the porting tool is useful.