Formal CHERI: design-time proof of full-scale architecture security properties (2022)(lightbluetouchpaper.org)
lightbluetouchpaper.org
Formal CHERI: design-time proof of full-scale architecture security properties (2022)
https://www.lightbluetouchpaper.org/2022/07/22/formal-cheri/
6 comments
A big application of CHERI is embedded where you can't just spend 6x more area/power on software.
Also CHERI isn't just about memory safety. It also supports software isolation & capabilities.
See CherIoT for an example of both of these.
Also CHERI isn't just about memory safety. It also supports software isolation & capabilities.
See CherIoT for an example of both of these.
Fil-C is capability based and its capabilities offer stronger guarantees than CHERI’s.
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.
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.
it would be interesting if you shared more details
https://github.com/pizlonator/llvm-project-deluge/blob/delug...
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.
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.
CHERI is more powerful than memory-safe-C because it's a capability system. It's also still useful in a world where memory safe languages are common because the there is still a large amount of unsafe code that world and CHERI lets that unsafe code still maintain the guarantees the safe code relies on.
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.
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.
> 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.
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.
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.
Improved hardware based abstractions to provide stronger security and better ways to isolate software components just seems like a good idea. Yes you can certainly do plenty in software (in particular using language like Rust) but presumably we still want hardware enforced security properties? So why not improve those as well as software?
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.
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.
Fil-C is not ABI compatible with regular C, so there’s no way to accidentally forget to compile some part of your stack with Fil-C.
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.
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.
Rust still needs CHERI to fully deliver on our expectations because it is astonishingly easy for unsafe code to violate sometimes subtle invariant that must be upheld for safe code to be safe. And both due to performance and because some correct and important code structures can't be represented well in safe rust, there will always exist some unsafe code.
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.
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.
That’s pretty damning if Rust needs CHERI to be fully safe. Fil-C has no such problem since there is no unsafe statement in Fil-C.
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.
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.
CHERI is insufficient for unsafe Rust to be fully safe, and I suspect Fil-C plus C's restrict is insufficient as well (if restrict isn't treated as a no-op, of course).
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.
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.
Restrict is treated as a no-op in Fil-C. Fil-C offers no escape hatch from memory safety, period.
CHERI plays fine with virtual memory, it's omitted in some of these minimized cores because it's not necessary for security and the target cores didn't have virtual memory to begin with.
It's still useful for making swapping work efficiently, but that's not relevant on a tiny embedded device.
It's still useful for making swapping work efficiently, but that's not relevant on a tiny embedded device.
What happens if you do a shared memory mapping and place capabilities into it?
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.
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.
It's an interesting approach. A hybrid software with limited hardware change is interesting.
> Fil-C will get faster even without architecture help
Only to a point. You'll plateau eventually since you have checks on every dereference.
> Fil-C will get faster even without architecture help
Only to a point. You'll plateau eventually since you have checks on every dereference.
No, I won’t have checks on every dereference. The monotonicity of Fil-C’s capabilities makes it possible to do a lot of redundant check elimination.
That’s what I’m working on now. Should have some early results soon.
That’s what I’m working on now. Should have some early results soon.
Obviously, removing repeated/redundant bounds checks is a basic optimization. That's not what I meant. My point still stands.
I think that check on every access is a lot different than check on some accesses.
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.
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.
Recompiling everything is a non-starter in many cases.
If recompiling is a nonstarter then a new HW arch like CHERI is even more of a nonstarter.
That's only mostly true; Big CHERI (that is, the 64-bit CHERI systems, not CHERIoT) specifically has support for running legacy binaries within capability confinement. It's true that we think recompiling is generally the better approach, but we can sandbox pre-CHERI libraries, for example, at library-scale granularity.
I'd take this over incremental clock speed improvements any day.
I've been a huge fan of CHERI for years, but unfortunately the hardware is super closed (huge research institutions only). Hopefully there will be a hardware option for hobbyists one of these years (the virtual machines don't interest me).
CHERIoT chips will be available early next year from SCI Semiconductor iirc. I have heard of some samples floating around
FWIW...
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...)
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...)
Morello is definitely what I'd been eyeing for a while. AFAICT those are real systems (somewhat like HiFive Unleashed) and not just embedded chips (although they are embedded chips too). I'm kind of bored of microcomputers (Raspberry Pi et al.).
[deleted]
This project shares so many foundational computing ideals this represents the best aspects of “the many eyes surfacing not just bugs but assumptions”.
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.
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.
Hi, sorry, this is all quite a bit above my head but I am interested in alternate architectures, would you mind expanding on what kinds of symbols you're talking about? My mind jumps to the members of an instruction set, but I assume you would have called them instructions in that case, what's the alternative to a local symbol?
Sorry I'm always trying to keep it simple.
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.
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.
Intriguing, thanks, I'll have to marinate on that.
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.
https://en.m.wikipedia.org/wiki/What_the_Dormouse_Said
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.
https://en.m.wikipedia.org/wiki/What_the_Dormouse_Said
I haven't read that book yet. I have been meaning to but just haven't gotten to it.
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.
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.
[deleted]
See the references I just posted, crossing with that, for CHERI-RISC-V if others are interested.
I wonder why emulators aren't interesting for a hobbyist. However, there are FPGA implementations [1], and micro-controller-type systems on FPGA available commercially [2].
[3] has a list of publications for the rigorous engineering agenda.
1. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
2. https://cheriot.org/
3. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
[3] has a list of publications for the rigorous engineering agenda.
1. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
2. https://cheriot.org/
3. https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...
[deleted]
> I wonder why emulators aren't interesting for a hobbyist.
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.)
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.)
> 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-...
You might be interested in a very timely blog post: https://cheriot.org/cheri/myths/2024/08/28/cheri-myths-safe-...
> CHERI doesn’t guarantee that your code is free from memory-safety errors, it guarantees that any memory-safety bugs will trap and not affect confidentiality or integrity of your program.
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.
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 on CHERI hardware is not magically memory-safe. CHERI just traps on memory-unsafety.
If it traps on all things that would otherwise be memory-unsafety then it is memory safe. If trapping doesn't count as memory safe, then e.g. Rust isn't memory safe, since it traps on OOB accesses to arrays.
CHERI capabilities are memory-safe, because they trap on any attempted memory unsafety. Safe Rust is memory-safe, assuming all the underlying Unsafe Rust traps on any attempted memory unsafety.
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...)
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...)
I'm not sure if we are talking past each other or what.
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?
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?
In #3, the C implementation is not what's memory-safe, that's what I've been trying to say. CHERI is memory-safe, but the C isn't what actually guarantees the memory safety. You can dereference a null pointer on CHERI. The architecture can trap it, but that doesn't change the fact that C actually attempted to do it and therefore would not be memory-safe. Only the system as a whole prevents the memory unsafety.
Aha. I think we agree. I originally said "C on CHERI hardware is memory safe" by which I meant "the system as a whole of (C code + CHERI hardware)" is memory safe, but you seemed to think I meant (C code) is memory safe.
I'm not talking about writing robust software, I'm talking about having fun - Rust's type system already provides the type of fun that I would have gotten from a CHERI emulator. That's why only getting to own physical CHERI hardware would truly pique my interest.
That article indeed is quite timely. I do agree with it. Slightly different angle though.
That article indeed is quite timely. I do agree with it. Slightly different angle though.
[deleted]
(2022)
[deleted]
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.