Our great sponsors
-
checkedc
Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
-
checkedc-clang
This is the primary development repository for 3C, a tool for automatically converting legacy C code to the Checked C extension of C, which aims to enforce spatial memory safety. This repository is a fork of Checked C's. (by correctcomputation)
Checked C appears to be a relatively recent research project from Microsoft[0][1], so I'm not sure that FreeBSD would be terribly keen on refactoring around it. There have also been many "safer C" languages before, so the only advantage that the paper that Checked C really offers is that it seems to have a high degree of backwards compatibility, so I guess the refactoring could occur over a longer period of time.
[0] https://www.microsoft.com/en-us/research/project/checked-c/
Checked c is interesting, but I think a more fruitful avenue would be verifast[0]. Verifast is completely compatible with existing c codebases (so you can keep using your existing c compiler), and is able to verify more interesting behaviour than checked c. [1] finds that it would have prevented 5 of 50 recent CVEs in FreeBSD, whose causes include unlocked memory accesses, fd leaks, and bad use of reference counts.
0. https://github.com/verifast/verifast
1. https://metasepi.org/en/posts/2020-10-14-avoid-freebsd-secur...
KLEE is only popular with the HN crowd, but not certainly not in the industry. There cbmc/satabs is leading. Esp. automotive. Also much older, and much easier to use. I recently even added formal verification to my CTL library variant, the STL for C.
https://github.com/rurban/ctl/commit/cc65e82ba1fdafcf9c83697...
cbmc found some huge bugs the testsuites were not able to find.
KLEE has similar status as Z3. Hugely popular, but rarely used in practice. Educational toys, or used in side-projects only.
At Correct Computation (https://correctcomputation.com/, we are hiring), we are developing a tool called 3C to provide automation assistance for the conversion of C code into Checked C. A completely automated approach is impractical (i.e., without making lots of changes to the target program's code and adding lots of overhead), but we have found a "best effort" approach works well.
See here for more info (which transitively links to a tutorial of 3C's use): https://github.com/correctcomputation/checkedc-clang/blob/ma...