(Dis)Proving Spectre Security with Speculation-Passing Style

TL;DR

This work addresses formal gaps in lifting constant-time verification to speculative constant-time SCT tools by introducing Speculation-Passing Style SPS, a program transformation that makes speculative leakage behave like sequential leakage. It proves a sound and complete reduction: a program is SCT if and only if its SPS transform is CT, enabling the reuse of existing CT verification techniques. The authors develop end-to-end verification workflows by combining SPS with non-interference, assertion safety, and dynamic taint analysis, showcasing practical verification on Spectre-v1 benchmarks with EasyCrypt, BINSEC, and ctgrind. They extend the framework to fine-grained leakage models and Spectre-v4, and provide an artifact with mechanized proofs and evaluation materials to support replication and broader adoption.

Abstract

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.

Figures (15)

• Figure 1: The program in (\ref{['fig:init:original']}) is CT but vulnerable to Spectre-v1, and (\ref{['fig:init:protected']}) is its protected version using SelSLH. The programs in (\ref{['fig:init:sps-insecure']}) and (\ref{['fig:init:sps-protected']}) show the application of SPS to the previous two, which internalizes speculation as part of the program.
• Figure 2: Transformation of the program in \ref{['fig:init:sps-protected']} for non-interference verification.
• Figure 3: Speculative semantics of the source language.
• Figure 4: Speculation-Passing Style transformation.
• Figure 5: Selected rules of the fine-grained semantics of the source language.

Theorems & Definitions (16)

• Theorem
• Definition 3.1: ${{\mathphi}\text{-SCT}}$
• Definition 3.2: ${{\mathphi}\text{-CT}}$
• Theorem 4.1: Soundness and Completeness of SPS
• Corollary 4.2: Reduction of SCT to CT
• Lemma 5.1: Reduction of Fine-Grained SCT to Fine-Grained CT
• Theorem 6.1: Reduction of SCT to CT for Spectre-v4
• Theorem 7.1: Soundness and Completeness of Assertion Elimination for CT
• Theorem 7.2: Soundness and Completeness of RHL for CT
• Corollary 7.3: Soundness and Completeness of RHL for SCT