Checked C extends C with bounds checking and improved type-safety. This helps developers write more secure systems code.
- It is opt-in and backwards compatible. As a developer, you add annotations and/or modify types to opt-in to bounds checking and type-safety.
- All existing C code is valid Checked C code.
- It supports incremental conversion of code. You can convert a few security-critical functions or your entire program, and do the conversion as you have time.
- It supports annotations that can be erased from your program using macros, so that your Checked C code can compile with C compilers that do not understand Checked C annotations.
Checked C includes a language specification, samples, a compiler, and 3C, a tool for translating existing C code to Checked C.
The language specification and compiler were developed at Microsoft from 2015-2021. The Checked C effort now continues as an active open-source research project. Recent contributions include:
- The 3C tool for translating C to Checked C (Aravind Machiry, Mike Hicks and others). A paper on this tool appeared in OOPSLA '22 and won a Distinguished Paper award.
- Fat-pointers for temporal safety (Jie Zhou, John Criswell, and Mike Hicks). This work will appear in the upcoming OOPSLA ’23 conference.
- Support for erasing annotations for C compilers that don’t support Checked C (in progress).
- Experiments with converting open-source systems code.
As of 2023, we're officially a non-profit! This supports continuity of the project beyond any one person, helps us keep track of intellectual property rights, and will let us raise funds so support project activities.
