Department of Computer Science and Technology

CHERI

CheriBSD

CheriBSD is an adaptation of the open-source FreeBSD operating system to support the CHERI-MIPS, CHERI-RISC-V, and Arm Morello ISAs. We have used CheriBSD to validate a number of hypotheses about the CHERI capability model, including hybridization between MMU-based virtual memory and the in-address-space CHERI capability model, and also C-language hybridization. CheriBSD provides a highly functional operating-system prototype that demonstrates how fine-grained memory protection 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 various 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. A prototype branch implements userspace heap temporal memory safety using capability revocation; we aim to merge this to the CheriBSD main development branch in early 2021. We also have several in-progress prototypes of scalable userspace software compartmentalization based on different software operational models, which should mature over the course of 2021.

Obtaining CheriBSD

The best way to get started with CheriBSD on CHERI-MIPS, CHERI-RISC-V, or on Morello is using our cheribuild tool. 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-MIPS and CHERI-RISC-V, that's QEMU-CHERI. For Morello, it's Arm's Morello FVP model, which cheribuild will download automatically.

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

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

Get started with CheriBSD/Morello in one command line:

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

Get started with CheriBSD/CHERI-MIPS in one command line:

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

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

Running CheriBSD

CheriBSD can be cross compiled from x86 development workstations/servers and booted both on our BERI FPGA 64-bit MIPS ISA soft-core processor and also on QEMU-CHERI, an ISA-level emulation of the CHERI instruction set.

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 are committed to upstreaming pertinent improvements to FreeBSD where sensible, and have already done so for support of the BERI soft-core processor and peripherals, general improvements to MIPS and ARMv8-A support, the RISC-V architecture port, improvements to Clang/LLVM integration, and many other aspects of the open-source OS including QEMU-based ports crossbuilding that we required for our research prototype.