PaperlayerView exact revision on arXiv

Source-linked AI summary

SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)

Shixin Song, Davide Davoli, Elias Storme, Marton Bognar, Dominique Devriese, Frank Piessens, Tamara Rezk

arXiv:2609.17399v1cs.CRcs.AR

TL;DR

CHERI’s architectural isolation and constant-time programming do not by themselves prevent speculative microarchitectural leakage, while existing secure-speculation proposals fail to preserve confidentiality. The paper develops a joint formal framework, demonstrates leaks, and presents SCHERI with formally proved end-to-end guarantees for constant-time programs. Its main scope boundary is that BLACKOUT relies on software invariants that are difficult to maintain during transient execution.

  • Problem

    Speculative execution can invalidate constant-time guarantees and leak secrets despite CHERI’s architectural isolation, while existing approaches lack unified reasoning about capability safety, speculation, and information flow.

  • Method

    The paper defines speculative CHERI semantics and a strong leakage model, analyzes CSC and BLACKOUT, and proposes SCHERI with explicit taint metadata and formal security proofs.

  • Results

    SCHERI formally satisfies end-to-end secure speculation guarantees for the constant-time policy, while CSC and BLACKOUT admit confidentiality leaks under stronger leakage models.

  • Takeaways & Limitations

    Secure CHERI speculation requires jointly reasoning about authorization and information flow so constant-time behavior remains confidential under speculation.

  • Takeaways & Limitations

    BLACKOUT relies on software invariants that are highly non-trivial to construct and must hold during transient as well as architectural execution.

Abstract

from arXiv · show

Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leakage, software can be written in a constant-time fashion. Modern processors, however, rely heavily on speculative execution, which can invalidate the constant-time guarantees and leak isolated secrets transiently. In this work, we show that providing secure speculation for CHERI is non-trivial, and that existing proposals fail to preserve the confidentiality guarantees. We develop a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security, and use it to demonstrate potential leaks. We then present SCHERI, a new processor design within this framework, and formally prove that it provides end-to-end secure speculation guarantees for the constant-time policy. Our results provide formal foundations and practical guidance for building future capability-based processors, which are resilient to Spectre attacks for constant-time programs.

1 Introduction

CHERI strengthens architectural isolation, but speculative execution can preserve microarchitectural effects that leak secrets despite architectural rollback. The paper identifies shortcomings in existing approaches and introduces a formal framework and SCHERI to provide secure speculation guarantees.

  • CHERI’s capability architecture provides fine-grained memory protection and compartmentalization, but these guarantees assume architecturally correct execution.
  • Speculation can violate CHERI’s architectural guarantees because rolled-back instructions may leave observable cache and other microarchitectural effects.
  • CSC preserves capability invariants but does not guarantee confidentiality under leakage models stronger than speculative sandboxing.
  • BLACKOUT tracks secret-data flow toward data-oblivious guarantees, yet the paper shows that it does not fully secure speculation for the constant-time policy.
  • Existing approaches lack a unified framework for comparing memory safety, sandboxing, and secure speculation guarantees.
  • The paper defines speculative CHERI semantics with a strong attacker model, analyzes CSC and BLACKOUT leaks, and proposes SCHERI with formally proved end-to-end guarantees.

2 Background

CHERI uses unforgeable, bounded capabilities to enforce architectural memory safety and support compartmentalization. Speculative execution can nevertheless expose secret-dependent behavior through persistent microarchitectural effects, motivating stronger confidentiality properties than sandboxing alone.

  • CHERI capabilities carry bounds, permissions, validity, and provenance metadata, and hardware checks capability-based accesses to enforce spatial memory safety.
  • Speculative instructions may execute before checks resolve, and rollback does not erase persistent cache, predictor, or timing effects.
  • Spectre- and Meltdown-style attacks exploit transient execution to leak secrets, showing that architectural safety alone is insufficient.
  • For CHERI, bypassed speculative checks can expose secret-dependent behavior even when software is capability-safe.
  • Sandboxing prevents speculative reads outside a designated compartment, whereas constant-time execution requires secret-independent observable behavior.

3 Threat Model

