PaperlayerView exact revision on arXiv

Source-linked AI summary

Hardware-Software Contracts for Secure Speculation

Marco Guarnieri, Boris Köpf, Jan Reineke, Pepe Vila

arXiv:2006.03841v3cs.CR

TL;DR

Secure speculation presents a trade-off between defensive strength and performance, but the intuition lacks a framework for specifying hardware-software contracts. This paper formalizes and compares hardware guarantees, derives software properties for constant-time programming and sandboxing, and shows how to automate checks for secure programs.

  • Problem

    Secure speculation trades stronger defensive mechanisms and broader program coverage against performance, while lacking a structured way to specify hardware-software contracts.

    Source: §I · p. 1

  • Method

    The framework specifies contracts using an ISA language, a microarchitecture model, and an adversary model, then derives program-level properties for constant-time programming and sandboxing.

    Source: §I · pp. 1–2, §IV · p. 5

  • Results

    The defined contracts form a lattice for rigorous comparison of secure-speculation mechanisms, and the studied mechanisms prevent leaks of speculatively accessed data.

    Source: §I · p. 2

  • Takeaways & Limitations

    The framework characterizes secure programming in constant-time and sandboxing scenarios and supports automated checks for programs on these mechanisms.

    Source: §I · p. 2, §IX · p. 14

Abstract

from arXiv · show

Since the discovery of Spectre, a large number of hardware mechanisms for secure speculation has been proposed. Intuitively, more defensive mechanisms are less efficient but can securely execute a larger class of programs, while more permissive mechanisms may offer more performance but require more defensive programming. Unfortunately, there are no hardware-software contracts that would turn this intuition into a basis for principled co-design. In this paper, we put forward a framework for specifying such contracts, and we demonstrate its expressiveness and flexibility. On the hardware side, we use the framework to provide the first formalization and comparison of the security guarantees provided by a representative class of mechanisms for secure speculation. On the software side, we use the framework to characterize program properties that guarantee secure co-design in two scenarios traditionally investigated in isolation: (1) ensuring that a benign program does not leak information while computing on confidential data, and (2) ensuring that a potentially malicious program cannot read outside of its designated sandbox. Finally, we show how the properties corresponding to both scenarios can be checked based on existing tools for software verification, and we use them to validate our findings on executable code.

I. INTRODUCTION

The introduction motivates hardware-software contracts as a way to formalize secure-speculation guarantees and connect them to program requirements. It presents a framework for comparing hardware protections and characterizing software security in constant-time programming and sandboxing.

I. INTRODUCTION

  • The paper addresses the lack of contracts for characterizing hardware guarantees and showing how software can leverage them for end-to-end security.The framework is intended to formalize the trade-off between hardware protection and the defensive programming required of software.Source: §I · p. 1
  • Contracts define observable executions against which hardware guarantees are stated, using an ISA language, a microarchitecture model, and an adversary model.The adversary model specifies which microarchitectural components, such as caches or branch-predictor state, are observable via side channels.Source: §I · p. 1
  • The framework identifies program properties for constant-time programming and sandboxing, and supports automated checks of programs for both scenarios.Constant-time programming protects confidential data computed on by a benign program; sandboxing restricts which memory a potentially malicious program can read.Source: §I · p. 2
  • The hardware analysis formalizes mechanisms against an adversary observing caches, predictors, and part of the reorder buffer, then compares their guarantees using a lattice of contracts.It characterizes mechanisms including disabled speculation, delayed speculative loads, and speculative taint tracking.Source: §I · p. 2

A. ISA language

  • The paper models programs in µASM, whose instructions include assignments, memory operations, jumps, branches, and a speculation barrier.Programs are instruction sequences; the architectural semantics represents states with memory and register assignments and defines runs from initial to final states.Source: A. ISA language · p. 2

B. Architectural semantics →

  • Architectural semantics maps each state to a successor, and a run is a finite sequence from an initial state to a final state where pc = ⊥.Initial states assign 0 to all registers, including pc.Source: B. Architectural semantics → · p. 2

C. Hardware semantics ⇒

