Repository logo
 

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture

Simple item page
cam.depositDate2022-02-01
cam.orpheus.counter87*
dc.contributor.authorBauereiss, Thomas
dc.contributor.authorCampbell, Brian
dc.contributor.authorSewell, Thomas
dc.contributor.authorArmstrong, Alasdair
dc.contributor.authorEsswood, Lawrence
dc.contributor.authorStark, Ian
dc.contributor.authorBarnes, Graeme
dc.contributor.authorWatson, Robert NM
dc.contributor.authorSewell, Peter
dc.contributor.orcidSewell, Thomas [0000-0002-4891-0797]
dc.contributor.orcidSewell, Peter [0000-0001-9352-1013]
dc.date.accessioned2022-02-03T00:30:21Z
dc.date.available2022-02-03T00:30:21Z
dc.date.updated2022-02-01T17:34:02Z
dc.description.abstractMemory 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.
dc.description.sponsorshipThis work was supported by the UK Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694), EPSRC programme grant EP/K008528/1 REMS, ERC AdG 789108 ELVER, Arm iCASE awards, EPSRC IAA KTF funds, the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm, Google, Google DeepMind, HP Enterprise, and the Gates Cambridge Trust. Approved for public release; distribution is unlimited. This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 ("CTSRD"), FA8750-11-C-0249 ("MRC2"), HR0011-18-C-0016 ("ECATS"), and FA8650-18-C-7809 ("CIFV"), as part of the DARPA CRASH, MRC, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.
dc.identifier.doi10.17863/CAM.80993
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/333576
dc.language.isoeng
dc.publisher.departmentDepartment of Computer Science And Technology
dc.rightsAll Rights Reserved
dc.rights.urihttp://www.rioxx.net/licenses/all-rights-reserved
dc.titleVerified Security for the Morello Capability-enhanced Prototype Arm Architecture
dc.typeConference Object
dcterms.dateAccepted2021-12-22
prism.publicationNameAdvanced Research in Computing and Software Science (ARCoSS)
pubs.conference-finish-date2022-04-07
pubs.conference-nameEuropean Symposium on Programming
pubs.conference-start-date2022-04-02
pubs.licence-display-nameApollo Repository Deposit Licence Agreement
pubs.licence-identifierapollo-deposit-licence-2-1
rioxxterms.versionAM
rioxxterms.versionofrecord10.17863/CAM.80993

Files

Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
top.pdf
Size:
455.07 KB
Format:
Adobe Portable Document Format
Description:
Accepted version
Licence
http://www.rioxx.net/licenses/all-rights-reserved
Download

Collections

Cambridge University Research Outputs