PaperlayerView exact revision on arXiv

Source-linked AI summary

Constant-Time Foundations for the New Spectre Era

Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe

arXiv:1910.01755v3cs.CRcs.PL

TL;DR

Classical constant-time can fail to protect secrets when modern processors use speculative and out-of-order execution. The paper defines speculative constant-time under adversarially controlled execution and implements Pitchfork to check it. Its semantics captures Spectre variants, and Pitchfork finds leaks in real cryptographic code, though its analysis has bounded depth and coverage.

  • Problem

    Classical constant-time code can still leak secrets on processors with microarchitectural features, making its usual guarantees insufficient for modern hardware.

    Source: §1 · p. 1

  • Method

    The paper defines semantics and speculative constant-time for out-of-order and speculative execution, then checks violations with Pitchfork’s attacker-schedule generation and symbolic execution.

    Source: §1 · p. 1, §4 · p. 10

  • Results

    Pitchfork detects leaks in Kocher’s Spectre v1 cases, v1.1 variants, and real cryptographic code, while the semantics captures existing Spectre variants as SCT violations.

    Source: §1 · p. 2, §3.2 · p. 5

  • Takeaways & Limitations

    The semantics captures existing transient-execution attacks and can be extended to future predictors and potential attacks.

    Source: §6 · p. 12

    Pitchfork covers only part of the semantics and is constrained by symbolic-execution state explosion, supporting speculation bounds up to 20 instructions, or 250 with store-forwarding checks disabled.

    Source: §4 · p. 10, §4.2 · p. 11

Abstract

from arXiv · show

The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time as it exists today far less useful. This paper lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries.

1 Introduction

Timing side-channels make secret protection difficult, and Spectre-like attacks show that classical constant-time guarantees can fail on modern hardware. The paper defines speculative constant-time and presents Pitchfork, which detects leaks in real cryptographic libraries.

1 Introduction

  • Timing side-channels can reveal secrets through effects such as cache behavior, while Spectre, Meltdown, ZombieLoad, RIDL, and Fallout show that usual constant-time code can still leak on modern processors.Source: §1 · p. 1
  • The semantics models a three-stage fetch, execute, and retire machine with reorder buffers and transient instructions, while treating microarchitectural features as attacker-controlled.Predictor control is represented with directives, and the semantics can be extended to new predictors such as a hypothetical memory-aliasing predictor.Source: §1 · p. 1
  • Speculative constant-time extends constant-time to out-of-order and speculative execution, and all four Canella et al. Spectre attack classes violate the property.Source: §1 · p. 1
  • Pitchfork detects leaks in Kocher’s Spectre v1 test cases, v1.1 variants, and real code from libsodium, OpenSSL, and curve25519-donna.It is a prototype built on angr’s symbolic execution engine.Source: §1 · p. 2

2 Motivating Examples

The examples show how speculation can expose secrets even when sequential execution follows the classical constant-time discipline. They illustrate a bounds-check bypass and a hypothetical store-to-load forwarding attack.

2 Motivating Examples

  • The first example guesses that a bounds check passes and transiently executes two public-array loads, although the sequential path skips them for an out-of-bounds index.Source: §2 · p. 2
  • The semantics gives the attacker directives for fetch and execution order, including which branch to follow speculatively and which transient instructions to execute.Transient instructions may record the branch choice.Source: §2 · p. 2
  • The Spectre v1 example is sequentially constant-time, yet speculative execution past the bounds check lets a secret-derived load affect cache state and reveal Key[1].The attacker directs fetch and execution before the bounds check is resolved.Source: §2 · p. 2
  • The hypothetical aliasing-predictor attack differs from prior speculative data-forwarding attacks because it needs no branch misprediction.Source: §2 · p. 2, Figure 2 · p. 3
  • The aliasing-predictor example forwards secret xsec from a store into a later load address, which leaks the secret even though the loaded value is irrelevant.The speculative execution later rolls back, but the address has already been observed.Source: §2 · pp. 2–3