The framework models hardware execution and adversary observations, then specifies contracts that divide side-channel security responsibilities between hardware and software. Its contracts expose different observations and execution paths, allowing hardware guarantees to be compared and software requirements to be stated against them.

C. Hardware semantics ⇒

  • A hardware semantics steps deterministically between states containing architectural state and microarchitectural state, including predictors, caches, and the reorder buffer.The paper assumes a fixed initial microarchitectural state, such as an empty reorder buffer and invalidated caches.Source: C. Hardware semantics ⇒ · p. 3

D. Adversary model

  • The adversary model projects hardware states onto observable components; the paper considers caches, predictors, and part of the reorder buffer.A program’s hardware trace is the sequence of these projected observations during its run.Source: D. Adversary model · p. 3

A. Formalizing contracts

  • A contract is a labeled deterministic ISA semantics whose traces specify when executions must be indistinguishable to an attacker.Hardware satisfies a contract when matching contract traces imply matching hardware-observation traces for every program and pair of initial states.Source: A. Formalizing contracts · p. 3

B. Contracts for secure speculation

1) Building blocks for contracts:

  • Observer modes determine what is exposed, while execution modes determine which paths are explored, including bounded mispredicted paths before rollback.The constant-time observer exposes the program counter and memory-access addresses; the architectural observer also exposes loaded values.Source: 1) Building blocks for contracts · p. 3
  • Recent secure-speculation proposals still violate the sequential constant-time contract, while speculative out-of-order processors satisfy the speculative constant-time contract.The architectural contract also guarantees confidentiality for data loaded only transiently, providing software an interface based on transient noninterference.Source: 1) Building blocks for contracts · p. 4

5) Special contracts:

The paper orders contracts by the security guarantees they provide and proves that satisfaction transfers from stronger contracts to weaker ones. This makes stronger-contract platforms compatible with code secured under weaker contracts.

5) Special contracts:

  • A contract is stronger when agreement under its traces implies agreement under the weaker contract’s traces; fewer exposed labels can therefore indicate stronger guarantees.The lattice places the no-observation contract at the top and the entire-architectural-state contract at the bottom.Source: C. A lattice of contracts · p. 4, Figure 4 · p. 5
  • If a hardware platform satisfies a contract, it also satisfies every weaker contract.This follows from the contract-strength ordering.Source: C. A lattice of contracts · pp. 4–5
  • Stronger-contract processors can securely execute side-channel-resilient legacy code that was secure under weaker contracts.This is the paper’s backward-compatibility consequence of satisfaction transferring to weaker contracts.Source: C. A lattice of contracts · p. 5

IV. PROGRAMMING AGAINST CONTRACTS

The paper characterizes secure programming as noninterference under a contract, then applies that framework to confidential-data processing and sandboxing. For sandboxing, vanilla bounds checks must be paired with weak speculative noninterference to guarantee the broader property.

A. Secure programming

  • For constant-time programming, low-equivalent initial states must produce identical contract traces, preventing high-memory information from leaking through those traces.If the hardware satisfies that contract, the program is also non-interferent at the hardware-observation level.Source: A. Secure programming · p. 5

B. Sandboxing

  • General sandboxing requires both vanilla sandboxing and noninterference under the contract, so outside-sandbox data cannot affect adversary observations on a platform satisfying it.Vanilla sandboxing alone prevents architectural accesses to high memory; general sandboxing additionally addresses covert channels.Source: B. Sandboxing · pp. 5–6
  • A vanilla-sandboxed program that also satisfies wSNI is generally sandboxed; checking both properties therefore establishes general sandboxing.The paper presents wSNI as a bridge between vanilla and general sandboxing.Source: B. Sandboxing · p. 6

C. Constant-time programming

The section distinguishes traditional constant-time from the stronger contract-relative property, using speculative non-interference to bridge them. Experiments illustrate how outcomes vary across contracts for sandboxing and constant-time programs.

