Checked C adds static and dynamic checking to C to detect or prevent common programmingerrors such as buffer overruns and out-of-bounds memory accesses.The goal of the project is to improve systems programming by making fundamental improvements to C.This repo containssample code, the extension specification,and test code.
We presented a research paper onChecked C 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.
We presented another paperon 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 blameproperty 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.
We presented aposterat the LLVM Dev Meeting2019: "Overflows BeGone: Checked C for Memory Safety". The poster provides an introduction toChecked C, outlines the compiler implementation and presents an experimentalevaluation of Checked C.
We presented a talk(slides)at the 2020 LLVM Virtual DevMeeting: "Checked C: Adding memorysafety support to LLVM". The talk describes the design of bounds annotationsfor checked pointers and array pointers as well as the framework for the staticchecking of the soundness of bounds. We also briefly describe novel algorithmsto automatically widen bounds for null-terminated arrays and for comparison ofexpressions for equivalence.
We're 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.You can watch the announcement pagefor announcements about the project.
The software in this repository is covered by the MIT license. See the file LICENSE.TXT for the license. TheChecked C specification is made available by Microsoft under the OpenWeb Foundation FinalSpecification Agreement, version 1.0.Contributions of code to the Checked LLVM/clang repos aresubject to the CLANG/LLVM licensing terms.
This project has adopted theMicrosoft Open Source Code of Conduct.For more information see theCode of Conduct FAQ orcontact opencode@microsoft.com with anyadditional questions or comments.