Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Tue 16 Jun 2020 05:00 - 05:40 at REMS/DeepSpec live stream - REMS-DeepSpec Session 4

Joint work with Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell

Memory safety bugs are still a major source of security vulnerabilities. CHERI aims to address this by extending commodity instruction set architectures with hardware support for capabilities, enabling fine-grained memory protection and scalable software compartmentalisation while maintaining performance. CHERI was initially developed as a MIPS extension, but work on versions for RISC-V and ARM is underway.

The integration of such a security mechanism into hardware architectures requires high confidence in its correctness: one bug in the mechanism or its interaction with other architecture features can lead to security vulnerabilities in all implementations of the architecture. This makes machine-checked statements and proofs of the intended security properties essential.

In this talk, we discuss our formal models of production-scale ISAs with CHERI extensions, as well as our formalisation of key security properties of those ISAs. In particular, these properties establish bounds on which capabilities arbitrary code can construct from an initial set of capabilities. As a use case of the capability mechanism, we discuss the isolation of a software compartment. The properties and the isolation scenario have been formalised and verified using the interactive theorem prover Isabelle/HOL w.r.t. a model of the complete CHERI-MIPS ISA. Work on verifying the properties for prototypes of CHERI-RISC-V and CHERI-ARM is ongoing.

Slides (pres.pdf)2.11MiB

Tue 16 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change

05:00 - 07:00: REMS-DeepSpec Session 4REMS-DeepSpec at REMS/DeepSpec live stream
05:00 - 05:40
Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Thomas BauereissUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Alexandre JoannouUniversity of Cambridge, Anthony FoxUniversity of Cambridge, UK, Michael RoeUniversity of Cambridge, Brian CampbellUniversity of Edinburgh, Matthew NaylorUniversity of Cambridge, Robert M. NortonUniversity of Cambridge, Simon W. MooreUniversity of Cambridge, Peter G. NeumannSRI International, Ian StarkThe University of Edinburgh, Robert N. M. WatsonUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached
05:50 - 06:30
Katamaran: semi-automated verification of ISA specifications
Steven Keuchel, Georgy LukyanovNewcastle University, UK, Dominique DevrieseVrije Universiteit Brussel
File Attached