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

Displayed time zone: Pacific Time (US & Canada) change

05:00 - 07:00
REMS-DeepSpec Session 4REMS-DeepSpec at REMS/DeepSpec live stream
Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Thomas Bauereiss University of Cambridge, Kyndylan Nienhuis University of Cambridge, Alexandre Joannou University of Cambridge, Anthony Fox University of Cambridge, UK, Michael Roe University of Cambridge, Brian Campbell University of Edinburgh, Matthew Naylor University of Cambridge, Robert M. Norton University of Cambridge, Simon W. Moore University of Cambridge, Peter G. Neumann SRI International, Ian Stark The University of Edinburgh, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge
File Attached
Katamaran: semi-automated verification of ISA specifications
Steven Keuchel , Georgy Lukyanov Newcastle University, UK, Dominique Devriese Vrije Universiteit Brussel
File Attached