This paper introduces Triosecuris, 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). Triosecuris is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and RSB misspeculation for returns and set the SLH misspeculation flag. We formalize Triosecuris 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.

翻译：本文提出Triosecuris，一种针对Spectre BTB、RSB和PHT的形式化验证防御方案，它将基于CET的硬件辅助控制流完整性保护与编译器插入的推测加载硬化技术相结合。Triosecuris基于一个新颖的观察：在存在CET风格保护的情况下，我们可以精确检测间接调用的BTB误推测和返回的RSB误推测，并设置SLH误推测标志。我们在Rocq中将Triosecuris形式化为一种变换，并提供了机器验证的证明，表明其实现了相对安全性：任何经过变换的程序在推测执行时泄露的信息不超过源程序在无推测执行时泄露的信息。这一强大的安全保证适用于任意程序，即使那些不遵循密码学恒定时间编程规范的程序也不例外。