一句话：提出值依赖信息流类型系统与编译变换，抵御所有已知 Spectre 攻击并在 Jasmin 中验证实现。
Spectre 攻击会在推测执行中泄漏秘密，破坏常时密码代码的安全性。已有工作仅能低开销防御 Spectre-v1，其他变体尤其 Spectre-RSB 仍缺乏保护。本文提出一种组合方案：一个值依赖的信息流类型系统，保证推测执行下秘密不泄漏；以及一个编译器变换，将保护落实到生成的低层代码。作者在 Coq 中证明类型系统可靠性及变换正确性，并在 Jasmin 高保障密码框架中实现。评估表明，多数密码原语的全部 Spectre 防护开销低于 2%，复杂后量子密钥封装 Kyber 约为 5--7%。
Spectre attacks void the guarantees of constant-time cryptographic code by leaking secrets during speculative execution. Recent research shows that such code can be protected from Spectre-v1 attacks with minimal overhead, but leaves open the question of protecting against other Spectre variants. In this work, we design, validate, implement, and verify a new approach to protect cryptographic code against all known classes of Spectre attacks, in particular Spectre-RSB. Our approach combines a new value-dependent information-flow type system that ensures that no secrets leak even under speculative execution and a compiler transformation that enables it on the generated low-level code. We first prove the soundness of the type system and the correctness of the compiler transformation using the Coq proof assistant. We then implement our approach in the Jasmin framework for high-assurance cryptography and demonstrate that the overhead incurred by all Spectre protections is below 2% for most cryptographic primitives and reaches only about 5--7% for the more complex post-quantum key-encapsulationkmechanism Kyber.
@inproceedings{OlmosBCGL0SY025,
title = {Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants)},
author = {Santiago Arranz Olmos and Gilles Barthe and Chitchanok Chuengsatiansup and Benjamin Gregoire and Vincent Laporte and Tiago Oliveira and Peter Schwabe and Yuval Yarom and Zhiyuan Zhang},
booktitle = {ASPLOS},
year = {2025},
doi = {10.1145/3676641.3716015}
}