CHERI-seL4 and CHERI-Microkit Released

Hesham Almatary – Capabilities Limited

We are happy to release a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This comes with CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment.

The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s x730 processor, CHERI-Toooba and CHERI-CVA6 on FPGA.

The software release roadmap for CHERI-seL4
Disclaimer:
CHERI-seL4 and CHERI-Microkit are independent research prototypes developed by the CHERI Alliance. They are not affiliated with or endorsed by the seL4 Foundation. seL4 is a trademark of the seL4 Foundation.

Why Try CHERI-seL4

CHERI-seL4: Why?

seL4 is a formally verified microkernel known for enforcing strong isolation between protection domains in separate address spaces. However, seL4 does not currently provide protection between components in the same address space.

CHERI is a hardware capability architecture that enables fine-grained memory safety and compartmentalisation within a single address space. By combining CHERI with seL4, developers can use CHERI to explore new ways to enforce memory-safety in their C/C++ projects/components, at no extra development cost.

This opens up use cases where:

  • Isolation is needed between mixed-trust components without separate address spaces
  • You want hardware enforcement of memory safety for C/C++ userspace
  • You need a lightweight runtime that avoids the complexity of full MMU-based separation

CHERI-seL4 enables all of this with minimal changes to the kernel and no need to rewrite existing C code in managed languages.

What this Release Includes

This initial release provides:

  • A prototype implementation of the CHERI-seL4 RFC discussed with the seL4 community
  • Support for the draft CHERI-RISC-V (Zcheri) architecture
  • Compatibility with Codasip’s x730 processor, CHERI-Toooba and CHERI-CVA6
  • A minimal kernel extension that supports memory-safe CHERI C in userspace while keeping the kernel unchanged when CHERI is disabled
  • CHERI-Microkit: a lightweight framework for running CHERI-enabled and unmodified C/C++ or Rust programs side by side
  • A set of exercises and tutorials to get developers started with CHERI on seL4

About Microkit

Microkit simplifies seL4 development by abstracting away low-level kernel primitives. It allows you to define a static security policy and deploy isolated components without needing to write complex seL4 setup code.

Microkit consists of:

  • A runtime library for applications
  • A monitor (root task) that manages startup
  • A Rust-based build tool that generates the required bootstrapping and system setup logic

CHERI support in Microkit lets you run legacy C/C++ (non-CHERI), memory-safe C/C++ (using CHERI capabilities), and Rust programs in distinct protection domains.

Try it Out

All code for CHERI-seL4, CHERI-Microkit and CHERI-seL4 Exercises is available as open source. The tutorials walk through how to build and run the system, and include example code to test different features.

This is a prototype release and the CHERI-RISC-V standard is still in draft. The focus is on enabling experimentation and early development.

To run the CHERI-Microkit system on QEMU, start by installing the following dependencies (Ubuntu example):

Install dependencies (Ubuntu example):

				
					# Install cheribuild dependencies:

sudo apt install autoconf automake libtool pkg-config clang bison cmake mercurial ninja-build samba flex texinfo time libglib2.0-dev libpixman-1-dev libarchive-dev libarchive-tools libbz2-dev libattr1-dev libcap-ng-dev libexpat1-dev libgmp-dev bc


# Install Microkit dependencies (Rust and XML tools):

curl https://sh.rustup.rs -sSf | sh
rustup target add x86_64-unknown-linux-musl
sudo apt install libxml2-utils


# Clone and build:

git clone https://github.com/CTSRD-CHERI/cheribuild.git -b std-cheri-riscv-microkit

cd cheribuild
./cheribuild.py cheri-microkit-baremetal-riscv64-zpurecap -d

Run tests and examples:

				
					./cheribuild.py cheri-microkit-baremetal-riscv64-zpurecap --build-and-test

CHERI-seL4 Tutorials and Exercises

You can find the CHERI-seL4 Exercises here, with extensive documentation, instructions, scripts, and source code.

Feedback Welcome

We welcome contributions, questions and feedback. If you run into issues, have feature requests or want to help shape future development, please get in touch. The CHERI-RISC-V standard is still being finalised and we encourage developers to share feedback while it is still open to changes.

Resources