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 non-interference, assertion safety and dynamic taint analysis. We realize these combinations with three existing tools, EasyCrypt, BINSEC, 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.

翻译：恒定时间验证工具通常用于检测密码学库中潜在的侧信道漏洞。最近，一类称为推测恒定时间工具的新型工具也被用于检测潜在的Spectre漏洞。在许多情况下，这些推测恒定时间工具作为恒定时间工具的提升版本出现。然而，这些提升很少被精确定义，且几乎从未经过形式化分析。本文的目标是通过为这些提升建立形式化基础来填补这一空白，并证明这些基础能带来实际效益。具体而言，我们引入了一种称为推测传递式的程序转换方法，用于将推测恒定时间验证归约为恒定时间验证。本质上，该转换通过引入对应攻击者控制预测的新输入来对程序进行插装，并修改程序以遵循这些预测。该方法具有完备性：一个程序是推测恒定时间的当且仅当其推测传递式变换是恒定时间的。因此，我们可以利用现有恒定时间验证工具来证明推测恒定时间性质；我们通过将推测传递式与三种标准恒定时间验证方法（即归约为非干涉性、断言安全性和动态污点分析）相结合来展示这一能力。我们使用三种现有工具EasyCrypt、BINSEC和ctgrind实现了这些组合，并在Kocher的Spectre-v1基准测试集上进行了评估。我们的研究结果主要关注标准恒定时间泄漏模型中的Spectre-v1；同时我们也讨论了该方法在其他Spectre变体及其他泄漏模型中的应用。