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.

翻译：本文介绍SpecIBT，一种针对Spectre BTB、RSB和PHT攻击的经形式化验证防御方案，其结合了CET风格硬件辅助控制流完整性与编译器插入的推测式加载加固（SLH）。SpecIBT基于一项新颖发现：在存在CET风格保护机制的情况下，我们能够精确检测间接调用的BTB推测失误并设置SLH推测失误标志。我们将SpecIBT形式化为Rocq中的转换规则，并提供了机器验证证明，证实其实现相对安全性：任何经过转换的程序在推测执行环境下泄露的信息，不会超过源程序在非推测执行环境下泄露的信息。这一强安全保证适用于任意程序，包括那些未遵循密码学恒定时间编程规范的程序。