Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts

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

16 Downloads (Pure)

Abstract

Progress has recently been made on specifying instruction set architectures (ISAs) in executable formalisms rather than through prose.
However, to date, those formal specifications are limited to the functional aspects of the ISA and do not cover its security guarantees.
We present a novel, general method for formally specifying an ISA's security
guarantees to (1) balance the needs of ISA implementations (hardware) and clients (software), (2) can be semi-automatically verified to hold for the ISA operational semantics, producing a high-assurance mechanically-verifiable proof, and (3) support informal and formal reasoning about security-critical software in the presence of adversarial code.
Our method leverages universal contracts: software contracts that express bounds on the authority of arbitrary untrusted code.
Universal contracts can be kept agnostic of software abstractions, and strike the right balance between requiring sufficient detail for reasoning about software and preserving implementation freedom of ISA designers and CPU implementers.
We semi-automatically verify universal contracts against Sail implementations of ISA semantics using our Katamaran tool; a semi-automatic separation logic verifier for Sail which produces machine-checked proofs for successfully verified contracts.
We demonstrate the generality of our method by applying it to two ISAs that offer very different security primitives: (1) MinimalCaps: a custom-built capability machine ISA and (2) a (somewhat simplified) version of RISC-V with PMP.
We verify a femtokernel using the security guarantee we have formalized for RISC-V with PMP.
Original languageEnglish
Title of host publicationCCS '23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
PublisherACM
Pages2083–2097
Number of pages15
ISBN (Electronic)979-8-4007-0050-7
DOIs
Publication statusPublished - 21 Nov 2023
EventACM Conference on Computer and Communications Security - Tivoli Congress Center, Copenhagen, Denmark
Duration: 26 Nov 202330 Nov 2023
Conference number: 2023
https://www.sigsac.org/ccs/CCS2023/index.html

Publication series

NameCCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security

Conference

ConferenceACM Conference on Computer and Communications Security
Abbreviated titleCCS
Country/TerritoryDenmark
CityCopenhagen
Period26/11/2330/11/23
Internet address

Bibliographical note

Funding Information:
This research was partially funded by the Research Fund KU Leuven, by the Flemish Research Programme Cybersecurity and by a European Research Council (ERC) Starting Grant (UniversalContracts; 101040088), funded by the European Union. Views and opinions expressed are, however, those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. We thank Thomas Van Strydonck for his help gathering statistics and Denis Carnier for proof-reading.

Publisher Copyright:
© 2023 Copyright held by the owner/author(s). Publication rights licensed to ACM

Fingerprint

Dive into the research topics of 'Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts'. Together they form a unique fingerprint.

Cite this