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, Peter Sewell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Memory safety bugs continue to be a major source of security vulnerabilities in our critical infrastructure. The CHERI project has proposed extending conventional architectures with hardware-supported capabilities to enable fine-grained memory protection and scalable compartmentalisation, allowing historically memory-unsafe C and C++ to be adapted to deterministically mitigate large classes of vulnerabilities, while requiring only minor changes to existing system software sources. Arm is currently designing and building Morello, a CHERI-enabled prototype architecture, processor, SoC, and board, extending the high-performance Neoverse N1, to enable industrial evaluation of CHERI and pave the way for potential mass-market adoption. However, for such a major new security-oriented architecture feature, it is important to establish high confidence that it does provide the intended protections, and that cannot be done with conventional engineering techniques. In this paper we put the Morello architecture on a solid mathematical footing from the outset. We define the fundamental security property that Morello aims to provide, reachable capability monotonicity, and prove that the architecture definition satisfies it. This proof is mechanised in Isabelle/HOL, and applies to a translation of the official Arm specification of the Morello instruction-set architecture (ISA) into Isabelle. The main challenge is handling the complexity and scale of a production architecture: 62,000 lines of specification, translated to 210,000 lines of Isabelle. We do so by factoring the proof via a narrow abstraction capturing essential properties of arbitrary CHERI ISAs, expressed above a monadic intra-instruction semantics. We also develop a model-based test generator, which generates instruction-sequence tests that give good specification coverage, used in early testing of the Morello implementation and in Morello QEMU development, and we use Arm’s internal test suite to validate our model. This gives us machine-checked mathematical proofs of whole-ISA security properties of a full-scale industry architecture, at design-time. To the best of our knowledge, this is the first demonstration that that is feasible, and it significantly increases confidence in Morello.
Original languageEnglish
Title of host publicationProgramming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings
EditorsIlya Sergey
PublisherSpringer
Pages174-203
Number of pages30
ISBN (Electronic)978-3-030-99336-8
ISBN (Print)978-3-030-99335-1
DOIs
Publication statusPublished - 29 Mar 2022
Event31st European Symposium on Programming - Munich, Germany
Duration: 2 Apr 20227 Apr 2022
Conference number: 31
https://etaps.org/2022/esop

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume13240
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference31st European Symposium on Programming
Abbreviated titleESOP 2022
Country/TerritoryGermany
CityMunich
Period2/04/227/04/22
Internet address

Fingerprint

Dive into the research topics of 'Verified Security for the Morello Capability-enhanced Prototype Arm Architecture'. Together they form a unique fingerprint.

Cite this