Computer Laboratory

CHERI

The (First?) CHERI Microkernel Workshop

On 23 April 2016, adjacent to EuroSys 2016 in London, the University of Cambridge hosted a workshop to investigate potential uses for CHERI in microkernel design. The event included attendees from Cambridge, SRI, ETH Zurich, George Washington University, TU Dresden, ARM, Broadcom, Google, Hewlett Packard Labs, and Oracle, who presented on various current microkernel designs and capability models, the CHERI instruction-set architecture, and potential new directions in operating-system design supported by architectural change.

Presentations

Talk titleSpeaker
Workshop WelcomeRobert N. M. Watson (University of Cambridge)
Introducing CHERIRobert N. M. Watson (University of Cambridge)
CHERI Processor ModelsSimon W. Moore (University of Cambridge)
CHERI: A Hybrid Capability ArchitectureRobert N. M. Watson (University of Cambridge)
Simon W. Moore (University of Cambridge)
CHERI: C/C++-language and compiler supportDavid Chisnall (University of Cambridge)
Khilan Gudka (University of Cambridge)
CheriBSD: Hybrid-Capability OS PrototypeRobert N. M. Watson (University of Cambridge)
CheriABI: A Pure-Capability OS Process EnvironmentBrooks Davis (SRI International)
CheriOS: A CHERI MicrokernelHadrien Barral (University of Cambridge / ENS)
Formally Proving Nonforgeability of Capabilities (work in progress)Peter Sewell (University of Cambridge)
Kyndylan Nienhuis (University of Cambridge)
Rack Scalable OS for The Machine and the Case for CapabilitiesDejan Milojicic (Hewlett Packard Labs)
Caps2: L4Re and CHERIAdam Lackorzynski (TU Dresden)
Hermann Hartig (TU Desden)
The seL4 Capability ModelMatthew Grosvenor (University of Cambridge)
Capabilities in BarrelfishTimothy Roscoe (ETH Zurich)
Language capability modelsBen Laurie (Google)
FirePath operating systemJohn Redford (Broadcom)