Software written in C (and C++) is the source of many serious security vulnerabilities.
Over the last 30 years, software written in C and C++ has been the target of widespread attacks with colorful names like buffer overflow, buffer overread, and integer overflow. These attacks are possible because C/C++ programs are not spatially memory safe, meaning that attackers can induce code to read or write a memory buffer outside its bounds, either to steal information or even to run code of the attacker’s choosing. Despite their long history, these attacks are still among the most dangerous and prevalent today (they are #2, #4, and #5 on this 2020 list from MITRE).
5C (and its open-core version, 3C) is a software tool that aims to help address this tension. 5C employs novel automated reasoning technology to analyze your legacy C codebase, and will insert annotations that conform to the Checked C dialect of C. Using these annotations, the Checked C open-source compiler can ensure your code is spatially memory safe. Because Checked C is backward-compatible with legacy C, you can use 5C to migrate your code in a pay-as-you-go fashion, rather than require a large investment all at once, as would be required to move your code to a different, safe language like Rust or Go.
The accompanying video demonstrates how 5C works.