CHERI

CHERI-seL4

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 and within the same VM (e.g., Linux). CHERI is an architectural extension to add memory safety and compartmentalisation within the same address space. CHERI-seL4 aims to combine seL4's security, realised through formal verification, with CHERI's memory safety and software compartmentalisation at the user level. The end goal is a fully enhanced, secure, memory-safe system spanning from the kernel and/or hypervisor level (seL4), through VMs (e.g. CheriBSD or CHERI-Linux), to seL4's native OS libraries, VMMs, and applications.

Current status

We have added support to the seL4 microkernel for running memory-safe (CHERI C) userspace. This includes support for both CHERI-RISC-V and Arm's Morello. This means:

• We can host seL4 tasks/programs with referential and spatial safety, but not temporal safety or compartmentalisation, as the required runtimes are not yet available.
• We can host guest VMs (e.g. CheriBSD) that use the full range of CHERI features, including temporal safety and compartmentalisation.

There are two released variants of CHERI-seL4, running on more than 10 platforms:

1. Current community development project (CHERI Alliance): Provides simplified and minimal CHERI support, aiming to encourage reproducibility, industrial adoption, ease of formal verification of the CHERI extensions and their minimal changes to the upstream seL4 microkernel, and upstreaming efforts. This variant currently supports Morello and the RVY CHERI-RISC-V draft standard, which is intended to become part of the RISC-V CHERI extension standard developed by RISC-V International. There is an end-to-end software release including Microkit and CHERI Exercises. The main targets are QEMU, CVA6-CHERI (Ariane), and Morello.
   
2. Initial research prototype (Capabilities Limited): Explored research ideas and design-space trade-offs. For example, we ported the seL4 microkernel to execute in both hybrid and pure-capability CHERI modes and explored passing capabilities in IPC. This variant included support for Morello (Armv8.2 with CHERI extensions), Cambridge's rich-ISAv9 CHERI-RISC-V, and RVY CHERI-RISC-V This variant is no longer maintained but is kept for reference and historical purposes here.

CHERI-seL4 as a hypervisor

This is ongoing early research and is currently experimental. We have demonstrated a proof of concept on Arm's Morello in which CHERI-seL4 runs as a hypervisor and provides strong isolation between virtual machines (VMs). The proof of concept runs memory-safe CheriBSD and CHERI-Linux VMs side-by-side, together with memory-safe VMMs and Microkit runtimes.

Importantly, this is achieved without rewriting the existing software stacks. While CheriBSD and CHERI-Linux require minimal modifications to their kernels to support CHERI, their millions of lines of existing C and C++ software can run with CHERI memory safety. This demonstrates the potential of CHERI to provide memory safety for large, existing software stacks without requiring extensive rewrites.

The goal is to extend CHERI's memory safety across VMs, VMMs, and native seL4 servers and libraries while retaining seL4's strong isolation guarantees between them.