I was privileged to join the CHERI research group at Cambridge University as a postdoctoral researcher. As part of the effort to verify that CHERI could be used for more than academic efforts, a large team constructed a CHERI-backed ABI for FreeBSD/MIPS systems, called CheriABI.

This paper provides a relatively thorough overview, complete with pedagogy, design, and experimental observations; a forthcoming tech report will follow along with all the details it was necessary to trim from the conference paper.

The paper won one of four Best Paper awards at ASPLOS’19.

The paper itself is available, as is a lengthier tech report that restores much of the material we had to cut for the conference paper.

Abstract:

The CHERI architecture allows pointers to be implemented as capabilities (rather than integer virtual addresses) in a manner that is compatible with, and strengthens, the semantics of the C language. In addition to the spatial protections offered by conventional fat pointers, CHERI capabilities offer strong integrity, enforced provenance validity, and access monotonicity. The stronger guarantees of these architectural capabilities must be reconciled with the real-world behavior of operating systems, run-time environments, and applications. When the process model, user-kernel interactions, dynamic linking, and memory management are all considered, we observe that simple derivation of architectural capabilities is insufficient to describe appropriate access to memory. We bridge this conceptual gap with a notional abstract capability that describes the accesses that should be allowed at a given point in execution, whether in the kernel or userspace. To investigate this notion at scale, we describe the first adaptation of a full C-language operating system (FreeBSD) with an enterprise database (PostgreSQL) for complete spatial and referential memory safety. We show that awareness of abstract capabilities, coupled with CHERI architectural capabilities, can provide more complete protection, strong compatibility, and acceptable performance overhead compared with the pre-CHERI baseline and software-only approaches. Our observations also have potentially significant implications for other mitigation techniques.

BibTeX:

@InProceedings{brooks:cheriabi19,
  author  = {Brooks Davis and Peter G. Neumann and Robert N. M. Watson and
            Simon W. Moore and Alexander Richardson and John Baldwin and
            David Chisnall and Jessica Clarke and Nathaniel Wesley Filardo
            and Khilan Gudka and Alexandre Joannou and Ben Laurie and A.
            Theodore Markettos and J. Edward Maste and Alfredo Mazzinghi and
            Edward Tomasz Napierala and Robert M. Norton and Michael Roe and
            Peter Sewell and Stacey Son and Jonathan Woodruff},
  title   = {{CheriABI}: Enforcing Valid Pointer Provenance and Minimizing
            Pointer Privilege in the POSIX C Run-time Environment},
  year    = {2019},
  month   = {4},
  booktitle={Proc. of The 24th ACM International Conference on Architectural
            Support for Programming Languages and Operating Systems
            (ASPLOS)},
  note    = {Best Paper Award}
}