FSLH: Flexible Mechanized Speculative Load Hardening

TL;DR

This paper introduces a flexible speculative load hardening technique that balances security and performance, protecting arbitrary programs against Spectre attacks with formal security guarantees.

Contribution

It generalizes existing SLH methods into a flexible framework with formal security proofs, improving protection for non-cryptographic code.

Findings

Flexible SLH achieves strong security guarantees.

Formal proof confirms security properties of the proposed variants.

Encompasses existing SLH methods as special cases.

Abstract

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.