Detecting speculative leaks with compositional semantics

TL;DR

This paper introduces a formal framework based on speculative non-interference to detect and analyze security leaks caused by speculative execution, and presents a tool called Spectector for practical vulnerability detection.

Contribution

It proposes a novel semantic security notion for speculative execution and develops a compositional analysis framework and tool for verifying program security against such leaks.

Findings

Spectector effectively detects speculative execution vulnerabilities.

The framework models complex interactions of multiple speculation mechanisms.

Evaluations show the approach's effectiveness on benchmarks and new vulnerabilities.

Abstract

Speculative execution enhances processor performance by predicting intermediate results and executing instructions based on these predictions. However, incorrect predictions can lead to security vulnerabilities, as speculative instructions leave traces in microarchitectural components that attackers can exploit. This is demonstrated by the family of Spectre attacks. Unfortunately, existing countermeasures to these attacks lack a formal security characterization, making it difficult to verify their effectiveness. In this paper, we propose a novel framework for detecting information flows introduced by speculative execution and reasoning about software defenses. The theoretical foundation of our approach is speculative non-interference (SNI), a novel semantic notion of security against speculative execution attacks. SNI relates information leakage observed under a standard non-speculative semantics to leakage arising under semantics that explicitly model speculative execution. To capture their combined effects, we extend our framework with a mechanism to safely compose multiple speculative semantics, each focussing on a single aspect of speculation. This allows us to analyze the complex interactions and resulting leaks that can arise when multiple speculative mechanisms operate together. On the practical side, we develop Spectector, a symbolic analysis tool that uses our compositional framework and leverages SMT solvers to detect vulnerabilities and verify program security with respect to multiple speculation mechanisms. We demonstrate the effectiveness of Spectector through evaluations on standard security benchmarks and new vulnerability scenarios.