PaperlayerView exact revision on arXiv

Source-linked AI summary

SPECTECTOR: Principled Detection of Speculative Information Flows

Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez

arXiv:1812.08639v2cs.CR

TL;DR

Existing countermeasures lack a precise security characterization for speculative execution attacks. The paper introduces speculative non-interference and SPECTECTOR, which uses symbolic execution to prove security or detect leaks; evaluations find compiler leaks and optimization opportunities while scalability remains comparable to symbolic-path discovery.

  • Problem

    A precise characterization of security against speculative execution attacks is missing, limiting principled reasoning about countermeasure effectiveness and placement.

  • Method

    The paper defines speculative non-interference and implements SPECTECTOR, which uses symbolic execution to check it automatically.

  • Results

    SPECTECTOR detects speculative leaks, proves many compiler countermeasures secure, and finds that checking speculative non-interference costs are comparable to discovering symbolic paths.

  • Takeaways & Limitations

    The tool exposes subtle leaks and optimization opportunities in how state-of-the-art compilers apply SPECTRE mitigations.

Abstract

from arXiv · show

Since the advent of SPECTRE, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. In this paper (1) we put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and (2) we develop SPECTECTOR, an algorithm based on symbolic execution to automatically prove speculative non-interference, or to detect violations. We implement SPECTECTOR in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place SPECTRE countermeasures. A scalability analysis indicates that checking speculative non-interference does not exhibit fundamental bottlenecks beyond those inherited by symbolic execution.

I. INTRODUCTION

The paper defines speculative non-interference as a semantic security criterion and develops SPECTECTOR, a symbolic-execution algorithm for proving it or detecting speculative leaks. Evaluations apply the tool to compiler countermeasures and assess its scalability.

  • Motivation: Speculative execution can leave cache effects after architectural rollback, allowing speculatively accessed data to leak through microarchitectural state.This affects modern processors and threatens confidentiality in multi-tenant platforms.
  • Security notion: Speculative non-interference requires speculative execution to leak no more information than standard non-speculative execution.The definition compares traces of memory locations and jump targets under the two semantics.
  • Analysis: SPECTECTOR uses symbolic execution, a worst-case branch predictor, and SMT formulas to automatically prove speculative non-interference or detect violations.It represents traces along symbolic paths and checks whether standard trace equivalence implies speculative trace equivalence.
  • Evaluation: In a corpus of 240 assembly programs, SPECTECTOR detected known and subtle speculative leaks and analyzed compiler-inserted countermeasures.The corpus covered 15 SPECTRE v1 variants compiled with CLANG, Intel ICC, and Microsoft Visual C++ under different optimization and protection settings.
  • Scalability: The cost of checking speculative non-interference is comparable to discovering symbolic paths, with no fundamental bottlenecks beyond symbolic execution.The comparison is feasible because SPECTECTOR compares executions following the same symbolic path.

III. LANGUAGE AND SEMANTICS

µASM provides a core assembly language with instructions and well-formedness conditions for modeling speculative execution. Its standard semantics represents configurations, observations, individual steps, and complete terminating runs.

  • Language: µASM includes assignments, loads, stores, branches, jumps, and speculation barriers, with conditional assignments and barriers serving as SPECTRE countermeasure primitives.Programs are sequences of labeled instructions and must satisfy uniqueness, initial-label, and branch-form constraints.
  • Language: A program is treated as a partial function from natural-number labels to instructions, returning ⊥ when no instruction has the queried label.
  • Standard semantics: The evaluation relation maps configurations to configurations while producing observations; runs collect an initial configuration, observation trace, and final configuration.The set of runs contains all executions, and the section considers only terminating programs; nonterminating extensions are future work.
  • Standard semantics: A configuration pairs a memory with a register assignment, while initial and final states are identified by program-counter values 0 and ⊥.
  • Standard semantics: The adversary observes program-counter values and memory-access locations through pc, load, and store observations, capturing cache leakage without an explicit cache model.

IV. SPECULATIVE SEMANTICS

