FSLH：灵活的机械化推测加载加固技术

Spectre推测侧信道攻击构成严峻的安全威胁。研究表明，遵循密码学常数时序规范的代码可通过选择性变体的推测加载加固（Speculative Load Hardening, SLH）有效抵御Spectre v1。然而，SLH对非密码学代码的保护力度不足，导致引入Ultimate SLH，该方法为任意程序提供保护，但因保守地假设所有数据均为机密，导致通用使用时的开销过大。本文我们提出一种灵活的SLH概念，通过对Selective和Ultimate SLH的通用化，实现两者的优势。我们给出适合保护任意程序的安全定义：运行于推测执行的转换后程序不应泄露超过源程序顺序执行时泄露的更多信息。我们使用Rocq证明器形式化证明两种灵活SLH变体强制执行此相对安全保证。作为直接推论，我们也获得在本设置下，Ultimate SLH执行我们的相对安全概念，两种选择性SLH变体执行推测常数时序安全。