Home

Welcome

Welcome to the Wiki for the Secure Software Development Project (SSDP) fork of Checked C. Checked C was created by Microsoft, but Microsoft has stopped development work on Checked C. We created the SSDP fork to continue development of Checked C.

The goal of the SSDP fork of Checked C is to improve system programming by making fundamental improvements to C, the most widely-used system programming language. C was invented more than 40 years ago and at the time, it was a big step up over assembly code. As a community, we've learned a lot since then. There is a great opportunity to make improvements that would benefit overall computer security, given howw C is widely used.

The Checked C extension

Checked C adds checking to C to prevent or detect common low-level programming errors. Checked C provides a way for programmers to check that pointer and array accesses stay in bounds at run time. It also checks for memory accesses via null pointers. We plan to add more checking, including checking for pointer arithmetic involving null pointers, pointer arithmetic overflow, and checking casts.

• For a quick description of the extension, see the Extension Overview.
• For a detailed description, see the PDF of the specification.

Status

You can build your own copy of the compiler. The implementation is not complete, but it is far enough along that you can try out Checked C now.

A description of the extension features that we are implementing is here. The implementation status is here.

Example code

• For some simple code, see the samples directory.

• For some more complicated examples, see our Checked C translations of the Olden and PtrDist benchmarks.

• To see some real-world C code that has been converted to Checked C, see

  • The Checked C fork of the parson JSon parser.
  • The Checked C branch of the Microsoft Research Robust Internet of Things (RIoT) project. In this branch, the cryptography code has been converted to use Checked C.

  -For some in-progress conversions to Checked C, seeon converting the following code bases to Checked C:

  1. Vsftpd (re-port branch)
  2. Lua (checkedc-port branch)
  3. The Checked C fork of the musl C library.
  4. The Checked C fork of libc-test. Used to test the conversion of musl to Checked C.

Participating

Checked C is an open-source project. Anyone with time or interest can participate. We're happy to have the help! Just trying out Checked C, reporting bugs, and giving us feedback is helpful. There are other ways to contribute too.

People from Microsoft, the University of Maryland, the University of Washington, and Samsung have been participating in the project. Some folks are experimenting with using Checked C in the RIOT operating system.