Checked C

This is the Secure Software Development Project fork of Checked C. The Checked C extension was originally developed at Microsoft from 2016-2021. Microsoft has stopped funding further development of Checked C. We greatly appreciate the support of Microsoft for the project through 2021. We created this fork to continue development of Checked C.

Checked C adds static and dynamic checking to C to detect or prevent common programming errors such as buffer overruns and out-of-bounds memory accesses. The goal of Checked C is to improve systems programming by making fundamental improvements to C. This repo contains sample code, the SSDP extension specification, and test code.

• For a quick overview of Checked C, more information, and pointers to example code, see our Wiki.
• The PDF of the specification is available here.
• The Checked C fork of LLVM/clang is here.
• The instructions to build and test the Checked C compiler are documented on the SSDP Checked C clang wiki.

Publications and Presentations

• There was a research paper on Checked C presented at the IEEE 2018 Cybersecurity Development Conference: "Checked C: Making C Safe by Extension". The paper describes the key ideas of Checked C in 8 pages. Note that we have added features to Checked C for improving type safety (and reducing type confusion) since writing the paper. The Wiki and specification provide up-to-date descriptions of Checked C.

• There was another paper on Checked C at the 2019 Principles of Security and Trust Conference: "Achieving Safety Incrementally With Checked C". This paper describes a tool for converting existing C code to use Ptr types. It also proves a blame property about checked regions that shows that checked regions are blameless for any memory corruption. This proof is formalized for a core subset of the language extension.

• There was a poster presented at the LLVM Dev Meeting 2019: "Overflows Be Gone: Checked C for Memory Safety". The poster provides an introduction to Checked C, outlines the compiler implementation and presents an experimental evaluation of Checked C.

• Therew was a talk (slides) at the 2020 LLVM Virtual Dev Meeting: "Checked C: Adding memory safety support to LLVM". The talk describes the design of bounds annotations for checked pointers and array pointers as well as the framework for the static checking of the soundness of bounds. The talk also briefly describes novel algorithms to automatically widen bounds for null-terminated arrays and for comparison of expressions for equivalence.

Build Status

Automated testing is not currently available.

Participating

We are happy to have the help. You can contribute by trying out Checked C, reporting bugs, and giving us feedback. There are other ways to contribute too.

Licensing

The software in this repository is covered by the MIT license. See the file LICENSE.TXT for the license. The Checked C specification is made available by Microsoft under the OpenWeb Foundation Final Specification Agreement, version 1.0. Contributions of code to the SSDP Checked LLVM/clang repos are subject to the LLVM/clang licensing terms.

Code of conduct

This project has adopted a Code of Conduct.