3 Speculative Semantics and Security

This section defines and extends speculative constant-time semantics to cover memory operations, aliasing prediction, speculation barriers, and indirect control flow, exposing memory and control-flow observations under attacker directives rather than modeling particular caches or predictors. It uses this framework to model Spectre variants and fencing mitigations, showing how secret-dependent observations violate SCT.

3.1 Speculative Constant-Time

  • SCT uses observation sequences and attacker directives to avoid modeling specific caches or predictors, remaining tractable and robust across predictors and replacement policies that do not directly leak secrets.The semantics is also validated against sequential execution by proving sequential equivalence.Source: §3.1 · p. 4

3.2 Overview of the Semantics

  • The semantics captures Spectre v1, v1.1, v4, and a hypothetical variant; these attacks violate SCT by producing observations that depend on secrets.Additional variants, including v2 and ret2spec, can be expressed with the extended semantics in Appendix A.Source: §3.2 · p. 5

3.3 Speculative Execution

  • Branch directives choose the speculatively executed path; when the branch resolves, a misprediction rolls back younger buffer entries and emits jump and rollback observations.The observations represent attacker-visible control flow and misspeculation timing.Source: §3.3 · p. 5

3.4 Memory Operations

  • Loads read memory or forward data from the latest resolved matching store, producing distinct read or forwarding observations; resolving a store address late can trigger rollback after a load used an outdated store.Store value and address resolution may occur in either order.Source: §3.4 · p. 7, Figure 5 · p. 7
  • Memory semantics make retired stores observable and detect stale-load hazards, capturing Spectre v1.1 through speculative store forwarding and Spectre v4 through loads bypassing unresolved stores.The modeled attacks leak data when a forwarded secret or outdated value is used by a later load.Source: §3.4 · pp. 7–8

3.5 Aliasing Prediction

  • Aliasing prediction permits forwarding from any value-resolved store before its address is known, then checks addresses and forwarded values, rolling back mismatches—including after the store retires.When the originating store has retired, the forwarded value is checked against memory if no intervening store matches the load address.Source: §3.5 · pp. 8–9
  • The semantics demonstrate the attack in Figure 2; an earlier draft [7] incorrectly claimed a proof-of-concept exploit on real hardware.Source: §3.5 · p. 9

3.6 Speculation Barriers

  • A fence blocks later instructions from executing until prior instructions retire, preventing the modeled Figure 1, 6, and 7 attacks by forcing a branch to resolve before following loads.In the Figure 8 example, branch misprediction rolls back the loads and fence.Source: §3.6 · pp. 9–10

3.7 Indirect Jumps and Return Address Prediction

  • Indirect jumps use predicted targets, while calls and returns expand into stack and memory operations with a return-stack buffer; the semantics express Spectre v2, ret2spec, and retpoline mitigation.Source: §3.7 · p. 10

4 Detecting Violations

Pitchfork checks speculative constant-time violations by analyzing worst-case attacker schedules, then applies the analysis to test cases and cryptographic libraries. It finds violations in real code, while symbolic-execution limits constrain the speculation it can analyze.

4 Detecting Violations

  • Pitchfork’s schedule set is sound for detecting SCT violations, but its implementation omits alias-prediction, indirect-jump, and return-stack-buffer violations.The omitted cases would require prohibitively many schedules; the tool still exposes attacks based on Spectre variants 1, 1.1, and 4.Source: §4 · p. 10

4.1 Schedule Generation

  • Pitchfork builds worst-case schedules by eagerly filling the reorder buffer, exploring both conditional-branch guesses and possible load-store forwarding outcomes.Other instructions execute eagerly and in order because reordering them is described as either commuting or invalid.Source: §4.1 · pp. 10–11

