Скачать или смотреть [PriSC'26] FSLH: Flexible Mechanized Speculative Load Hardening

FSLH: Flexible Mechanized Speculative Load Hardening (Video, PriSC 2026)
Jonathan Baumann, Roberto Blanco, Léon Ducruet, Sebastian Harwig, and Cătălin Hriţcu
(Max Planck Institute for Security and Privacy (MPI-SP; Max Planck Institute for Security and Privacy (MPI-SP; Aarhus University; MPI-SP and Ruhr University Bochum; MPI-SP)

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 recent work, 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 Selective SLH enforces speculative constant-time security.


Presentation at the PriSC 2026 workshop, Jan 11, 2026, https://popl26.sigplan.org/home/prisc...
Sponsored by ACM SIGPLAN.