Version 0.9 of the Checked C specification released!

[sulekhark]

We are happy to announce the release of version 12.0.1 of the Checked C compiler and version 0.9 of the Checked C specification. The compiler is based on LLVM/Clang 12.0.1. The compiler is ready for experimental use with real-world code.

Over the past two years Checked C has moved from ensuring bounds safety to ensuring type safety. Our goal is to let programmers write C code that is guaranteed to be type-safe by the compiler at low cost. This prevents many common zero-day attacks on C code. It detects or prevents low-level programming errors such as buffer overflows, null dereferences and unsafe type casts.

Checked C is great for dealing with legacy C code. You do not have to rewrite the code in another programming language: Checked C is completely backwards compatible (plain C code is valid Checked C code), and Checked C annotations can be added incrementally and semi-automatically in small steps.

For an overview of the Checked C extension, see the wiki.

Checked C includes new pointer and array types with bounds checking and null checking. The bounds for pointer-typed variables and members are declared using bounds declarations. Bounds-safe interfaces allow you to declare expected behavior of libraries and to incrementally add Checked C annotations to existing code. Checked scopes provide strict type checking that guarantees type safety of code. Generic functions, generic structures and existential structures allow you to eliminate unsafe void pointer casts. Bounds-safe interfaces combined with generic functions lets you make calls to common library functions type safe. There is a semi-automated conversion tool called 3c that helps you iteratively convert code to use Checked C.

What's new in the last two years:

• Checked C compiler releases are based on LLVM/Clang release branches.
• Bounds checking for null-terminated arrays including widening of bounds based on strlen or null element checks.
• Improved checking of bounds declarations. We are very close to full soundness and the checker is smarter.
  • The checker detects the invalidation of bounds declarations when variables used in bounds declarations are modified.
  • The checker handles checking for structure members.
  • The checker handles conditional operators in assignment expressions.
  • The checker has improved validation of bounds declarations when variables used in bounds declarations are modified but the modification is invertible.
  • The checker incorporates dataflow facts in checking allowing it to prove more things.
• Improved error messages with more contextual information when the compiler is unable to statically validate bounds.
• Added support for generic structures and existential types.
• Implicit inclusion of checked header files.
• Numerous bug fixes.