Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts

Sander Huyghebaert, Steven Keuchel, Coen De Roover, Dominique Devriese

TL;DR

The paper addresses the lack of formal security guarantees in executable ISA specifications and proposes a general, tool-supported method based on universal contracts to express ISA security properties independent of software abstractions. It introduces Katamaran, a semi-automatic Iris-based verifier for µSail, enabling verification of universal contracts against Sail semantics and official ISA semantics, demonstrated on MinimalCaps and RISC-V PMP. The authors show end-to-end applicability by verifying a femtokernel that relies on PMP guarantees, and provide a quantitative evaluation of verification effort and automation. The work promises robust, scalable reasoning about security-critical software interacting with untrusted code, supporting ISA evolution without compromising declared guarantees, and guiding secure ISA design and verification in practice.

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 ISAs 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.

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts

TL;DR

The paper addresses the lack of formal security guarantees in executable ISA specifications and proposes a general, tool-supported method based on universal contracts to express ISA security properties independent of software abstractions. It introduces Katamaran, a semi-automatic Iris-based verifier for µSail, enabling verification of universal contracts against Sail semantics and official ISA semantics, demonstrated on MinimalCaps and RISC-V PMP. The authors show end-to-end applicability by verifying a femtokernel that relies on PMP guarantees, and provide a quantitative evaluation of verification effort and automation. The work promises robust, scalable reasoning about security-critical software interacting with untrusted code, supporting ISA evolution without compromising declared guarantees, and guiding secure ISA design and verification in practice.

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 ISAs 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.
Paper Structure (19 sections, 14 equations, 15 figures, 2 tables)

This paper contains 19 sections, 14 equations, 15 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Separation Logic
  4. Capability Machines
  5. RISC-V PMP
  6. ISA specifications in Sail
  7. Security Guarantees as Universal Contracts
  8. Capability Safety for MinimalCaps
  9. Memory Integrity for RISC-V PMP
  10. Verifying and applying a Universal Contract
  11. Katamaran
  12. Verification of Universal Contracts using Katamaran
  13. MinimalCaps
  14. RISC-V PMP
  15. Evaluation
  16. ...and 4 more sections

Figures (15)

  • Figure 1: Concept of a capability
  • Figure 2: An example RISC-V PMP policy in Top-of-Range mode (TOR).
  • Figure 3: $\mathit{fdeCycle}$ and $\mathit{fdeStep}$ definitions as found in Sail specifications.
  • Figure 4: Sail specification of the store instruction of our capability machine (simplified).
  • Figure 5: Logical relations for capability safety
  • ...and 10 more figures