一句话：提出 Speculation-Passing Style 程序变换，将推测常量时间验证可靠完备地归约到常量时间验证。
推测常量时间（SCT）工具常由常量时间（CT）工具提升而来，但其精确定义和形式分析不足。本文提出 Speculation-Passing Style（SPS）程序变换，将 SCT 验证归约到 CT 验证：为程序引入表示攻击者可控预测的新输入，并令程序沿预测执行。该变换可靠且完备：程序 SCT 当且仅当其 SPS 变换 CT。作者将 SPS 与三种 CT 验证方法结合——归约到非干扰、断言安全和动态污点分析，并分别在 EasyCrypt、Binsec/Rel、CTGrind 中实现，在 Kocher 的 Spectre-v1 基准上评估，还讨论了扩展到其他 Spectre 变体和泄漏模型。
Constant-time (CT) verification tools are commonly used for detecting potential side-channel vulnerabilities in cryptographic libraries. Recently, a new class of tools, called speculative constant-time (SCT) tools, has also been used for detecting potential Spectre vulnerabilities. In many cases, these SCT tools have emerged as liftings of CT tools. However, these liftings are seldom defined precisely and are almost never analyzed formally. The goal of this paper is to address this gap, by developing formal foundations for these liftings, and to demonstrate that these foundations can yield practical benefits. Concretely, we introduce a program transformation, coined Speculation-Passing Style (SPS), for reducing SCT verification to CT verification. Essentially, the transformation instruments the program with a new input that corresponds to attacker-controlled predictions and modifies the program to follow them. This approach is sound and complete, in the sense that a program is SCT if and only if its SPS transform is CT. Thus, we can leverage existing CT verification tools to prove SCT; we illustrate this by combining SPS with three standard methodologies for CT verification, namely reducing it to noninterference, assertion safety, and dynamic taint analysis. We realize these combinations with three existing tools, EasyCrypt, Binsec/Rel , and CTGrind , and we evaluate them on Kocher’s benchmarks for Spectre-v1. Our results focus on Spectre-v1 in the standard CT leakage model; however, we also discuss applications of our method to other variants of Spectre and other leakage models.
@article{paperbot3820,
title = {(Dis)Proving Spectre Security with Speculation-Passing Style},
author = {Santiago Arranz-Olmos and Gilles Barthe and Lionel Blatter and Xingyu Xie and Zhiyuan Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798222}
}