Repository logo
 

Verified security properties for the capability-enhanced CHERI-MIPS architecture

Simple item page
cam.depositDate2022-04-04
cam.restrictionthesis_access_open
cam.supervisorSewell, Peter
dc.contributor.authorNienhuis, Kyndylan
dc.date.accessioned2022-04-06T16:51:47Z
dc.date.available2022-04-06T16:51:47Z
dc.date.submitted2021-09-01
dc.date.updated2022-04-04T12:39:46Z
dc.description.abstractDespite decades of research, the computer industry still struggles to build secure systems. The majority of security vulnerabilities are caused by a combination of two fundamental problems. First, mainstream engineering methods are not suited to find small bugs in corner cases. Second, mainstream hardware architectures and C/C++ language abstractions provide only coarse-grained memory protection, which lets these small bugs escalate to serious security vulnerabilities. CHERI, the context of our work, is an ongoing research project that addresses the second problem with hardware support for fine-grained memory protection and scalable software compartmentalisation. CHERI achieves this by extending commodity hardware architectures with a capability system, in which all memory accesses must be authorised by a capability. Capabilities are unforgeable tokens that contain address bounds and permissions, determining the memory region and the types of accesses they can authorise. They can be passed around and manipulated only in specific ways. CHERI has been initially developed as CHERI-MIPS, with later work on CHERI-RISC-V. In this thesis, we address the first problem in the context of CHERI: we formally state and prove security properties for the CHERI-MIPS architecture. Our first set of security properties forms a new abstraction layer of CHERI-MIPS, explaining execution steps in terms of nine abstract actions, one for each kind of memory access, capability manipulation, and security domain transition. We use this abstraction to reason about arbitrary code: we characterise which capabilities can be accessed or constructed by potentially compromised or malicious code and which memory locations it can overwrite until it transitions to another security domain. We use this to prove the correctness of a simple compartmentalisation scenario, in which CHERI’s capability system is used to isolate a component from the rest of the system. Our results are based on a full, non-idealised, sequential specification of CHERI-MIPS, which is complete enough to boot an operating system. The challenges of proving our properties include the size of the architecture, its easy-to-miss corner cases, and the fact that the architecture keeps evolving. As a step towards CHERI’s industrial adoption, the Morello program is developing the eponymous prototype CHERI extension of the Armv8-A architecture, along with a processor implementation, development board, and software. Building on our work, the formal verification of architectural security properties is an important part of this program.
dc.description.sponsorshipGates Cambridge Trust, Computer Laboratory, EPSRC programme grant EP/K008528/1 (REMS: Rigorous Engineering for Mainstream Systems), European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement 789108, ELVER), and the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8650-18-C-7809 (CIFV). The views, opinions, and/or findings contained in this paper are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government.
dc.identifier.doi10.17863/CAM.83267
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/335835
dc.language.isoeng
dc.publisher.institutionUniversity of Cambridge
dc.rightsAll Rights Reserved
dc.rights.urihttps://www.rioxx.net/licenses/all-rights-reserved/
dc.subjectformal verification
dc.subjectcapability systems
dc.subjectCHERI
dc.titleVerified security properties for the capability-enhanced CHERI-MIPS architecture
dc.typeThesis
dc.type.qualificationlevelDoctoral
dc.type.qualificationnameDoctor of Philosophy (PhD)
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/K008528/1)
pubs.licence-display-nameApollo Repository Deposit Licence Agreement
pubs.licence-identifierapollo-deposit-licence-2-1
rioxxterms.licenseref.urihttps://www.rioxx.net/licenses/all-rights-reserved/
rioxxterms.typeThesis

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Verified security properties for the capability-enhanced CHERI-MIPS architecture.pdf
Size:
2.65 MB
Format:
Adobe Portable Document Format
Description:
Thesis
Licence
https://www.rioxx.net/licenses/all-rights-reserved/
Download

Collections

Theses - Computer Science and Technology