2 ms·

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

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.

remexre 2y ago
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.
- pizlonator 2y ago
  Restrict is treated as a no-op in Fil-C. Fil-C offers no escape hatch from memory safety, period.
nullc 2y ago
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.
- pizlonator 2y ago
  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.

remexre 2y ago

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.

pizlonator 2y ago
Restrict is treated as a no-op in Fil-C. Fil-C offers no escape hatch from memory safety, period.

nullc 2y ago

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.

pizlonator 2y ago
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.