Sam Elliott

PhD Student at University of Washington

Checked C for Safety, Gradually

Draft paper including some of my work on Checked C • Currently under submission
Andrew Ruef, Archibald Samuel Elliott, Michael Hicks, David Tarditi

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. Performance evaluation on a set of standard benchmark programs shows overheads to be relatively low. More interestingly, Checked C introduces 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 violation, meaning it must have arisen from unchecked code. We formalize and prove this property. To assist programmers in migrating legacy code to Checked C, we have implemented a rewriting tool that introduces the use of checked pointers, where safe. Experiments on several legacy programs show it to be fast and effective.

Download Draft [PDF]