Formal CHERI: design-time proof of full-scale architecture security properties (2022)
lightbluetouchpaper.org
lightbluetouchpaper.org
I bet that the Intel chip I’m on is more than 6x faster than any of the CHERI hardware.
Fil-C has a more deterministic and safer handling of use-after-free and it’s flexible enough to run CPython (pretty sure CPython was too much for CHERI’s capabilities).
If you consider that:
- Fil-C will get faster even without architecture help
- Fil-C runs on normal HW
- it probably only takes a small extension to the HW to eliminate any remaining Fil-C overhead (a much smaller extension than CHERI).
- Fil-C is just a thing I pulled out of my ass in the last 10 months or so and is a totally solo spare-time project (I.e. if a real compiler team did this full time they’d probably make it even better than where I’m at)
Then it sure does seem like CHERI is going to be doomed long term.
Also CHERI isn't just about memory safety. It also supports software isolation & capabilities.
See CherIoT for an example of both of these.
My point is that if a single dude working solo for 10 months gets to 6x overhead in the bad case then the overhead of the software capability approach (either exactly Fil-C or something vaguely like it) is likely to be much much less than 6x in the limit. Fil-C was 200x slower just six months ago and I’m not even done optimizing. That should give you an idea of where it’s heading.
https://m.youtube.com/watch?v=JRoX9_lXJFg
Note that both that doc and the video have old perf numbers. I’m landing optimizations all the time.
> Fil-C will get faster even without architecture help
Only to a point. You'll plateau eventually since you have checks on every dereference.
That’s what I’m working on now. Should have some early results soon.
That plateau might not be any different than the CHERI plateau, since at the microarch level, CHERI will have more checks since it cannot benefit from a compiler’s static reasoning about redundant check elimination.
To put it another way why not remove existing hardware security abstractions we do have? Ditch virtualization (or hugely strip it back), get rid of different privilege levels, loose page-table enforced permissions. After all you can just build safe software why bother with these things?
I for one don't think this is a sensible line of argument, defence in depth is a good idea, build your software to be as secure as possible then build your hardware such that if there is some flaw in your software's defences you can keep things contained though hardware abstractions.
Even with improved languages there's a giant body of existing code you need to work with, with compartmentalization in CHERI you can keep this stuff safely contained. Plus how do you guarantee everything running on the system has been built in your safe language and compiled with your blessed known good compiler? Feasible in some places (like embedded systems) far less feasible in others.
If changing all the HW we use was as easy as waving a wand, then your argument would be sound. Unfortunately, it’s super hard to get folks to use different HW. And because of how silicon economics work out, a new upstart architecture with limited users is sure to experience slower perf scaling than the mainstream HW. That strongly disincentivizes anyone from being an early adopter of exotic new HW. I think that’s why CHERI isn’t mainstream yet despite a decade of investment.
Hence why even ignoring Fil-C, it’s probably more realistic to rewrite stuff in Rust than it is to switch to CHERI. Fil-C adds a third option where you pay some perf but you don’t have to rewrite your code or switch what HW you use. CHERI also costs perf - practically speaking, available CHERI HW is more than 6x slower than the HW Fil-C can run on. That’s fundamental, due to silicon economics.
Finally, I think you’re overselling the CHERI defense in depth. My understanding is that CHERIoT doesn’t use virtual memory and that there are subtle reasons why virtual memory and CHERI put together gets weird, especially if you want to support capability revocation. On the other hand, Fil-C works on top of virtual memory so you get both virtual memory protection and capability protection, hence more defense in depth.
One of the advantages of CHERI is that you can get a safe system with no virtual memory, no overheads of TLB lookups and hardware, etc. but you don't have to do that. The CHERI arm and riscv64 designs have the normal memory management hardware.
No virtual memory is not an advantage of CHERI, it’s a disadvantage. It means CHERI replaces a very well understood security barrier (virtual memory) with one that is less well understood (no matter how many proofs you write about it). I would be more willing to buy CHERI’s claims if they had kept virtual memory. Fil-C plays nice with virtual memory so there’s no need to disable it.
For unsafe Rust code to be sound, it has to uphold the invariant that no location pointed to by an &mut is modified through a pointer not derived from that &mut. However, there's no such restriction on *mut pointers ("raw pointers"), and it is in many cases perfectly sound (but unsafe, of course) to cast from *mut to &mut, or to directly mutate through a *mut. Without maintaining global information about what references are live, it sounds really, really hard to guarantee this.
It's still useful for making swapping work efficiently, but that's not relevant on a tiny embedded device.
Fil-C just says that shared memory mappings are integer-only, so trying to place a capability there instantly traps. That’s both sound and adequate even for sophisticated uses of shared memory.
My understanding is that this is a conundrum for CHERI, but maybe my understanding is wrong.
The cheri extension is rather small and simple, though isn't not extremely cheap due to the longer pointers and the tag bit.
Cheri does have an answer to temporal safety too, though it has added costs. Freed memory is not immediately reused, eventually the tagged memory is swept for references then the pointer freed memory can be reused. This is both safe and faster than you might guess because all tagged objects are capabilities and all capabilities are tagged.
The simplicity of cheri itself makes it easier to be confident that its protection is correct-- relative to the entirety of a compiler/libc/etc.
The cheri solution to use after free still kinda stinks though, so I think a combination of safer languages and cheri will be interesting in the future.
Edit: I see now that Fil-c is also a capabilities system. Thanks for bringing it to my attention.
To get confidence in Fil-C’s safety, you don’t have to prove anything about the libc because the libc is compiled with Fil-C.
You have to prove stuff about the compiler and Fil-C’s runtime. The runtime is about 100KLoC.
I’m actually more interested in developing from the riscV branch.
Thinking about computers in the 100 year time frame I decided that processing “local” symbols is better than more sophisticated processes. The risc-V direct access to symbol development is where I want to start defining my “local” symbols.
The hope is that this line of thought will reduce the number of abstraction layers between the user and their environment.
CHERI having these concepts defined for risc-v creates a foundation for local processing Of symbols with a “good computing seal of integrity. I also see it as leading to less re-invention which should help progress.
The symbols I'm discussing were first documented by Claude Shannon. When I'm discussing symbols or large circuits I consider them interchangeable views of the same thing. They represent each other.
https://en.wikipedia.org/wiki/Claude_Shannon
I'm actually a designer so if I wanted to describe them as instructions I easily could. I'm a stickler for language so I believe that the use of the term instructions limits the conversation because it is too specific to communicate what I'm thinking about.
I would say an early example local symbol development might be libC. Our current computing environment evolved from the Personal Computing revolution and the internet. This came about through commercial interests and public adoption. I see this development as reaffirming the ideals first proposed by the "mother of all demos".
https://en.wikipedia.org/wiki/The_Mother_of_All_Demos
What I consider a "local" symbol is being demonstrated by Apple with their on device ML. The highest ideal to me is that everyone develops their own personal symbol table of digital services. I see CHERI as offering the fast track to that type of computing. I see this a integrating rather than programming.
I'm a big fan of the mother of all demos. Have you happened to have read "what the dormouse said" ? It has a great narrative of that event including all the behind the scenes action that Stewart Brand contributed, like setting up the TV broadcast truck on top of the hill to relay the video output and importantly the sounds of the mainframe back in Menlo park.
I can't believe we can watch the "mother of all demos". That alone proves its significance.
My favorite aspect of the demo is that it reveals that our human computing desires are universal and have been there from the start. It has taken generations to achieve the mass adoptions of these ideas. This realization takes the mystique away from the BigCo and their services. They are simple human desires for technology that were obvious from the beginning.
[3] has a list of publications for the rigorous engineering agenda.
1. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
3. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
I have the Rust programming language to fill the software part of this niche. The hardware part of CHERI is what makes it interesting to me.
(e.g. I've tinkered with Rust bootloaders before, and it doesn't matter too much whether the emulator is CHERI or not since Rust itself lets me express memory safety in the type system.)
You might be interested in a very timely blog post: https://cheriot.org/cheri/myths/2024/08/28/cheri-myths-safe-...
That sounds an awful lot like ensuring your code is free from memory-safety errors. A language which always traps on erroneous memory accesses is a memory safe language, so if CHERI really guarantees what that sentence says, then C on CHERI hardware is memory safe.
C is not memory-safe, even on CHERI, because it has to be trapped by CHERI; it cannot catch itself.
Safe Rust is memory-safe on its own, because memory unsafety can only be introduced by Unsafe Rust; Safe Rust has no unsafe operations. Assuming the Unsafe Rust is sound, Safe Rust cannot cause memory safety to be violated on its own. (You can do `/proc/mem` tricks on Linux, but that's a platform thing...)
1. Non-unsafe rust is memory-safe because otherwise unsafe operations (e.g. out-of-bounds accesses on arrays) are guaranteed to trap.
2. A typical C implementation on typical non-CHERI hardware is not safe because various invalid memory operations (e.g. out-of-bounds, use after free) may fail to trap.
3. A typical C implementation on CHERI hardware guarantees that all otherwise memory-unsafe operations trap.
I think we both agree on #1 and #2. Am I wrong about #3? If I'm not wrong about #3, then what makes you say that #3 is not memory-safe?
That article indeed is quite timely. I do agree with it. Slightly different angle though.
Morello boards are hard to come by, but there have been efforts to offer cloud-computing style use of them, especially now that bhyve support exists; if you're interested I can try to find out more (I'd offer you time on my cloud-computing Morello cluster from MSR, but it's offline for silly reasons). The "Big CHERI" RISC-V FPGA boards are indeed quite expensive, but CHERIoT-Ibex runs on the Arty A7 or the purpose-built Sonata board, and those are much more reasonable. (I'd still love to see it brought up on cheaper boards, too...)