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.