Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking

1. Problem Statement

The paper addresses the critical security threat posed by Spectre speculative side-channel attacks, specifically variants Spectre BTB (Branch Target Buffer), Spectre RSB (Return Stack Buffer), and Spectre PHT (Pattern History Table).

• The Vulnerability: Modern processors use speculative execution to improve performance. Attackers can manipulate hardware predictors (BTB, RSB) to force the processor to speculatively execute code at arbitrary addresses (control-flow hijacking). This transient execution can leak secrets via microarchitectural side channels (e.g., cache timing) even if the architectural state is eventually rolled back.
• Limitations of Existing Defenses:
  • Hardware CFI (e.g., Intel CET): While Intel's Control-flow Enforcement Technology (CET) provides Indirect Branch Tracking (IBT) and shadow stacks, previous implementations against Spectre relied on static overapproximation. They define a set of valid targets for indirect calls. However, because the set is overapproximated (e.g., allowing calls to multiple functions within a group), attackers can still redirect control flow to a valid but unintended function, bypassing the protection.
  • Software Defenses (SLH): Speculative Load Hardening (SLH) masks data during speculation but does not inherently prevent the control-flow hijack that leads to the leak.
  • Complexity: Existing comprehensive defenses (like Serberus) require complex enforcement mechanisms (e.g., procedure-private stacks, register cleaning) and impose strict programming disciplines (e.g., secrets cannot be passed by value), limiting their applicability to arbitrary software.

2. Methodology: The Triosecuris Approach

Triosecuris proposes a novel defense that combines hardware-assisted Control-Flow Integrity (CFI) with compiler-inserted Speculative Load Hardening (SLH). The core innovation is the ability to precisely detect speculative control-flow hijacking without static overapproximation.

Core Mechanism

1. Precise Detection via Dynamic Checks:
   • For Indirect Calls (BTB): Before an indirect call, the compiler saves the intended function pointer into a dedicated register (callee). The target function begins with a check comparing the callee register against its own address.
     • Result: If the BTB mispredicts and jumps to a different function (even a valid one in the same group), the check fails.
   • For Returns (RSB): Before a ret instruction, the compiler reads the top of the call stack (via a peek instruction) into the callee register. The function prologue checks if the return address matches the expected location.
2. Integration with Ultimate SLH:
   • When a mismatch is detected (indicating misspeculation), a misspeculation flag (msf) is set.
   • This flag is used by Ultimate SLH to mask all sensitive operands (memory addresses, branch conditions, division operands) with a safe value (e.g., 0) during speculative execution.
   • Crucially, this detection is precise: it distinguishes between the intended target and the misspeculated target, eliminating the need for static overapproximation sets used in FineIBT.

Formalization and Verification

The authors formalize the entire system in the Rocq (formerly Coq) proof assistant to provide machine-checked security guarantees.

• Languages: They define a source language (MINIMIR with basic blocks and abstract code pointers) and a target language (MINIMC with linearized machine code).
• Semantics: They model sequential semantics, speculative semantics (including attacker directives to force misprediction), and an "ideal" semantics where protections are enforced directly.
• Handling Undefined Behavior: A key technical challenge was handling the comparison between code pointers and integers (which is undefined in C but happens during masking). The authors introduced CompCert-style undefined values to the semantics. This allows the system to prove that Triosecuris does not introduce undefined behavior, ensuring safety preservation.

3. Key Contributions

1. Triosecuris Defense: A novel defense mechanism that precisely detects BTB and RSB misspeculation by comparing dynamic function pointers against static addresses, combined with Ultimate SLH to mask leaks.
2. Formal Verification: The first machine-checked proof of relative security for a defense against Spectre BTB, RSB, and PHT.
   • Relative Security Guarantee: The proof demonstrates that for any source program (even those not following cryptographic constant-time discipline), the hardened program running with speculation leaks no more than the source program leaks when running sequentially.
3. End-to-End Proof: The verification covers the entire compilation pipeline:
   • Transformation from MINIMIR (with abstract pointers) to MINIMIR (hardened).
   • Linearization from MINIMIR to MINIMC (machine code).
   • Composition of proofs to show end-to-end security for safe inputs.
4. Safety Preservation: Proved that the transformation does not introduce new undefined behaviors, a critical requirement for the security proofs to hold in the presence of masking.

4. Results

• Theorem 1 (Relative Security for Triosecuris): Proves that the transformation from source to hardened code preserves observational equivalence. If two source executions are indistinguishable to a sequential attacker, the hardened speculative executions are indistinguishable to a speculative attacker.
• Theorem 2 (End-to-End Relative Security): Combines the Triosecuris transformation proof with the linearization proof to guarantee security all the way down to machine code for safe inputs.
• Implementation Status: The formalization consists of approximately 6,800 lines of Rocq code. The authors also utilized ~2,500 lines of property-based testing to identify edge cases (such as the need for undefined values) before formal proof.

5. Significance

• Broader Applicability: Unlike previous defenses that require strict constant-time programming or restrict how secrets are passed (e.g., only by reference), Triosecuris protects arbitrary programs.
• Simplicity and Efficiency: By leveraging precise dynamic checks rather than static overapproximation, Triosecuris avoids the complex enforcement mechanisms (like private stacks) required by Serberus, potentially reducing overhead and complexity.
• Hardware-Software Synergy: It demonstrates how existing hardware features (Intel CET/IBT) can be utilized more effectively when combined with compiler-inserted logic, rather than relying solely on hardware or solely on software.
• Trustworthiness: The machine-checked proof provides a level of assurance that manual security proofs (common in prior work) cannot match, addressing the "implementation mistakes" and "unclear attacker models" that often plague Spectre defenses.

In summary, Triosecuris represents a significant advancement in speculative execution security by providing a formally verified, precise, and broadly applicable defense that bridges the gap between hardware CFI and software hardening.