
CHERI-seL4: Enhancing seL4’s C/C++ memory-safety and software compartmentalisation using CHERI

Purecap seL4 kernel, user libraries, and sel4test passing all tests on a Morello box.
Introduction
seL4 is a formally verified microkernel that offers isolation between different protection domains in different address spaces. However, seL4 does not provide security at user-level within the same address space. CHERI is an architectural extension to add memory safety and compartmentalisation within the same address space. This project aims to enhance the overall security of seL4-based systems by combining both technologies: seL4’s inter-address-space isolation, and CHERI’s intra-address-space memory safety and software compartmentalisation.

Why
Having CHERI on seL4 would allow seL4 developers to:
-
Follow secure coding practices, especially when it comes to pointers
-
Introduce memory-safety for your existing C/C++ userspace, without rewriting everything in Rust
-
Be able to further automatically compartmentalise your projects in a single AS seL4 protection domain
-
Maintain C/C++ source-code backward compatibility
-
Protect against dynamic zero-day vulnerabilities
-
Be able to run completely memory-safe Linux/FreeBSD VMs

CHERI-seL4: real-world project setup
An ideal goal of an end-to-end CHERI-seL4 project with memory-safe VMs (e.g., CHERI-Linux) would be something like the following:

How
CHERI-seL4: user-space always purecap, but the kernel could be:

Status
Currently, we have released a CHERI-aware seL4 kernel that can be built and run in both CHERI C (purecap) and hybrid modes. This includes Morello and CHERI-RISC-V, both Cambridge's rich CHERI ISAv9 and a minimal subset of it called the draft standard that is going to be a standard RISC-V extension part of RISC-V International. It is able to also run complete purecap userspace projects such as sel4test and sel4bench. However, this is still largely experimental and under review. We will announce more stable releases that can be built on in the future.
