Checked C
Image by yogiermansyah22 on Freepik
An extension to C for making existing C code more secure
Checked C extends C with bounds checking and improved type-safety. It helps programmers retrofit existing C code to be more secure. It is:
Opt-in: you choose to use features by adding annotations.
Binary-compatible: data layout and ABIs do not change.
Incremental: programs can be converted in steps as you have engineering time.
Erasable: your code can still compile with C compilers that do not understand Checked C.
Learn More
Checked C is an open-source project. Most of our work happens on GitHub. We have:
An overview of the Checked C extension.
A language extension specification.
A fork of clang that implements the Checked C extension. Checked C clang compiler releases for Windows, Mac, and Ubuntu are available here.
A conversion tool named 3C for adding Checked C annotations to existing C code. 3C is included in the compiler releases.
Try It Out
You can download the Checked C compiler for Windows, Mac, and Ubuntu here.
Try some simple programs from https://github.com/checkedc/checkedc/tree/main/samples.
To see Checked C on some real-word code bases, look at these forks of:
Next Steps For Checked C
In 2024,
Microsoft transferred ownership of the Checked C and Checked C clang repos to the Checked C GitHub organization. We merged our forks back into those repos.
We have started work on updating to newer clang sources.
We will be updating the specification to include additional features implemented in the compiler that currently are only documented on Wiki pages or in compiler documentation, such as widening of bounds for pointers to null-terminated arrays, safe varargs support, and existential types
History
In 2023, we made Checked C easier to use:
We released pre-built versions of the Checked C compiler for Windows, Mac, and Ubuntu, so that users do not have to build the latest version of the compiler from source code.
We updated the specification to make it easier to read and to match the compiler implementation. We clarified what features are implemented versus in a future roadmap.
We have been adding support for erasing Checked C annotations so that programs can still compile with C compilers that do not understand Checked C.
Checked C is an independent open-source project. It started as a research project at Microsoft in 2015. We were looking for a way to improve the security of existing systems software and eliminate classes of bugs. One approach is to rewrite the software in a newer language such as Rust. However, rewriting code can be costly, technically challenging, and take a long time before you have working system. The technical challenges can range from having to use a different approach to managing memory, such as Rust's ownership types, to subtle nuanced differences in basic language features such as arithmetic. A costly, technically challenging, and lengthy rewrites is a high-risk software endeavor for almost any project or company. For these reasons, we think it is crucial for the security of modern systems to provide approach that let code be re-used and modified incrementally to be more secure.
Researchers from many universities and companies have contributed to Checked C, including researchers at Purdue University, the University of Maryland, the University of Rochester, the University of Washington, Samsung, Rutgers University, and the University of Pennsylvania Apple has proposed and implemented a C extension similar to Checked C that uses more dynamic checking.