Two proven technologies, combined for stronger security.
CHERI: memory protection built into the processor
CHERI (Capability Hardware Enhanced RISC Instructions) adds hardware capabilities to today's processors. Every memory access is checked against its allowed bounds and permissions before it happens, and most existing code can be recompiled for CHERI with only minor changes.
This matters because memory-safety bugs cause a large share of security vulnerabilities; Microsoft has reported the figure as around 70%. A typical example is a network message that is larger than the program expects, letting an attacker overwrite nearby memory. On CHERI hardware, that attack triggers an exception before any memory is changed. The attempt can be logged and the software restarted safely.
CHERI also detects related attacks such as use-after-free, and lets software be split into isolated compartments that cannot access each other's memory.
seL4: the formally verified microkernel
seL4 is a real-time microkernel with mathematical proof that it behaves as specified, from design down to the running code, and that it enforces key security properties. It is also among the fastest kernels of its kind.
Its job is to keep programs separate in both memory and time, while letting them communicate in controlled ways. This makes it possible to analyse and prove properties about a whole system.
Why combine them
These protections complement each other. Our project ports seL4 to the Arm Morello board, Arm's CHERI prototype based on the Neoverse N1 processor.
Progress so far
Capability exceptions can now be raised, handled and, where appropriate, the program continued. A small number of seL4 libraries and example applications have been recompiled for CHERI. The work was supported by Digital Catapult's Digital Security by Design programme and by Dstl through DASA, and presented at the 2023 seL4 Summit.