sel4 on CHERI / Morello

CHERI

(Capability Hardware Enhanced RISC Instructions) is a technology to retro-fit hardware capabilities (See also) onto current processor designs. This means that every access to memory dereferences a capability, not a pointer, and so is checked to be inside its allowable bounds, and otherwise within it's allowed permissions, before the memory is accessed or updated. Furthermore, existing software can be re-compiled to run with these checks on a CHERI-enabled processor with only very minor changes.

A large proportion (~70% - Microsoft) of security vulnerabilities are caused by software that does not correctly check that messages received from the network are not (much) bigger than they are supposed to be, or are badly formed in some other way. This allows attackers to modify the server's memory around the buffer, and change the response to the message to create a foothold for a break in. If the software has been re-compiled for CHERI, and is running on CHERI hardware, then the attack message will cause a run-time exception before any memory is affected. This allows the attack to be logged, and analysed, while the software can be restarted, and continue running unaffected.

A number of related attack techniques are directly detected by CHERI, which can also be usef to detect "use-after-errors", which can also be the vector for an attack.

Finally, CHERI provides a hardware enforced mechanism to "compartmentalize" software into communicating "compartments" which cannot access each others' memory. This provides a completely new security mechanism that can improve the security of future software.

seL4

is a real-time micro-kernel, and is unique in being the only kernel that has been formally proven to be both correctly translated from the specification to the binary running on the hardware, and also to uphold a number of security requirements. It is also very fast, currently beating all comers at a number of important benchmarks.

The kernel's main job is to separate the resources of the computer, both space and time, so that programs cannot affect each other. At the same time, the kernel has to allow those programs to communicate in useful, but bounded ways. The combination of these means that the interactions between programs can be analysed, and properties proved about the bechaviour of the overall system.

seL4 on CHERI

Simplistically:

• seL4 stops programs from interfering with each other, and
• CHERI stops programs from interfering with other parts of their own state

these are complimentary properties, both central to the security and correct operation of systems, which it should be possibe to put together. This is what our "seL4 on CHERI" project has set out to do, for the Arm Morello incarnation of CHERI based on the Arm Neoverse N1 processor.

Capability exceptions can be raised, handled, and the program continued (if appropriate). However, we have only so far been able to recompile a small number of seL4 libraries and example applications.