A Formal Model of Checked C
arxiv.org
arxiv.org
• ptr<T > types a pointer that is either null or points to a single object of type T.
• array_ptr<T > types a pointer that is either null or points to an array of T objects. The array width is defined by a bounds expression, discussed below.
• nt_array_ptr<T > is like array_ptr<T > except that the bounds expression defines the minimum array width— additional objects may be available past the upper bound, up to a null terminator."
It's not hard to do this if you retrofit checkable array types. I've proposed that myself.[1] The trouble is, you've created another C variant, one with checking. There are many of those, and none have caught on.
[1] http://www.animats.com/papers/languages/safearraysforc43.pdf
But that isn't what you mean, I know.
Because none of these approaches have been adopted by the standards committee – of which most of the members think C as it is today is just fine and are not interested in these sorts of large-scale safety improvements.
If we as an industry could get some new blood on the committee this is an entirely solvable problem. It doesn't require a disruption either: the standard can specify that behavior is implementation defined when safety guarantees are violated so your embedded DSP target can continue whatever it is doing today but the rest of us stuck with 100s of millions of lines of C code can start making some improvements.
Another interesting link is https://support.apple.com/guide/security/memory-safe-iboot-i... : Apple modified C compiler to improve iBoot security. I never found this particular implementation, I guess it's proprietary.
If anything releasing the modifications would carry significant weight and might even kick the tires sufficiently enough to see some coherent coordination and actual traction. I mean Apple clearly have the knowhow, what with LLVM and all!
:v
The first step is build as 32 bits as clean as possible then attempt to update to be able to also build for 64 bits.
Actually it's already working on Ubuntu 18.04 see the build here https://github.com/mingodad/cyclone/actions .
One of the main reasons to do it is to preserve for historical purposes .
There is also this other repositories that seems to try something similar:
https://github.com/moon-chilled/cyclonic https://github.com/catb0t/cyclone https://github.com/pippijn/cyclone https://github.com/iphydf/cyclone
The hard part is taking that unsafe C/Rust and turning it into checked/safe code. For this part, Rust has many benefits over C:
- As a language it is easier to refactor. This is due to a more hygenic macro system, a lack of header files, etc.
- The safe subset of Rust is much larger and more expressive than the subset of checked C. This provides more options for the unsafe -> safe translation effort.
- The safe subset of Rust is more powerful than the subset of checked C. This means that it's more likely that a piece of code can be translated 1:1 into safe Rust, compared to a more complex transformation. For example, code which returns a pointer into one of its arguments is not uncommon in C, and this can be directly translated into Rust lifetime annotations.
This makes no sense; extending C code with Checked-C would still be easier as with Checked-C you wouldn't do any translation at all; it's a superset of C, in the same way that TypeScript is to JavaScript.
Second, you can't just add checked C to a codebase, because you have to actually interop with the unchecked C code, which uses different pointer types.
My argument is that it may be easier to do an automatic migration to unsafe Rust, and then incrementally convert to safe Rust, than it would be to leave the codebase as C and try to incrementally convert it to checked C, because the "incremental conversion to checked C" is extremely difficult.
Then add the fact that exist transformations that turn temporal errors into spatial errors, and you'll see it's not necessarily much of a limitation even then:
> Memory deallocation can be modeled as an assignment. For example, the statement free(p) can be represented by the statement p=invalid, where invalid is a special untyped pointer to a temporally ‘invalid’ range of memory.
Absolutely not. That works for memory accesses through 'p'. It doesn't help you at all for memory accesses through other pointer aliases to the same memory block.
I mean, it's trivial to replace "free(p)" with a macro that also nulls out 'p', but no-one claims that that solves UAF bugs.
If you think the paper is right, just explain how it detects use-after-free in the following code fragment:
int* p = (int*)malloc(sizeof(int));
int* q = p;
free(p);
*q = 1;> After this assignment, the base and bound of p would be updated to be equal to that of the invalid pointer, and any pointer derived from or aliased with p would inherit this metadata as well (see Section 3.5).
Looking at section 3.5, it sounds like what it's actually doing is keeping a global table of every valid base pointer and its maximum offset, and when you free a pointer, it updates that table accordingly, not just the local variable containing the pointer as it previously said.
According to the paper, it is:
"Checked C is backward compatible with legacy C in the sense that all legacy code will type-check and compile. However, only code that appears in checked regions, which we call checked code, is spatially safe. Checked regions can be designated at the level of files, functions, or individual code blocks, the first with a #pragma and the latter two using the checked keyword. Within checked regions, both legacy pointers and certain unsafe idioms (e.g., variadic function calls) are disallowed."
>> I’ve yet to see a convincing reason to use it instead of, say, Go. Or Rust, if you want real safety.
What if you have a legacy codebase with hundreds of thousands of lines of C you want to maintain and improve?
What if Go, Rust, etc. are not supported on your target platform?
We know that smaller projects have successfully gone on the journey of moving from C to Rust, and they did so the same way you a whale right? One bite at a time.
So that might absolutely be a reasonable choice. Things that could make it especially attractive:
* There's existing Rust skill set in your team and not checked C
* You intend to do other new work in Rust, so this is a skill set you'll be needing anyway.
* There is relevant existing work in Rust e.g. today you use a popular C library for processing radar data. You know an equivalent library (or a port of the C library) is available as a Rust crate, if you went with Checked C, either the library isn't checked (partly undoing the good work) or you have to also translate the third party library to checked C.
* The main benefit you were looking for is something checked C doesn't care about e.g. freedom from data races is a pretty big deal for concurrent software, and checked C doesn't do that today, and has no plans to do it in future but such races aren't possible in (safe) Rust. Or you wish you had nice built-in features like iterators.
* Or the opposite side of the same coin, the main thing you dislike about C is still present in checked C. Maybe you don't like C's silent wrapping overflow, in checked C it's still there, but in Rust you can switch it off. Maybe you don't want the integer fifteen to be silently considered boolean "true" because you thought this programming language was supposed to have type checking, Rust is with you on that, Checked C of course is not.
Not everyone has those options, so any tools that can help within the limitations (such as Checked C) are welcome.
Spoken by someone who clearly doesn't understand software safety. Neither Rust nor Go are "safe", formally.