C. Constant-time programming

  • Traditional constant-time excludes secret-dependent control flow, memory accesses, and inputs to variable-latency instructions, but modern processors require reasoning beyond this architectural view.The section characterizes general-constant-time as non-interference with respect to a contract.Source: C. Constant-time programming · p. 6
  • Vanilla-constant-time together with SNI implies general-constant-time, allowing existing vanilla checks to be paired with an SNI check.The section proposes using vanilla-constant-time tools and then checking SNI to bridge the gap.Source: C. Constant-time programming · p. 6
  • The sequential architectural contract is inadequate for constant-time programming because non-interference under it can preclude accessing secret data, which constant-time code must compute on.Source: C. Constant-time programming · p. 6

D. Experiments

  • The experiments use eight small x86 programs and an enhanced Spectector to check SNI and wSNI across contracts; the results support a two-step verification path.That path checks vanilla sandboxing or constant-time first, then wSNI or SNI with Spectector.Source: D. Experiments · pp. 6–7
  • P1 fails wSNI under J·Kspec_ct but satisfies it under J·Kseq-spec_ct-pc; P′1 violates wSNI under J·Kspec_ct-pc, while fenced variants satisfy wSNI under J·Kspec_ct.The reported counterexamples show that the respective programs are not sandboxed under those contracts.Source: D. Experiments · p. 7
  • P2 violates SNI under J·Kspec_ct but satisfies it under J·Kseq-spec_ct-pc; P′2 violates SNI under both contracts, while fenced P2 and P′2 satisfy SNI under both.Source: D. Experiments · p. 7

V. MODELING MICROARCHITECTURE AND ADVERSARIES

The section introduces a microarchitectural semantics for modeling speculative, out-of-order execution. It aims to capture key execution features while remaining simple and supporting varied caches and branch predictors.

V. MODELING MICROARCHITECTURE AND ADVERSARIES

  • The semantics models µASM execution on a simple out-of-order processor with a unified instruction and data cache and branch prediction for speculative execution.Source: §V · p. 7
  • Its design goals are to capture key speculative and out-of-order features, remain simple, and support broad classes of caches and branch predictors.Source: §V · p. 7
  • The section formalizes hardware configurations, pipeline steps, and the adversary used in the security analysis.Source: §V · p. 7

A. Hardware configurations

Hardware configurations combine architectural and microarchitectural state, while the semantics models pipeline execution and component interactions. Its fetch rules account for instruction order, branch prediction, and cache misses.

A. Hardware configurations

  • A hardware configuration pairs architectural state with microarchitectural state, which includes the reorder buffer, cache, branch predictor, and scheduler.The cache tracks metadata about stored memory blocks rather than their contents.Source: A. Hardware configurations · p. 7

1) Reorder buffers:

  • The reorder buffer stores in-flight instructions, including whether they are resolved and, for predicted control flow, the branch address associated with a predicted PC assignment.The buffer has a maximum length, and its data-independent projection replaces expressions with resolved or unresolved markers.Source: 1) Reorder buffers · p. 8

2) Caches, Branch predictors, and Schedulers:

  • Caches, branch predictors, and schedulers are modeled through interfaces for access and update, prediction, and choosing pipeline directives.The scheduler selects fetch, execute, or retire steps.Source: 2) Caches, Branch predictors, and… · p. 8

3) Microarchitectural states:

  • The microarchitectural state is a tuple containing the reorder buffer, unified cache, branch predictor, and scheduler; it is initial with an empty buffer and component initial states.Source: 3) Microarchitectural states · p. 8

B. Hardware semantics

  • Each hardware-semantics step follows a scheduler directive, updates the hardware state, then updates the scheduler using a data-independent projection of the reorder buffer.This encodes the assumption that scheduler decisions may depend on instruction dependencies, but not computed values.Source: B. Hardware semantics · p. 8

1) Fetch:

  • Instructions are fetched in order; a branch fetch queries the predictor and records its predicted PC and branch label in the reorder buffer, while a cache miss updates the cache without changing that buffer.The fetch rules use the reorder-buffer contents to determine the current architectural assignment.Source: 1) Fetch · pp. 8–9

2) Execute:

The section formalizes execution, retirement, and observation in a speculative processor, then uses this model to compare secure-speculation mechanisms and their guarantees.

