SpecIBT: Formally Verified Protection Against Speculative Control-Flow Hijacking

TL;DR

SpecIBT targets speculative-control-flow attacks arising from $BTB$, $RSB$, and $PHT$ by marrying CET-style hardware-assisted CFI with compiler-inserted Ultimate SLH. The authors formalize SpecIBT in the Rocq prover, prove relative security for both the transformation and its machine-code translation, and address undefined behavior using CompCert-style undefined values. The work provides a fully mechanized end-to-end verification, supported by a Rocq artifact with thousands of lines of code and extensive tests, and demonstrates that precise BTB-misprediction detection suffices to bound leakage under speculation. This approach offers a practical path to secure compilation for arbitrary programs without relying on cryptographic-time assumptions, potentially informing future LLVM implementations and hardware-software defenses against speculative execution attacks.

Abstract

This paper introduces SpecIBT, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening (SLH). SpecIBT is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and set the SLH misspeculation flag. We formalize SpecIBT as a transformation in Rocq and provide a machine-checked proof that it achieves relative security: any transformed program running with speculation leaks no more than what the source program leaks without speculation. This strong security guarantee applies to arbitrary programs, even those not following the cryptographic constant-time programming discipline.

Figures (8)

• Figure 1: Languages and security results
• Figure 2: Granularity comparison of different IBT defenses against speculative executions attackers
• Figure 3: Language syntax
• Figure 4: Evaluation of expressions. We assume the standard interpretation of binary operators on integers. Note that the conditional expression $b \operatorname{\texttt{?}} e_1 \operatorname{\texttt{:}} e_2$ can still produce a defined value if only the unused expression is undefined.
• Figure 5: Speculative semantics for MiniMIR

Theorems & Definitions (23)

• Example 1
• Example 2
• Example 3
• Example 4
• Example 5
• Example 6
• Example 7
• Lemma 1: SpecIBT preserves safety
• Lemma 2: Backwards compiler correctness of SpecIBT
• proof : Proof outline