Checked C is not yet 1.0, now at 0.9, so it is natural to find low adoption. But yes, I am not aware of any significant early adoption (like Dropbox did for Rust).
This paper seems to indicate that Amazon is interested in Checked C?
The gradual typing approach looks interesting: [emphasis mine]
Checked C’s design was inspired by prior safe C dialects such as Deputy and Cyclone. A key departure is that it aims to facilitate incremental porting. To this end, Checked C is backward compatible with legacy C, which allows checked pointers to be added piecemeal to an existing program, in the style of gradual typing.
For example, the following is valid Checked C:
void foo(int *q) { int x; ptr<int> p = &x; *q = 0; *p = 1; }
Spatial safety checks are only added for Checked pointer types, e.g., p above.
When a program is not fully ported, the spatial safety guarantee is partial. In particular, a programmer is able to designate regions of code — whole files, single functions, or even single blocks of code — as checked regions; these are often designated with a checked annotation.
So instead of marking unchecked regions as you’d do in Rust for instance, you mark checked regions.
However:
Checked C does not yet ensure temporal memory safety, which means that it does not prevent use-after-free errors. While spatial safety is still quite useful on its own, an extension to Checked C to ensure temporal safety, similar in spirit to CETS. Temporal safety can also be ensured by linking a conservative garbage collector.
I wanted to give it a try, but it took me a while to find a pointer to the source code in the paper: (I would have put this either at the beginning or at the end of the paper)
3C and the programs we have ported with it are freely available as part of the Secure Software Development Project (SSDP)’s fork of Checked C, at https://github.com/secure-sw-dev
I might try it out later today, it will take a while to build:
Because all of LLVM and clang are built as dependencies, this may consume up to ~50 GB of disk space, take several hours (depending on the speed of your computer), and require ~10 GB of RAM.
Who is using checked C?
I’ve heard C users often want something “like C but safe”, but who has actually made the switch?
Checked C is not yet 1.0, now at 0.9, so it is natural to find low adoption. But yes, I am not aware of any significant early adoption (like Dropbox did for Rust).
This paper seems to indicate that Amazon is interested in Checked C?
The gradual typing approach looks interesting: [emphasis mine]
So instead of marking unchecked regions as you’d do in Rust for instance, you mark checked regions.
However:
I wanted to give it a try, but it took me a while to find a pointer to the source code in the paper: (I would have put this either at the beginning or at the end of the paper)
That link is too general. It turns out to be buried here: https://github.com/microsoft/checkedc-clang/blob/master/clang/tools/3c/README.md
I might try it out later today, it will take a while to build: