top of page
Abstract Shape

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.

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.

Screenshot 2025-01-21 at 10.55.04.png
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

Screenshot 2024-11-03 at 13.24.40.png
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:

Screenshot 2025-01-21 at 11.00.28.png
How

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

Screenshot 2025-01-21 at 11.04.38.png
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.

Screenshot 2025-01-21 at 11.08.18.png
bottom of page