Automatic Detection of Speculative Execution Combinations

TL;DR

This paper introduces a flexible framework and tool for reasoning about and verifying security vulnerabilities caused by combined speculative execution mechanisms in modern processors, addressing limitations of previous fixed models.

Contribution

We develop a novel, extensible semantics for speculative execution that supports reasoning about multiple combined mechanisms, integrated into the Spectector verification tool.

Findings

Successfully verified code vulnerable to Spectre variants v1, v4, and v5.

Extended Spectector to handle combined speculation mechanisms.

Demonstrated security guarantees for complex speculative execution scenarios.

Abstract

Modern processors employ different prediction mechanisms to speculate over different kinds of instructions. Attackers can exploit these prediction mechanisms simultaneously in order to trigger leaks about speculatively-accessed data. Thus, sound reasoning about such speculative leaks requires accounting for all potential mechanisms of speculation. Unfortunately, existing formal models only support reasoning about fixed, hard-coded mechanisms of speculation, with no simple support to extend said reasoning to new mechanisms. In this paper we develop a framework for reasoning about composed speculative semantics that capture speculation due to different mechanisms and implement it as part of the Spectector verification tool. We implement novel semantics for speculating over store and return instructions and combine them with the semantics for speculating over branches. Our framework yields speculative semantics for speculating over any combination of those instructions that are secure by construction, i.e., we obtain these security guarantees for free. The implementation of our novel semantics in Spectector let us verify existing codebases that are vulnerable to Spectre v1, Spectre v4, and Spectre v5 vulnerabilities as well as new snippets that are only vulnerable to their compositions.