4.2 Implementation and Evaluation

  • Pitchfork uses angr symbolic execution to check schedules and sanity-checks its analysis on Spectre v1 and v1.1 cases, but symbolic-execution limits bound its speculation depth.The tested bound reached 20 instructions with store-forwarding checks, or 250 when those checks were disabled.Source: §4.2 · p. 11

4.2.1 Evaluation Procedure.

  • The real-library evaluation uses FaCT case studies whose implementations were verified sequentially constant-time and whose inputs had secrecy labels; runs used a 250-instruction bound without forwarding checks and 20 with them.The reduced bound was chosen to keep analysis tractable.Source: §4.2.1 · p. 11
  • Pitchfork found no violations in curve25519-donna, but found violations in libsodium and OpenSSL C code and, with forwarding checks, FaCT OpenSSL implementations.The C findings were in code ancillary to core crypto routines; the FaCT findings required forwarding-hazard detection.Source: §4.2.2 · p. 11, Table 2 · p. 11

4.2.2 Detected Violations.

  • In the OpenSSL MEE case, forwarding can restore a return address, making a second array access depend on secret-derived ret; the libsodium example involves speculative error handling.For OpenSSL, the secret condition is pad > maxpad, and the resulting access to _out[0] or _out[-1] leaks through cache state.Source: §4.2.2 · pp. 11–12

5 Related Work

Related work models speculation and out-of-order execution in different ways, but the paper distinguishes its security-focused semantics and direct SCT verification from approaches with narrower speculation models or no formal security property.

5 Related Work

  • Prior models of speculative or out-of-order execution focus on correctness, whereas this work models side-channel leakage explicitly and treats microarchitectural features as adversarially controlled.Disselkoen et al. use a higher-level relaxed-memory semantics but do not define a security property preventing Spectre-like attacks or provide verification support.Source: §5 · p. 12
  • Mcilroy et al. [24] model branch-predictor and cache state but omit barriers and store-forwarding, limiting their semantics to Spectre v1.Their work does not define a formal security property.Source: §5 · p. 12
  • Guarnieri et al. and Cheang et al. model branch-prediction speculation but not general out-of-order execution; their security property is equivalent to SCT for sequentially constant-time programs.The paper says its stronger SCT property is simpler to verify directly, without first checking sequential constant-time, and is required for its cryptographic-code focus.Source: §5 · p. 12
  • Balliu et al. [3] capture several Spectre attacks, including alias prediction, and also describe a memory-ordering attack that this paper’s semantics cannot capture.Other tools include oo7, which uses taint tracking and inserts mitigations, and Wu and Wang, which analyze LLVM cache behavior under speculation for Spectre v1.Source: §5 · p. 12

6 Conclusion

The paper introduces semantics for side channels under adversarially controlled out-of-order and speculative execution, defines speculative constant-time, and implements Pitchfork to check it. The prototype discovers vulnerabilities in real-world cryptographic libraries.

6 Conclusion

  • The semantics capture existing transient-execution attacks, namely Spectre, and can be extended to future hardware predictors and potential attacks.The model treats out-of-order and speculative execution as adversarially controlled.Source: §6 · p. 12
  • The paper defines speculative constant-time and implements Pitchfork, a prototype tool that checks whether code satisfies it.Pitchfork discovered new vulnerabilities in real-world crypto libraries.Source: §6 · p. 12
  • The authors identify proving the effectiveness of existing countermeasures, such as retpolines, and justifying new ones as future work.Source: §6 · p. 13

A.1 Indirect jumps

The indirect-jump semantics lets the schedule guess a target and later resolve it, making the jump target an observable leak. A mistrained predictor can direct execution to secret-revealing code beyond a fence.

A.1 Indirect jumps

  • At fetch, the schedule records an attacker-guessed jump target; execution resolves the actual target and either confirms the guess or rolls back the speculative path.The guess is modeled as an attacker directive because an adversary can influence branch predictors.Source: §A.1 · p. 14
  • Indirect jumps leak their calculated target, so a mistrained predictor can redirect execution to code that immediately reveals a loaded secret.The example states that speculation barriers do not prevent this attack because an arbitrary target can jump past the fence.Source: §A.1 · p. 14, Figure 11 · p. 14

