SoK: Practical Foundations for Software Spectre Defenses

### Overview In this talk, Sanjay presents a systematization of knowledge regarding software-based defenses against Spectre attacks. Spectre fundamentally breaks standard processor execution assumptions by exploiting speculative execution mechanisms—such as branch predictors, return target predictors, indirect jump predictors, and memory disambiguation/data flow prediction. Because early mitigation efforts relied on ad hoc, reactive patches that failed to cover slightly altered attack patterns or cross-process mistraining, the speaker advocates for formal methods, principled attacker models, and domain-appropriate abstractions to systematically eliminate speculative leaks.

### Key Topics - **Mechanisms of Spectre**: Out-of-order execution, branch misprediction bypassing memory bounds checks, indirect jump prediction, function return prediction, and data-flow store-to-load forwarding. - **Limitations of Early Defenses**: Flaws in ad hoc solutions such as pattern matching in compilers (e.g., Microsoft's QSpecter flag), recurring manual kernel patches (Linux eBPF), and browser mitigations (Google Chrome's strict site isolation undermined by Spook.js). - **Attacker Modeling and Abstraction Sweet Spots**: Why models that are too narrow (e.g., step-counter leakage models or influence-only models like 007) miss critical attacks like port contention or cross-process training, whereas overly expressive models (Constantine, Foundations, Inspector) introduce excessive false positives. - **Domain-Specific Approaches**: Translating sequential security definitions into speculative semantics for cryptographic code (constant-time models) and sandboxed environments (e.g., WebAssembly, Linux eBPF). - **Multi-Layer Verification and Compilation**: Establishing secure translation from high-level languages (C, Rust, Haskell) down through intermediate representations to structured assembly and machine code.

### Technical Details The speaker highlights two primary application domains where formal software defenses have shown success: 1. **Cryptographic Software**: Building on sequential constant-time security (where execution traces and memory access patterns do not depend on secret data), tools like those in High-Assurance Cryptography and Hunting the Haunter extend constant-time semantics to speculative execution paths. Because cryptographic code tends to feature regular control flow and structured data, tracking speculative misprediction paths is mathematically tractable. 2. **Sandboxed Systems**: In environments like Linux eBPF and browser WebAssembly/JavaScript, sandboxes treat any out-of-bounds read as an immediate leak. Tools like FaCT/FEniCS-style systems, FaSym, or Swivel leverage sandbox host control to rewrite code and eliminate dangerous speculative paths.

More generalized tools such as Spectector and FaST adopt relative non-interference: programs running speculatively must not leak any more information than they would under normal sequential execution. To restore broader properties destroyed by Spectre (memory safety, type safety, and control flow integrity), research spans several abstraction layers: - **Binary/Assembly Level**: Verified by tools such as Binsec and Spectector. - **Structured Assembly & IR**: Tools like Jasmin, Blade, and FaCT work at structured assembly or LLVM IR, inserting barriers or transformations. - **Sandboxed IR / High-Level Languages**: Swivel validates WebAssembly transformations. Blade establishes formal semantics between LLVM IR and assembly to prove that the resulting machine code remains Spectre-free, while hardware-software contracts bridge the gap between software semantics and hardware guarantees.

### Takeaways To achieve sound, long-term software defenses against speculative execution vulnerabilities, security must be rebuilt from the ground up using formal methods rather than reactive patching. Developers and security architects must select attacker models tailored to their domain (e.g., constant-time for crypto, strict isolation for sandboxing) to avoid false positives and missed attacks. The ultimate goal is end-to-end, compiler-verified preservation of sequential security properties from high-level source languages down to hardware.