The speculative semantics extends ordinary execution with prediction-driven, bounded speculative transactions. It snapshots state, tracks nested transactions and branch history, and commits correct predictions or rolls back incorrect ones.

  • Modeling speculation: Non-branching instructions follow standard semantics, while a prediction oracle selects the branch and speculative execution begins when a branching instruction is reached.
  • Modeling speculation: Each speculative transaction snapshots the configuration and executes the predicted branch for a bounded number of computation steps before its prediction is checked.Correct predictions commit; incorrect predictions restore the original configuration and continue on the correct branch.
  • Prediction oracles: A prediction oracle maps a program, branching history, and branch label to a predicted branch and speculative-window length.Branching history supports history-based predictors, and the oracle’s window is bounded by w.
  • Prediction oracles: The model can represent BTFNT and dynamic predictors, including simple 2-bit, correlating, and tournament predictors.BTFNT predicts taken when the target address is lower than the program counter, for a fixed speculative window.
  • Speculative transactions: Speculative states store a pre-transaction snapshot, transaction identifier, remaining length, and predicted branch; sequences of these states represent nested transactions.The semantics tracks simultaneous transactions and exposes their start, commit, and rollback events.

D. Evaluation relation

The speculative relation operates over extended configurations and models branch prediction, transaction progress, commit, rollback, and nested-transaction effects. Trace projections connect speculative behavior to ordinary semantics and support speculative non-interference.

  • Evaluation relation: An extended configuration contains a transaction counter, ordinary configuration, active speculative states, and branching history; the speculative relation produces extended observation traces.
  • Evaluation relation: SE-NOBRANCH executes non-branching instructions like the standard semantics while decrementing speculative lengths or zeroing them at speculation barriers.
  • Evaluation relation: SE-BRANCH queries the oracle, redirects the program counter, updates transaction bookkeeping, and appends a speculative state for the predicted branch.
  • Evaluation relation: SE-COMMIT checks prediction correctness against one non-speculative step, records a commit, and updates branching history.
  • Evaluation relation: SE-ROLLBACK detects an incorrect prediction, restores the saved configuration, and terminates nested speculative transactions.
  • Trace projections and security: The non-speculative trace projection removes rolled-back substrings and extended observations, and Proposition 1 states that it recovers the non-speculative runs.The semantics introduces speculative non-interference as a security notion for information leaks caused by speculative execution.

C. Always-mispredict speculative semantics

The always-mispredict semantics replaces predictor-specific analysis with a worst-case model that mispredicts every branch, while adjusting nested-transaction exploration. This model supports security guarantees for all prediction oracles and enables symbolic checking of speculative non-interference.

  • Nested-branch behavior: Correct prediction of a nested branch can expose a speculative leak that always-mispredict execution misses.In the example, always misprediction rolls back the outer transaction before line 4, whereas correctly predicting the inner branch reaches the leaking access.
  • Motivation and definition: Always-mispredict semantics mispredicts every branch, avoiding dependence on a prediction oracle.It is introduced to avoid considering correct and incorrect predictions at every branch, which would cause an exponential path explosion.
  • Transaction handling: Nested transactions receive bounded lengths while preserving the outer transaction’s exploration after rollback.Non-nested transactions have length w; nested transactions use the remaining enclosing length minus one, and only the innermost transaction is decremented.
  • Security guarantee: Checking SNI under always-mispredict semantics is sufficient for security against all prediction oracles with speculative window at most w.Theorem 1 characterizes this equivalence by comparing traces from P-equivalent initial configurations with equal standard traces.
  • Symbolic analysis: SPECTECTOR symbolically executes programs under the always-mispredict semantics and uses SMT-based checks to detect memory or control-flow leaks.Symbolic expressions, memories, traces, path conditions, and concretization represent the possible executions; the algorithm returns SECURE or INSECURE.

B. Checking speculative non-interference

SPECTECTOR checks symbolic executions for memory and control-flow differences that violate speculative non-interference. Its soundness and completeness theorem states that, when it terminates, SECURE exactly corresponds to speculative non-interference for all bounded-window prediction oracles.

  • Algorithm: SPECTECTOR analyzes each symbolic run with MEMLEAK and CTRLLEAK to detect speculative information flows through memory or control-flow observations.It reports INSECURE upon finding a witness and otherwise reports SECURE.
  • Memory leaks: MEMLEAK encodes two P-equivalent runs whose non-speculative memory observations agree but whose speculative memory observations differ.The satisfiability check uses path conditions, policy equivalence, non-speculative observation equivalence, and negated speculative equivalence.
  • Violation witnesses: A satisfiable MEMLEAK or CTRLLEAK formula witnesses a violation of speculative non-interference.For memory, the witness consists of differing speculative access observations; for control flow, it consists of differing speculative program-counter observations.
  • Control-flow leaks: CTRLLEAK searches for P-indistinguishable configurations with identical non-speculative traces but differing speculative branch or jump outcomes.It checks satisfiability of constraints including path conditions, policy equivalence, observation equivalence, and unequal symbolic branch conditions.
  • Correctness: SPECTECTOR is sound and complete when it terminates: SECURE holds exactly when the program satisfies SNI for all bounded-window prediction oracles.This result combines the always-mispredict semantics’ oracle abstraction with the symbolic semantics’ correspondence to concrete runs.