2) Execute:

  • The framework models in-flight commands executing out of order but retiring in order, with resolved mispredicted branches dropping later reorder-buffer entries.Loads update the cache on a hit; retirement commits assignments and stores to architectural state.Source: 2) Execute · p. 9, 3) Retire · p. 9

C. Formalizing the adversary model

VI. MECHANISMS FOR SECURE SPECULATION

  • The section formalizes multiple countermeasures in a common semantics and characterizes their guarantees using the framework’s contracts.The comparison covers disabling speculation, delaying speculative loads, and taint-tracking approaches.Source: §VI · pp. 9–10, C. tt: Taint tracking of speculative… · p. 11
  • Disabling speculation produces the strong sequential contract, exposing only the program counter and memory-access locations under sequential execution.The sequential scheduler fetches, executes the head instruction, and retires it before proceeding.Source: A. seq: Disabling speculation · p. 10
  • Delaying speculative loads prevents data-memory accesses on mis-speculated paths, but nested branches can still leak through instruction-cache or branch-predictor state.The mechanism delays loads until preceding branches resolve, while other instructions can execute speculatively and out of order.Source: B. loadDelay: Delaying all speculative… · p. 10
  • The load-delay mechanism satisfies a contract that exposes speculative program-counter values in addition to sequential control flow and memory accesses.The section also states that speculative control flow can depend only on data loaded non-speculatively.Source: B. loadDelay: Delaying all speculative… · p. 11

1) Overview:

STT and NDA both use hardware taint tracking to handle data retrieved speculatively, but differ in what they delay. The framework represents these design choices through labeling and unlabeling functions.

1) Overview:

  • STT and NDA track data retrieved by speculative instructions, propagate taint through computations, remove it when operations are no longer transient, and selectively delay tainted operations.Source: 1) Overview · p. 11
  • STT delays tainted transmit instructions, whereas NDA conservatively delays propagation of data from tainted instructions.Source: 1) Overview · p. 11
  • The framework captures differing taint schemes with labeling and unlabeling functions that represent label assignment and propagation, and how labels affect execution.Source: 1) Overview · p. 11

2) Supporting taint tracking:

The framework extends processor steps with labels that track dependencies and influence execution. Its STT model delays tainted transmit operations, yet can still leak information through transient loads that depend on non-transient data.

2) Supporting taint tracking:

  • The taint-tracking extension labels reorder-buffer entries, applies unlabeling before a pipeline step, then relabels the resulting buffer to track information flow.Source: 2) Supporting taint tracking · p. 11

3) Speculative taint tracking:

  • The labeling function assigns labels to newly fetched instructions and updates labels as instructions retire, execute, or resolve branches.A non-empty label marks entries that may depend on transiently retrieved data.Source: 3) Speculative taint tracking · pp. 11–12
  • STT’s unlabeling function blocks transmit instructions that depend on possibly transient data while allowing non-transmit instructions to execute freely.Source: 3) Speculative taint tracking · pp. 11–12
  • STT can still leak through transient loads dependent on non-transient data, so it does not satisfy the sequential constant-time contract.The example describes a data-cache leak when a transient load executes before the branch controlling it resolves.Source: 3) Speculative taint tracking · p. 12
  • The section characterizes the meaningful guarantee of the taint-tracking model with the sequential architectural contract, which prevents transmit instructions based on transiently retrieved data.The speculative contract is already satisfied by baseline hardware, making it less informative for this countermeasure.Source: 3) Speculative taint tracking · p. 12
  • NDA prevents propagation of potentially transient assignments and uses different labeling rules for strict and permissive strategies; its guarantees are similar to those of the taint-tracking model.Source: 3) Speculative taint tracking · p. 12

4) Non-speculative data access:

The section places NDA’s guarantees alongside those of other secure-speculation mechanisms in a lattice. This yields a rigorous comparison of their guarantees and a basis for secure programming.

4) Non-speculative data access:

D. Summary

  • Figure 8 summarizes the mechanisms’ security guarantees in the contract lattice, providing a rigorous comparison of secure-speculation mechanisms.Source: D. Summary · p. 12, Figure 8 · p. 13
  • The comparison translates the results into a principled basis for programming securely with these mechanisms.Source: D. Summary · pp. 12–13

