Department of Computer Science and Technology

CHERI

CheriBSD

CheriBSD is an adaptation of the open-source FreeBSD operating system to support CHERI-RISC-V and Arm Morello in emulation and on hardware. We have used CheriBSD to validate a number of hypotheses about the CHERI capability model, including hybridization between MMU-based virtual memory the in-address-space CHERI capability model, C/C++-language hybridization with strong memory safety, and scalable software compartmentalization. CheriBSD provides a highly functional operating-system prototype that demonstrates how CHERI support can be composed with a conventional OS design.

The CheriBSD kernel and userspace both support pure-capability CHERI C/C++: they can be compiled to implement strong capability-based referential and spatial memory protection. This includes continuous validation of pointer provenance, pointer bounds checking on code, the heap, the stack, and global variables, as well as pointer permission checking. The kernel has been extended to implement tag support in virtual memory, capability context switching, and capability-extended interfaces including debugging.

Our memory-safe userspace process environment is known as CheriABI, and extends the system-call and other ABIs to implement pointers as capabilities universally, rather than using an integer type. Support for CHERI library compartmentalization appeared in 2022, and support for co-process compartmentalization will be released in 2023. Heap temporal memory safety using capability revocation has been merged into the CheriBSD "dev" branch as of 2023, and will appear in the CheriBSD 23.11 software release. We are also developing integrated tooling for capability tracing and debugging.

CheriBSD resources

The main resource for CheriBSD is the CheriBSD website where you can download source code and pre-built releases, and also find documentation and support.

The document Getting Started with CheriBSD guide provides step-by-step installation instructions for Morello boards, gets you up and running with a CHERI-enabled "hello world", and provides support information for CheriBSD.

Building and running CheriBSD

CheriBSD can be cross compiled from x86 development workstations/servers and booted on our FPGA 64-bit CHERI-RISC-V ISA soft-core processors, on QEMU-CHERI, an ISA-level emulation of the CHERI-RISC-V and Morello instruction sets and on an Arm Morello board.

We provide prebuilt installer images and third-party packages for CheriBSD on Morello, which can be downloaded from the CheriBSD website. Follow the installation directions in the Getting Started with CheriBSD user guide.

For CheriBSD on CHERI-RISC-V, the best way to build and run CheriBSD is using our cheribuild tool. This tool can also be used to crossbuild CheriBSD images for Morello. cheribuild will download any necessary source code, build our cross-development environment, the OS itself, and any necessary emulators, create disk images, and run the emulation tool. For CHERI-RISC-V and Morello, that's QEMU-CHERI. For Morello, you can also choose Arm's Morello FVP model, which cheribuild will download automatically if using run-fvp-morello-purecap in place of the target below.

Get started with emulating CheriBSD/CHERI-RISC-V in one command line:

./cheribuild.py --include-dependencies run-riscv64-purecap

Get started with emulating CheriBSD/Morello in one command line:

./cheribuild.py --include-dependencies run-morello-purecap

By default images created by cheribuild can be logged into as root with no password.

The CheriBSD prototype source code can be found in the CheriBSD GitHub repository. We also use a GitHub issue tracker to track bugs and feature requests for CheriBSD.

Papers and documentation

CheriBSD was used as the foundation OS for our various publications at ISCA 2014, ASPLOS 2015, IEEE S&P 2015, ASPLOS 2019, and Oakland 2020 papers on CHERI memory protection, which can be found on the CHERI publications list.

Our paper on CheriABI explains CheriBSD's memory-safe process environment. The CHERI C/C++ Programming Guide introduces the CHERI variants of C and C++ that run in that process environment.

We have also published papers in open-source venues such as BSDCan, AsiaBSDCon, and FreeBSD Journal on how we built and support a long-running derivative research operating system based on FreeBSD.

Open-source research methodology

Our complete CHERI software stack including compiler and operating-system prototype are developed as open source. We have upstreamed non-CHERI-specific improvements wherever possible, including FreeBSD's RISC-V architecture port, improvements to FreeBSD's 64-bit Arm port, and numerous improvements to Clang/LLVM, QEMU, and other open-source packages.