VII. TOOL IMPLEMENTATION

SPECTECTOR combines an x86-to-µASM front end, symbolic/concolic execution, and SMT checking to analyze speculative leaks and compiler countermeasures. Across 240 compiled Kocher examples, it detects unprotected leaks, proves many mitigations secure, and exposes subtle or unnecessary compiler behavior.

  • Tool architecture: SPECTECTOR implements a front end for x86 assembly, a core engine for Algorithm 1, and an SMT-query back end.The front end translates assembly into µASM, while Z3 handles symbolic expressions over bitvectors and arrays.
  • Compiler countermeasures: The case study analyzes 240 x64 assembly programs generated from 15 SPECTRE examples using three compilers, two optimization levels, and two or three mitigation levels.The configurations include unprotected compilation, speculation barriers, and speculative load hardening.
  • Experimental results: SPECTECTOR detects speculative leaks in almost all unprotected programs across compilers, except Example #8 when -O2 produces a safe conditional move.At -O0, compilers translate the example into a vulnerable branch; at -O2, optimization closes the leak.
  • Experimental results: CLANG and ICC fence every branch and are proved secure, while VISUAL C++ exposes the leaks identified by Kocher and additional optimization-dependent behavior.For VISUAL C++, SPECTECTOR also establishes security for Examples #3 and #5 under FEN at -O0.
  • Experimental results: SPECTECTOR proves CLANG’s speculative load hardening secure except for Example #10 at -O2 and Example #15 at -O0.In Example #10, masking the address index without masking the loaded value leaves a speculative leak through the jump target.
  • Experimental results: Example #10 illustrates that SPECTECTOR can detect a subtle speculative non-interference violation that may nevertheless be mitigated by processor dependencies or OS-level memory policies.The paper notes that contextual policies can improve analysis precision.

C. Performance

The Xen scalability study evaluates SPECTECTOR under bounded exploration and incomplete modeling. Path discovery dominates the cost profile, while checking speculative non-interference is evaluated relative to symbolic-path discovery rather than as a complete security assessment.

  • Scope and limitations: The Xen study sacrifices soundness and completeness by bounding symbolic exploration and treating unsupported instructions as skip.The analysis therefore does not make security claims about the hypervisor.
  • Scalability analysis: The study discovers 24 701 symbolic paths, comparing path-discovery time with the time required to check speculative non-interference.This comparison factors out path explosion when evaluating the relative scalability of SNI checking.
  • Experimental setup: SPECTECTOR analyzes 3 959 Xen functions with at most 25 symbolic paths of at most 10 000 instructions each and a global timeout of 10 minutes.Execution time is recorded by trace length because it better reflects SMT-formula size.
  • Path discovery: The first symbolic path is cheap because concolic execution requires no SMT queries, whereas discovering further paths increases execution time by approximately two orders of magnitude.The first paths are shown as yellow dots and later paths as blue dots in Fig. 8(c).
  • Coverage: 48.3% of functions do not reach 25 paths, 35.4% do not reach 10 000 instructions per path, and 18.7% encounter no unsupported instructions.Only 13 functions satisfy all three conditions.

Cost of checking SNI:

SPECTECTOR’s SNI checking cost is comparable to symbolic-path discovery, with most traces analyzed within one minute. The authors attribute this scalability to comparing executions only when they follow the same symbolic path.

  • Cost of checking SNI:: 93.8% of traces were analyzed by MEMLEAK and 94.7% by CTRLLEAK within 1 minute, out of 24 701 traces.The remaining traces timed out.
  • Cost of checking SNI:: For 41.9% of traces, SNI checking was at most 10x faster than trace discovery, while for 20.2% it was 10x–100x faster.
  • Cost of checking SNI:: For 26.9% of traces, trace discovery was at most 10x faster than SNI checking, while for 7.9% it was 10x–100x faster.
  • Cost of checking SNI:: The cost of checking SNI is comparable to discovering symbolic paths, despite SNI being a relational property.SPECTECTOR compares executions that follow the same symbolic path, avoiding additional fundamental bottlenecks beyond symbolic execution.

