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 title | Speaker |
|---|---|
| Workshop Welcome | Robert N. M. Watson (University of Cambridge) |
| Introducing CHERI | Robert N. M. Watson (University of Cambridge) |
| CHERI Processor Models | Simon W. Moore (University of Cambridge) |
| CHERI: A Hybrid Capability Architecture | Robert N. M. Watson (University of
Cambridge) Simon W. Moore (University of Cambridge) |
| CHERI: C/C++-language and compiler support | David Chisnall (University of Cambridge) Khilan Gudka (University of Cambridge) |
| CheriBSD: Hybrid-Capability OS Prototype | Robert N. M. Watson (University of Cambridge) |
| CheriABI: A Pure-Capability OS Process Environment | Brooks Davis (SRI International) |
| CheriOS: A CHERI Microkernel | Hadrien 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 Capabilities | Dejan Milojicic (Hewlett Packard Labs) |
| Caps2: L4Re and CHERI | Adam Lackorzynski (TU Dresden) Hermann Hartig (TU Desden) |
| The seL4 Capability Model | Matthew Grosvenor (University of Cambridge) |
| Capabilities in Barrelfish | Timothy Roscoe (ETH Zurich) |
| Language capability models | Ben Laurie (Google) |
| FirePath operating system | John Redford (Broadcom) |