The threat model allows untrusted code to trigger victim execution and observe broad microarchitectural side channels without directly violating CHERI’s architectural protections. The target property is relative speculative constant time: architecturally hidden secrets must not affect attacker observations.

  • The attacker can run untrusted code, trigger victim execution with chosen public inputs, and observe side channels without directly reading privileged state or breaking CHERI memory protection.
  • The model covers caches, branch predictors, reorder buffers, speculation and rollback behavior, execution-port contention, and other timing-visible shared resources.
  • The goal is relative speculative constant time, ensuring that secrets not leaked architecturally do not influence attacker observations.
  • The desired guarantee is stronger than CSC-style sandboxing because it preserves confidentiality rather than merely preventing capability forgery.

4 Prior Approaches and Shortcomings

The section shows that CHERI’s Capability Speculation Contract preserves speculative capability authorization but not confidentiality against side channels. It then explains how BLACKOUT’s controlled invariant violations and tracking gaps permit concrete speculative leaks.

  • 4.1 Capability Speculation Contract: CSC authorizes speculative accesses through committed or transitively reachable capabilities, but does not prevent side-channel leakage of accessible secrets.Programs can satisfy CSC and remain secure without speculation yet leak secrets when speculation exposes microarchitectural effects.
  • 4.1 Capability Speculation Contract: A secret loaded into a register can speculatively alter a capability offset, and a subsequent load can leak the secret through its address-dependent behavior.The example loads secret data through csp, advances cs0 by that value, and uses cs0 for the leaking load.
  • 4.2 BLACKOUT: BLACKOUT permits controlled violations of its invariants for stack capabilities and register spills, creating opportunities to access blinded data through non-blinded capabilities.The non-blinded stack capability can overlap secret stack data, while compiler-enforced access restrictions may fail transiently during speculation.
  • 4.2.2 Concrete Attacks: Proof-of-concept attacks exploit BLACKOUT Issues 1a and 2a, while other identified issues require additional engineering or future speculation support.The prototype lacks the hardware speculation features needed to exploit Issue 1b, although the authors expect future implementations could enable it.
  • 4.2.1 Security Analysis: BRRs are recognized as blinded only through specific capability-load checks, so narrower loads such as cld can retrieve spilled secrets without setting the blinded bit.A speculative cld access to a BRR leaves the loaded value unblinded, after which using it as a load offset leaks the secret.
  • 4.2.2 Concrete Attacks: BLACKOUT’s stack overlap also lets speculation load function-local blinded data through csp, bypassing the compiler’s normal exclusive-use discipline.The attack loads secret data via csp, uses it to advance cs0, and then performs a leaking load.

5 SCHERI

SCHERI introduces a formal speculative execution model for CHERI-like architectures and protects taint-tracked secrets through explicit capability metadata. Its semantics model capabilities, memory, speculation, and attacks, while preventing speculative secret loads through tainted stack capabilities and non-aliasing guarantees.

  • 5.1 Preliminaries: SCHERI formally models speculative execution with capabilities carrying both pointer metadata and the security level of referenced data.The model includes tainted and partial register files, tagged capability memory, SCasm instructions, and hardware semantics.
  • 5.2 Design: Explicitly encoded taints avoid conservatively classifying every capability restored through the tainted stack as secret, preserving practical speculation.Stored capabilities encode taint in metadata using packTaint(·,·), while public values use distinguished untainted register records.
  • 5.2 Design: SCHERI keeps the initial stack capability tainted and prevents public aliasing capabilities from addressing the same region as secret stack data.When public data is stored in URRs, speculative accesses through the stack cannot produce untainted secret values.
  • 5.5 Running Example: For a secret-dependent capability offset, SCHERI propagates taint from the offset and blocks the resulting secret-dependent load under speculation.In the example, the stack capability has outer taint U, the loaded offset has taint T, and the combined capability expression has outer taint T.
  • 5.6 Hardware Semantics: SCHERI’s semantics model speculative register unavailability by mapping tainted values to ⊥ until the producing instruction retires.This prevents a transient instruction from accessing the tainted value before retirement.

6 Correctness and Security of SCHERI

SCHERI is shown correct with respect to its ISA semantics and secure against speculative leakage under the paper’s relative speculative constant-time property. The proofs relate hardware executions to ISA executions and preserve public equivalence through key capability-separation invariants.

  • Security of SCHERI: SCHERI’s main security result states that ISA-level confidentiality guarantees are preserved by the hardware semantics in the presence of speculation.If a program does not leak secret data at the ISA level, it also does not leak secret data under SCHERI’s hardware semantics.
  • Correctness of SCHERI: SCHERI is functionally correct with respect to its ISA-level semantics, with the proof established by induction over execution traces.The correctness theorem relates initial ISA and hardware configurations across finite executions.
  • Security of SCHERI: Hardware leakage equivalence requires corresponding configurations to produce identical target microarchitectural contexts at every transition step.The definition quantifies over execution lengths and adversarial contexts.
  • Security of SCHERI: The security proof preserves hardware-level public equivalence and relies on the absence of regions simultaneously referenced by tainted and untainted capabilities.This invariant prevents untainted capabilities from accessing and leaking tainted data.

