4 ms·
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
by nullc 2y ago
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.
- pizlonator 2y agoThat’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.
- remexre 2y agoCHERI 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.
- pizlonator 2y agoRestrict is treated as a no-op in Fil-C. Fil-C offers no escape hatch from memory safety, period.
- nullc 2y agoCHERI 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.
- pizlonator 2y agoWhat 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.