APPENDIX A: NON-SPECULATIVE SEMANTICS

The semantics defines ordinary and speculative executions, then uses symbolic representations and projections to compare their observable behavior. SPECTECTOR applies these semantics to detect leaks and verify compiler-generated defenses.

  • APPENDIX A: NON-SPECULATIVE SEMANTICS: The non-speculative projection retains observations from committed transactions and removes rolled-back transactions.
  • APPENDIX A: NON-SPECULATIVE SEMANTICS: The speculative projection retains observations produced by rolled-back transactions.
  • APPENDIX A: NON-SPECULATIVE SEMANTICS: The always-mispredict semantics recovers non-speculative behavior after projection and represents worst-case leakage for predictors with bounded speculative windows.
  • APPENDIX A: NON-SPECULATIVE SEMANTICS: SPECTECTOR detects leaks in unhardened or incompletely hardened compiler output, while proving speculative non-interference for selected optimized or hardened outputs.

A. Soundness of the speculative semantics

The soundness results establish that speculative executions preserve ordinary behavior after projection and that the always-mispredict semantics can represent behaviors of arbitrary predictors within the speculative window.

  • A. Soundness of the speculative semantics: The speculative semantics does not introduce spurious non-speculative behaviors.
  • A. Soundness of the speculative semantics: Every terminating non-speculative execution can be represented by a speculative execution whose non-speculative projection matches it.
  • A. Soundness of the speculative semantics: Rolled-back transactions leave the architectural configuration unchanged, while committed and ordinary steps preserve the corresponding non-speculative behavior.
  • A. Soundness of the speculative semantics: Theorem 1 characterizes SNI by requiring speculative observations to agree whenever security-equivalent initial states have equal non-speculative observations.
  • A. Soundness of the speculative semantics: If two initial configurations have the same always-mispredict speculative behavior, they have the same behavior under every prediction oracle with speculative window at most w.

B. Soundness

The soundness proof relates always-mispredict and general speculative executions through invariants preserved across branch, rollback, and ordinary steps. This establishes the predictor abstraction used by the analysis.

  • B. Soundness: The always-mispredict semantics is sound with respect to the speculative semantics.
  • B. Soundness: If two initial configurations have equal always-mispredict behavior, their executions under every bounded-window prediction oracle are equal.
  • B. Soundness: The proof maintains correspondence between always-mispredict and speculative configurations, including program counters, speculative states, and execution traces.
  • B. Soundness: The proof proceeds by case analysis on remaining speculative-window length and on whether a prediction is correct or mispredicted.

0. Moreover, by applying the rule

The proof establishes that paired speculative and non-speculative executions preserve aligned architectural states, speculative states, histories, and invariants across transitions. It handles both commit and rollback cases while maintaining matching control-flow observations.

  • Invariant preservation: The proof maintains speculation-window invariants by showing that stack lengths and minimum remaining windows continue to match the architectural execution.The argument treats the last speculative state and earlier states separately, including the effect of speculative barriers.
  • Control-flow agreement: Matching program-counter updates imply equal transition observations when corresponding instructions are non-jumps or jumps with the same target.The proof derives equal transition labels from equal initial states and equal branch targets.
  • Commit case: Committed speculative states can be removed while preserving architectural-state equality and the correspondence between speculative and architectural stacks.The commit case relies on the SE-COMMIT rule and the fact that the committed speculative state is removed from both executions.
  • Rollback case: Rollback transitions preserve paired speculative-state structure and maintain the correspondence between rollback identifiers and commit-free projections.The rollback case tracks the rolled-back state by its index and transaction identifier in both executions.

C. Completeness

The completeness argument shows that any concrete speculative behavior differing between two initial configurations can be realized by a prediction oracle with bounded speculative window. The constructed oracle follows a finite prediction list and then predicts branches as taken, yielding distinct observations.

  • Completeness result: Proposition 8 states that differing bounded-window behaviors imply a prediction oracle producing different speculative observations.The proposition applies to both terminating and non-terminating executions.
  • Non-termination: For non-terminating cases, speculative execution preserves the underlying termination difference, so every prediction oracle yields distinct outcomes.The proof uses the fact that speculation neither introduces nor prevents non-termination.
  • Terminating executions: For terminating cases, the proof distinguishes branch and non-branch transitions and constructs matching speculative executions until their observations diverge.The branch case uses differing branch outcomes to produce different transition traces.
  • Execution correspondence: The proof shows that the constructed oracle drives both executions through corresponding states before producing distinct traces.The argument explicitly relates the speculative configurations to the extended always-mispredict executions.
  • Oracle construction: The prediction oracle is constructed from a finite list of predictions and then always predicts the branch as taken.Its decisions depend only on the program counter, program, and history length, and its speculative window is at most w.