7 Comparison with Other Designs

The comparison shows that existing CHERI speculation designs can violate capability and confidentiality guarantees, while SCHERI prevents the identified leaks through hardware-enforced taint and capability handling.

  • CHERI-Toooba: Predicting a complete program-counter capability can cross architectural boundaries, unlike predicting only the program-counter offset.
  • CHERI-Toooba: CHERI-Toooba’s speculative capability construction can enable memory accesses that violate bounds and leak secrets unavailable to architectural execution.The constructed capability may be used before monotonicity checks are enforced, violating the CSC contract and relative speculative constant time.
  • BLACKOUT: BLACKOUT eagerly faults on some data-obliviousness violations, whereas SCHERI targets constant-time assembly by propagating rather than enforcing architectural taint.BLACKOUT relies on software-generated invariants, including invariants that must hold during transient execution.
  • SCHERI: SCHERI guarantees that URRs hold public values without software assumptions, preventing BLACKOUT’s first issue while making corrupted metadata conservative.Overwriting a URR’s tag or magic value treats the value as tainted, risking only performance degradation.
  • SCHERI: SCHERI prevents arbitrary stack-secret leakage by avoiding overlap between blinded and non-blinded capabilities, addressing BLACKOUT’s second issue.

8 Related Work

Related work develops formal models, relative-security notions, and hardware secrecy mechanisms for speculative execution. SCHERI extends these directions to capability-mediated memory access and provides a proof of constant-time security for CHERI.

  • SCHERI combines capability provenance, capability state, and authorization with formal transient-execution semantics.
  • Its relative-security model exposes control-flow and memory-access addresses, public stores, and assumes initially taint-tracked secrets and public-equivalent initial states.
  • Unlike ProSpeCT, SCHERI integrates secrecy into CHERI capabilities, enabling secret and public objects to coexist within one stack.This requires capability metadata, URR stack management, and capability-specific information-flow reasoning.
  • The paper positions SCHERI as closer to BLACKOUT but distinguishes it by providing security proofs for constant-time speculation in CHERI.
  • SecSep addresses post-compilation invalidation of source-level guarantees by separating secret and public data in compiled assembly.

9 Conclusion

The conclusion argues that CHERI’s architectural isolation alone does not ensure confidentiality under speculation. SCHERI instead combines authorization and information-flow reasoning with formal guarantees for constant-time behavior.

  • CHERI’s architectural isolation does not guarantee confidentiality under speculative execution.
  • Secure speculation for capability machines requires jointly reasoning about authorization and information flow.
  • SCHERI provides formal guarantees that preserve constant-time behavior under speculation and supports future capability systems secure at both architectural and microarchitectural levels.
  • The paper reports responsible disclosure of identified BLACKOUT issues before submission.

C Full hardware semantics

The full hardware semantics specify how SCHERI fetches, evaluates, checks, commits, and discards speculative instructions while controlling leakage through sanitized state and capability checks.

  • Fetch exposes the current program-counter value through the modeled microarchitectural leakage.
  • A mispredicted jump restores the correct target and drops all following speculative instructions from the reorder buffer.
  • SCHERI’s hardware semantics use sanitized register state when evaluating speculative branches, loads, and store capabilities to prevent transient leakage of tainted data.
  • Load execution checks capability permissions, while store execution records aliasing information and checks store permissions.
  • Committed stores update memory using the value held in the reorder buffer.

D Proofs

The appendix proves SCHERI’s functional correctness and security by establishing ISA invariants, public-state equivalence, and inductive hardware-level security arguments.

  • The proofs target SCHERI’s functional correctness and security.
  • ISA-level lemmas establish invariants needed for correctness and security reasoning.
  • SCHERI assumes no initial overlap between executable and writable memory, preserving this property through capability monotonicity.
  • Security requires tainted and untainted memory regions to remain disjoint, preventing cross-taint capability accesses and writes.
  • The framework defines public equivalence for architectural states and proves that ISA execution maintains it.
  • Functional correctness is proved by induction on hardware steps using reorder-buffer well-formedness invariants.
  • Relative speculative constant time is proved by inductive public equivalence of architectural states and microarchitectural contexts.

