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.

翻译：推测执行通过预测中间结果并基于这些预测执行指令来提升处理器性能。然而，错误的预测可能导致安全漏洞，因为推测性指令在微架构组件中留下痕迹，攻击者可加以利用。Spectre攻击系列即证明了这一点。遗憾的是，针对这些攻击的现有防御措施缺乏形式化的安全特征描述，使得验证其有效性变得困难。本文提出了一种新颖的框架，用于检测推测执行引入的信息流并对软件防御进行推理。该框架的理论基础是推测性无干扰（SNI），这是一种针对推测执行攻击的新型安全语义概念。SNI将标准非推测语义下观察到的信息泄露与显式建模推测执行语义下产生的泄露关联起来。为捕获其综合效应，我们在框架中引入了一种机制，安全地组合多个分别聚焦于推测单一方面的推测语义。这使得我们能够分析当多个推测机制共同运行时可能产生的复杂交互及其导致的泄露。在实践方面，我们开发了Spectector——一种符号分析工具，它利用我们的组合框架并借助SMT求解器检测漏洞，并验证程序在多种推测机制下的安全性。我们在标准安全基准测试和新型漏洞场景上评估了Spectector的有效性。