Search papers, labs, and topics across Lattice.
This paper introduces a novel semantic framework, speculative non-interference (SNI), for formally reasoning about information leakage due to speculative execution in processors. The framework uses compositional semantics to model different aspects of speculation and their interactions, enabling the analysis of complex speculative vulnerabilities. They implement Spectector, a symbolic analysis tool based on SNI, and demonstrate its effectiveness in detecting vulnerabilities and verifying program security against multiple speculation mechanisms on standard benchmarks.
Formalizing speculative execution vulnerabilities with compositional semantics allows for automated detection and verification, moving beyond ad-hoc countermeasures.
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.
