Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors

Gideon Mohr, Marco Guarnieri, Jan Reineke

TL;DR

The paper tackles the problem of formalizing microarchitectural leakage at the ISA level by proposing a semi-automatic method to synthesize hardware-software leakage contracts directly from RTL designs. It introduces a concrete four-step workflow—contract templates, test-case generation, evaluation, and ILP-based synthesis—and implements it for the RISC-V ISA, applying it to Ibex and CVA6 to derive precise leakage contracts. The results uncover subtle leaks (e.g., alignment, branch timing, and data dependencies) and demonstrate the practicality of the approach, aided by an open-source toolchain. This work enables ISA-level reasoning about security against microarchitectural attacks and provides a reusable framework for extending leakage contracts to other open-source processors and attacker models.

Abstract

Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction at the instruction set architecture (ISA) level that captures microarchitectural leakage. Hardware-software leakage contracts have recently been proposed as such an abstraction. In this paper, we propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. For a given ISA, our approach relies on human experts to (a) capture the space of possible contracts in the form of contract templates and (b) devise a test-case generation strategy to explore a microarchitecture's potential leakage. For a given implementation of an ISA, these two ingredients are then used to automatically synthesize the most precise leakage contract that is satisfied by the microarchitecture. We have instantiated this methodology for the RISC-V ISA and applied it to the Ibex and CVA6 open-source processors. Our experiments demonstrate the practical applicability of the methodology and uncover subtle and unexpected leaks.

Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors

TL;DR

The paper tackles the problem of formalizing microarchitectural leakage at the ISA level by proposing a semi-automatic method to synthesize hardware-software leakage contracts directly from RTL designs. It introduces a concrete four-step workflow—contract templates, test-case generation, evaluation, and ILP-based synthesis—and implements it for the RISC-V ISA, applying it to Ibex and CVA6 to derive precise leakage contracts. The results uncover subtle leaks (e.g., alignment, branch timing, and data dependencies) and demonstrate the practicality of the approach, aided by an open-source toolchain. This work enables ISA-level reasoning about security against microarchitectural attacks and provides a reusable framework for extending leakage contracts to other open-source processors and attacker models.

Abstract

Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction at the instruction set architecture (ISA) level that captures microarchitectural leakage. Hardware-software leakage contracts have recently been proposed as such an abstraction. In this paper, we propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. For a given ISA, our approach relies on human experts to (a) capture the space of possible contracts in the form of contract templates and (b) devise a test-case generation strategy to explore a microarchitecture's potential leakage. For a given implementation of an ISA, these two ingredients are then used to automatically synthesize the most precise leakage contract that is satisfied by the microarchitecture. We have instantiated this methodology for the RISC-V ISA and applied it to the Ibex and CVA6 open-source processors. Our experiments demonstrate the practical applicability of the methodology and uncover subtle and unexpected leaks.
Paper Structure (24 sections, 1 equation, 3 figures, 3 tables)

This paper contains 24 sections, 1 equation, 3 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Instruction Set Architectures
  4. Microarchitectures
  5. Microarchitectural Attackers
  6. Hardware-Software Leakage Contracts
  7. Contract-Synthesis Methodology
  8. Contract Templates
  9. Test-Case Generation
  10. Test-Case Evaluation
  11. Contract Synthesis
  12. Refinement of the Contract Template
  13. Instantiating the Methodology for RISC-V
  14. RISC-V Contract Template
  15. Test-Case Generation
  16. ...and 9 more sections

Figures (3)

  • Figure 1: High-level steps of our contract-synthesis methodology.
  • Figure 2: Precision of contracts (y-axis) w.r.t. 2,000,000 test cases for different contract templates starting from the base contract (IL+RL+ML) depending on the number of test case (x-axis) used for contract synthesis.
  • Figure 3: Sensitivity of contracts (y-axis) w.r.t. 2,000,000 test cases using the full contract template (IL+RL+ML+AL+BL+DL) depending on the number of test cases (x-axis) used for contract synthesis. Note the logarithmic x-axis.