C But Safe
Xr0 is a verifier for C.
It eliminates many stubborn instances of undefined behaviour, like
use-after-frees, double frees,
null pointer dereferences
and the use of uninitialised memory.
Xr0 uses C-like annotations to verify code:
void *
alloc() ~ [ return malloc(1); ] /* caller must free */
{
return malloc(1);
}
More about the annotations
They’re attached to every function that is potentially unsafe and express what
its callers need to know to use it safely:
void *
alloc_if(int x) ~ [ if (x) return malloc(1); ] /* caller must free if x != 0 */
{
if (x) {
return malloc(1);
} else {
return NULL;
}
}
The really subtle safety bugs creep in through layers of function calls.
Xr0 makes this impossible, because everything needed to secure safety is
distributed through every function call, so that no subtle mistake can creep in.
It “quantum entangles” the safety semantics of every part of the program with
every other part.
Think of it like a infinitely rich type system that rises to the demands of your
program’s structure.
You still have to make the code safe; Xr0 just checks your work.
Thus Xr0 is magical like the wand, not the magician.
The real magic comes from the programmer.
Xr0 is a work in progress and currently verifies a subset of C89.
Its most significant limitation is we haven’t yet implemented verification for
loops and recursive functions, so these are being bridged by axiomatic
annotations.
Xr0 1.0.0 will enable programming in C with no undefined behaviour, but for now
it’s useful for verifying sections of programs.
Xr0 is written in pure C and is open source.
View it on GitHub or
SourceHut.
Intrigued?
Read the tutorial and give Xr0 a spin.
If you want to go deeper, engage with our theses, which explain
how Xr0 will make C safe, and take a look at
our vision and roadmap.
Come and talk to us on the Xr0 Zulip, or
via email here and here.
The Xr0 project is grateful for generous support from
An open-source modern team chat app designed to keep both live and
asynchronous conversations organized.