A. Scope of the model

The model is intentionally tractable but limited to simple speculation and adversary observations, with theorems not guaranteed to extend beyond that scope. The framework can be extended to other transient attacks and used to specify vendor contracts or guide clean-slate design.

A. Scope of the model

  • The model captures Spectre v1 variants but omits store-to-load forwarding, memory-alias prediction, and adversaries observing internal processor-buffer leaks.It simplifies processors to a single-threaded, three-stage pipeline with conditional branch prediction as the only speculation source; the adversary sees reorder-buffer instructions and cache blocks, not their data.Source: A. Scope of the model · p. 13
  • Theorems 1–6 need not extend to scenarios excluded by the model, although the contract framework itself is not limited to this model.The paper discusses extensions to other transient-execution attacks.Source: A. Scope of the model · p. 13, B. Beyond Spectre v1 · p. 13

B. Beyond Spectre v1

  • Contracts can be extended for Spectre-BTB and Spectre-RSB by exploring bounded mispredicted paths for indirect jumps or returns.Spectre-STL requires modeling store-to-load forwarding from aliasing predictions, while straight-line speculation can expose observations after unconditional control-flow changes.Source: B. Beyond Spectre v1 · p. 13
  • Meltdown-type attacks arise from instruction faults or microcode assists, and contracts for vulnerable processors would expose large portions of memory, challenging secure programming.The discussion includes Meltdown and data-sampling attacks.Source: B. Beyond Spectre v1 · p. 13

C. Uses of contracts

  • The authors envision CPU vendors publishing contracts so users can reason about software security without microarchitecture details and validate vendors’ security claims.The framework can also guide clean-slate microarchitecture design that optimizes performance under a desired contract.Source: C. Uses of contracts · p. 13

VIII. RELATED WORK

  • Undo-based countermeasures roll back speculative cache effects, but likely do not protect against the paper’s trace-based attackers.They provide security against adversaries observing only the final cache state.Source: §VIII · p. 14
  • The framework answers calls for hardware-software side-channel contracts by providing contracts for secure speculation and showing how software can leverage them.The paper distinguishes its work from labeled-ISA proposals, which track data labels and are described as orthogonal to characterizing standard-ISA countermeasures.Source: §VIII · p. 14

IX. CONCLUSIONS

  • The conclusions characterize hardware guarantees across a representative set of mechanisms and address secure programming and automated checks for constant-time programming and sandboxing.The checks are intended to assess whether programs run securely on the mechanisms.Source: §IX · p. 14

APPENDIX A PROOF OVERVIEW

The proof overview connects contract executions to hardware runs through state relations and reorder-buffer correspondences. Its central lemma preserves hardware-state indistinguishability one step at a time, enabling an induction that establishes contract satisfaction.

APPENDIX A PROOF OVERVIEW

  • The proof relates hardware states to contract states using a relation indexed by reorder-buffer prefix length, with contract-specific requirements for sequential and speculative modes.In speculative mode, the relation also requires invariants such as finite speculative windows for mispredicted branches.Source: Appendix A · p. 16
  • A correspondence function maps reorder-buffer prefixes to unique contract states, and the proofs construct matching correspondences across the two runs.The overview also identifies hardware-state indistinguishability and the contract-to-hardware relation as components of the proof.Source: Appendix A · p. 16

Indistinguishability lemma:

  • The indistinguishability lemma preserves indistinguishable hardware states when corresponding contract states agree on the observation produced by one contract step.For each reorder-buffer prefix, the lemma requires related contract states for both hardware states; if the conditions hold, the hardware step preserves indistinguishability or both states are stuck.Source: Indistinguishability lemma · p. 16, Figure 9 · p. 16
  • The proof establishes contract satisfaction by induction: equal contract observations and matching correspondences let indistinguishable hardware states remain indistinguishable at the next step.The initial states are indistinguishable because their microarchitectural components agree.Source: Indistinguishability lemma · p. 16

Related papers

Loading 2006.03841v3…