The Spectre speculative side-channel attacks pose formidable threats for security. Research has shown that code following the cryptographic constant-time discipline can be efficiently protected against Spectre v1 using a selective variant of Speculative Load Hardening (SLH). SLH was, however, not strong enough for protecting non-cryptographic code, leading to the introduction of Ultimate SLH, which provides protection for arbitrary programs, but has too large overhead for general use, since it conservatively assumes that all data is secret. In this paper we introduce a flexible SLH notion that achieves the best of both worlds by generalizing both Selective and Ultimate SLH. We give a suitable security definition for such transformations protecting arbitrary programs: any transformed program running with speculation should not leak more than what the source program leaks sequentially. We formally prove using the Rocq prover that two flexible SLH variants enforce this relative security guarantee. As easy corollaries we also obtain that, in our setting, Ultimate SLH enforces our relative security notion, and two selective SLH variants enforce speculative constant-time security.

翻译：Spectre推测侧信道攻击对安全构成严峻威胁。研究表明，遵循密码学常数时间规范的代码可以通过选择性推测加载硬化（SLH）变体有效防御Spectre v1攻击。然而，SLH对于非密码学代码的保护强度不足，这促使了终极SLH的提出——该方案可为任意程序提供保护，但由于保守地假设所有数据均为秘密，其开销过大而难以广泛应用。本文提出一种灵活的SLH框架，通过泛化选择性与终极SLH方案实现优势融合。我们为此类保护任意程序的转换机制建立了适配的安全定义：经转换的程序在推测执行时的信息泄露量不应超过源程序在顺序执行时的泄露量。利用Rocq证明器，我们形式化验证了两种灵活SLH变体能够强制执行这种相对安全性保证。作为直接推论，我们进一步证明：在当前框架下，终极SLH满足我们提出的相对安全定义，而两种选择性SLH变体则能实现推测常数时间安全性。