Department of Computer Science and Technology

CHERI

CheriBSD

CheriBSD is an adaptation of the open-source FreeBSD operating system to support the CHERI-MIPS ISA. 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 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. Many parts of the CheriBSD userspace can operate with strong spatial protection, including continuous validation of pointer provenance, pointer bounds checking, pointer permissions checking, and fine-grained compartmentalization. The kernel initializes and maintains capability-register state for kernel and user threads, has a virtual-memory subsystem extended to support tagged memory, has a special system-call ABI adapted to use capabilities instead of pointers ("CheriABI"), as well as other extensions to debugging interfaces, signals, etc, to support userspace memory protection using CHERI.

Obtaining CheriBSD

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, and IEEE S&P 2015 on CHERI memory protection, which can be found on the CTSRD publications page.

Implementation and user information can be found on the CHERI Programmer's Guide.

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 support, 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.