Programming in C and C++ is risky. Unlike modern languages, C/C++ programs do not enjoy spatial safety, an aspect of memory safety that is ensured when a pointer dereference is always within the memory allocated to that pointer. Buffer overruns—a spatial safety violation—still constitute one of the most frequent and pernicious sources of vulnerability, despite their long history and many attempts to eliminate them. We have been working with Microsoft on Checked C, an extension to C that aims to provide spatial memory safety.

Why is Checked C useful? Today, most systems software is written in C (and/or C++). Systems software includes operating systems, cyberphysical systems, storage systems, and web browsers. System software is the “infrastructure” software that the world runs on. It seems oxymoronic that the software we trust the most is programmed in the least safe language(s). But this point of view fails to appreciate that there is a lot of C and C++ code out there; by one count there is 6.6 billion lines of open-source C. While new projects could benefit from being written in memory-safe languages like Rust or Go, we must accept the reality that a lighter-weight approach is needed for software we already have.

Checked C is specifically designed to ease the porting of and interaction with legacy code. It is a fork of Clang, and freely available on Github. Currently we are pursuing two main activities:

  • Developing a tool called Checked-C-convert that aims to assist in adding Checked C annotations to legacy C code automatically.
  • Formalizing the Checked C language and mechanizing its proof of spatial safety (using the Coq proof assistant).

Past publications from members of this project: