CHERI

CHERI-seL4

This is an ongoing project that aims to combine seL4's security realised by formal verification and CHERI's memory safety and software compartmentalisation at user-level. The end goal is to have a fully enhanced and secure, memory-safe system down from the kernel and/or hypervisor-level (seL4), to VMs (e.g., CheriBSD or CHERI-Linux), and seL4's native OS libraries, VMMs, and applications.

Current status

Currently, we have released a CHERI-aware seL4 kernel that can be built and run in CHERI C (purecap) mode. This includes Morello and CHERI-RISC-V support. 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.

More details could be found at this seL4 RFC, and our CHERI-seL4 kernel fork.