D.1 ISA-level Proof

The ISA-level proof establishes well-formedness preservation through capability monotonicity, showing that reachable capabilities and taint- and permission-related regions remain controlled across transitions.

  • Reachable capabilities are defined from registers and memory, with reachable addresses collected according to capability permissions and taints.
  • ISA well-formedness requires tainted and untainted memory, as well as writable and executable memory, to remain non-overlapping.
  • The ISA model maintains well-formedness, including through assignment, load, and store transitions analyzed using capability-operation monotonicity.
  • Capability monotonicity underpins preservation of ISA well-formedness across transitions.The proof uses monotonicity of tAddr(·) and pAddr(·) and analyzes transition rules by cases.
  • Expression evaluation is monotone: capability results derive from existing reachable capabilities and preserve ordered metadata and taint properties.
  • Storing an ordinary value does not expand reachable capabilities, while storing a capability adds only capabilities bounded by the stored capability.

D.1.2 ISA Maintains Public Equivalence.

The ISA proof preserves public equivalence by showing that corresponding instruction executions produce equal untainted observations under well-formed, publicly equivalent initial states.

  • Untainted projection removes tainted distinctions from values while retaining the information exposed to public observers.
  • ISA execution preserves public equivalence for well-formed, initially publicly equivalent states.
  • The inductive proof handles assignments, loads, stores, branches, and jumps by comparing their public observations and resulting memory states.
  • Taint propagation through reads and writes is constrained so that the taint of accessed data agrees with the capability context when required.
  • For public-equivalent states, corresponding reads produce equal untainted results under matching reachable capabilities and instruction conditions.

D.2 HW Functional Correctness

The hardware functional-correctness proof shows that speculative execution preserves correspondence with ISA execution by inducting over hardware steps and maintaining reorder-buffer invariants.

  • The proof maintains an invariant relating in-flight instruction outcomes and architectural application of the reorder buffer.
  • Initial hardware states have an empty reorder buffer, total registers, an untainted entry-point capability, arbitrary memory and microarchitectural context, and hardware well-formedness.
  • Fetch, execute, and commit steps are analyzed by induction, including assignments, loads, stores, branches, jumps, hazards, and squashed loads.
  • The proof relates speculative register states to architectural states using apl and aplsan, including cases where branches are mispredicted or instructions are squashed.
  • Well-formed hardware configurations remain well-formed after each hardware transition when the underlying ISA state is well-formed.
  • Under well-formed initial ISA and hardware states, SCHERI’s hardware semantics is functionally correct with respect to its ISA execution trace.

D.3 Relative Speculative Constant Time

The section defines public equivalence and proves relative speculative constant time by showing publicly equivalent executions preserve untainted speculative behavior. The proof relies on monotonicity and equivalence lemmas for capabilities, expressions, reorder buffers, and step-by-step hardware execution.

  • Relative Speculative Constant Time: Public equivalence is established using untainted reorder-buffer projections and partial-register projections, which make public expression evaluations agree across configurations.The auxiliary lemmas compare reorder buffers and registers with their untainted portions, supporting equivalence of apl and aplsan evaluations.
  • Relative Speculative Constant Time: Capability monotonicity lemmas ensure that hardware and expression executions preserve the relevant capability properties across an execution trace.Lemma D.18 addresses capability monotonicity for hardware traces, while Lemma D.19 addresses expression-level capability monotonicity.
  • Relative Speculative Constant Time: Publicly equivalent initial ISA and hardware configurations preserve hardware public equivalence throughout corresponding speculative executions.Theorem 6.2 assumes empty initial reorder buffers, matching public ISA observations, and ISA-equivalent initial states, then establishes corresponding hardware behavior.
  • Relative Speculative Constant Time: The proof maintains a step-by-step correspondence: whenever one hardware configuration executes n steps, the other can execute at least n steps while remaining publicly equivalent.The induction proceeds from the empty-buffer base case and analyzes fetch, execution, loads, stores, and control-flow cases.
  • Relative Speculative Constant Time: The induction handles speculative loads and stores by using equal untainted buffer contents, capability checks, and public equivalence of evaluated expressions.The load analysis distinguishes memory reads from forwarding previous stores and uses capability aliasing and checkCap conditions to preserve the correspondence.
Loading 2609.17399v1…