This repository contains a formal model capturing the essential security property of CHERI instruction-set architectures: reachable capability monotonicity. The model defines a small number of instruction-local properties that imply the whole-ISA monotonicity property. This model was used to verify reachable capability monotonicity for the Morello ISA, a CHERI-enabled prototype Arm architecture, but the model should also apply to other CHERI ISAs.
The model, the monotonicity proof, and the instantiation for Morello are described in the paper (available as PDF here):
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter Sewell. In ESOP 2022.
The model/lem directory contains the definitions of the
instruction-local properties, written in the Lem language.
The Properties.thy file in the
model/isabelle directory contains the monotonicity proof
for any ISA satisfying the instruction-local properties, mechanised in the
Isabelle interactive theorem prover.
The other files in the model/isabelle directory contain
proof infrastructure for verifying the instruction-local properties for a
concrete ISA, and the tools directory contains a tool for
automatically generating helper lemmas about the bulk of an ISA specification
written in the Sail language.
Run make in the top-level directory of this repository to build the lemma
generation tool and translate the Lem files of the model into Isabelle
theories.
See the Morello instantiation of the model for an example of how all these are used.
- Isabelle 2020
- Lem
- Sail (last checked with revision
5d18bd95)
The files in this repository are distributed under the BSD 2-clause licence in
LICENCE.