[irogers]

Given there is before and after code, perhaps the translation can be automated. If the whole code base were auto-translated, what bugs could be detected and fed back to the C implementation? I'm assuming there is going to be hesitance from the FreeBSD community from migrating their codebase from C to Checked C, but that doesn't mean this work needs to come to nought. On top of bounded memory accesses, it'd be interesting to see better thread, signal, interrupt, etc. safety support. I guess at some point this just looks like Rust.

[mwhicks1]

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...

[aduitsis]

Slightly tangential, I am under the impression that the CHERI project has actually identified security bugs and reported them back to FreeBSD.

https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/