A.2 Return address prediction

The semantics models function calls and returns with an explicit memory call stack and return stack buffer (RSB). Return prediction uses the RSB, except when it is empty, when the attacker can supply a speculative return address.

A.2 Return address prediction

  • Calls and returns update the memory call stack using rsp, storing return addresses on calls and loading them on returns.Abstract succ and pred operations allow different stack designs; rsp itself is not protected from illegal access.Source: §A.2 · pp. 14–16
  • The RSB models return prediction by pushing return addresses on calls and popping them on returns.It is rolled back on misspeculation or memory hazards; the semantics assumes these predictions cannot be attacker-influenced on most processors.Source: §A.2 · p. 15
  • An RSB underflow lets the attacker choose the speculative return address, enabling execution to an arbitrary program point.After a call and paired return empty the RSB, an unmatched return uses the attacker-controlled schedule to select the next program point.Source: Figure 12 · p. 15, §A.2 · p. 16
  • Retpoline prevents speculative hijacking of the indirect jump target by redirecting speculative returns to a fence loop.When the transient return sequence executes, the target is loaded from memory and execution is directed to the proper jump target.Source: §A.2 · pp. 16–17, Figure 13 · p. 16

B.1 Consistency

The consistency results relate executions under well-formed schedules to sequential execution. They establish equivalent configurations, with exact equality when the final configurations are terminal.

B.1 Consistency

  • The proof removes misspeculated steps and inductively rearranges the remaining directives into sequential schedules without changing terminal configurations.The argument proceeds by cases over instruction types, including branches, loads, stores, calls, and returns.Source: §B.1 · pp. 17–18
  • Any well-formed scheduled execution has a sequential counterpart with an equivalent final configuration; if terminal, the configurations are equal.A sequential schedule fetches an instruction, executes and retires it before fetching more.Source: §B.1 · p. 17
  • Executions from an initial configuration under any two well-formed schedules yield equivalent configurations, and terminal configurations are equal.When one schedule is sequential, the resulting configurations are equal.Source: §B.1 · pp. 17–18

B.2 Security

The security results relate speculative constant-time execution to sequential constant-time behavior. They show that secret-free speculative traces imply secret-free sequential traces, and that a terminal execution that is SCT under a well-formed schedule is sequentially constant-time.

B.2 Security

  • The label-stability argument compares executions with the same path and shows that corresponding observations preserve their labels.The proof notes that forwarded loads may retrieve values from memory after reordering, while the address attached to the observation remains unchanged.Source: §B.2 · p. 18
  • If a speculative trace contains no secret labels, sequential execution will never produce a trace containing secret labels.Source: §B.2 · p. 18
  • If an execution terminates and is SCT under a well-formed schedule, then the program is also sequentially constant-time.Source: §B.2 · p. 18

B.3 Soundness of Pitchfork

Pitchfork’s soundness argument bounds its schedule search and relates matching-path executions to matching observations. Consequently, any secret observation under a schedule within the speculation bound is also found by a tool schedule.

B.3 Soundness of Pitchfork

  • The path function records branch choices and store-forwarding information, providing the comparison criterion used in the soundness proof.Source: §B.3 · pp. 18–19
  • For matching-path schedules, corresponding fetches select the same physical instruction and corresponding executions and retirements produce the same observations.The proof accounts for register dependencies, store-forwarding behavior, and branch misspeculation hazards.Source: §B.3 · p. 19
  • Every well-formed schedule whose reorder buffer stays within n has a tool schedule with the same path.The tool considers both branch choices and allows loads to skip combinations of prior stores.Source: §B.3 · p. 20
  • If speculative execution within bound n produces a secret-labeled observation, some Pitchfork tool schedule in DT(n) also produces one.Source: §B.3 · p. 20
Loading 1910.01755v3…