APPENDIX I: RELATING CONCRETE AND SYMBOLIC ALWAYS MISPREDICT SEMANTICS (PROPOSITION 2)

Proposition 2 relates concrete and symbolic always-mispredict semantics by proving that each concrete run is represented by a symbolic trace valuation and each concretized symbolic trace is a concrete run.

  • Concrete-symbolic equivalence: Proposition 2 states that the concrete always-mispredict semantics equals the concretization of the symbolic semantics.The proposition is derived from Propositions 9 and 10.
  • Forward direction: Every concrete run has a symbolic trace, valuation, and path condition whose concretization yields the same initial state, trace, and final state.The forward direction maps a concrete run to a symbolic run satisfying its path condition.
  • Reverse direction: Every concretized symbolic trace corresponds to a concrete run in the always-mispredict semantics.The reverse direction applies a valuation satisfying the symbolic path condition to recover the concrete run.

A. Auxiliary definitions

The auxiliary definitions formalize next-step misprediction conditions for symbolic and concrete speculative states. They also record basic valuation properties used to connect symbolic assignments and memories with their concrete interpretations.

  • Mispredict path conditions: A symbolic speculative state’s next-step mispredict path condition requires a transition whose resulting program counter differs from the predicted target.If no such transition exists, the condition is defined as true.
  • Mispredict path conditions: For a sequence of symbolic speculative states, the next-step mispredict condition is the conjunction of the conditions for its individual states.The sequence condition combines all state-level requirements.
  • Well-formedness: A concrete speculative state is next-step mispredict well-formed when its actual successor program counter differs from the predicted target.The same requirement is lifted pointwise to sequences of speculative states.
  • Valuation properties: Valuation commutes with symbolic register assignments, memory lookups, and expression evaluation.These facts support the correspondence between symbolic execution and concrete execution.

C. Soundness

The soundness results show that every symbolic execution step can be concretized consistently, establishing that symbolic traces correspond to concrete executions. Proposition 9 formalizes this soundness for the symbolic semantics.

  • Symbolic executions are checked by cases over rules including skip, barrier, assignment, conditional update, load, store, and branch operations.
  • For each symbolic step, evaluating its expressions under a valuation yields the corresponding concrete state transition and trace.
  • The proof handles both satisfiable and unsatisfiable conditional updates, preserving the concrete register and program-counter updates under valuation.
  • The load and store cases show that symbolic memory reads and writes evaluate to the matching concrete memory operations.
  • Proposition 9 proves the soundness of the symbolic semantics for program executions and valuations.

D. Completeness

The paper establishes completeness of its non-speculative symbolic semantics and uses that foundation to characterize SPECTECTOR’s security decisions. Secure results correspond to speculative non-interference, while insecure results expose a violating prediction oracle within the analyzed window.

  • Non-speculative symbolic semantics: Lemma 10 proves that every concrete transition can be matched by a symbolic transition under any assignment satisfying the symbolic state.The proof proceeds by case distinction over concrete rules and preserves memory, assignment, trace, and path-condition correspondence.
  • Non-speculative symbolic semantics: The completeness proof covers assignment, conditional update, load, store, skip, and barrier transitions by showing that symbolic execution concretizes to the corresponding concrete step.The transition-specific cases establish correspondence for both ordinary expressions and symbolic memory operations.
  • Completeness result: Proposition 10 establishes completeness of the symbolic semantics, providing the semantic basis for reasoning about concrete executions through symbolic traces.Lemma 10 is identified as the completeness result used in this proposition.
  • SPECTECTOR decision correctness: If SPECTECTOR terminates with SECURE, the program satisfies speculative non-interference for the policy and every prediction oracle with speculative window at most w.The soundness direction is stated directly by Theorem 2 and Lemma 12.
  • SPECTECTOR decision correctness: If SPECTECTOR returns INSECURE, an oracle with speculative window at most w witnesses a violation of speculative non-interference.A satisfiable symbolic trace yields executions agreeing on non-sensitive behavior but differing in speculative observations, or a control-flow leak.
Loading 1812.08639v2…