Spectre is here to stay: An analysis of side-channels and speculative execution

TL;DR

This paper analyzes speculative side-channel attacks like Spectre, introduces models to understand them, evaluates mitigations, and concludes that hardware vulnerabilities pose significant challenges for software security, prompting a shift to process isolation.

Contribution

It introduces a mathematical meta-model and an architectural model to analyze speculative vulnerabilities and evaluates software mitigations, proving some are correct but highlighting the difficulty of comprehensive solutions.

Findings

Speculative vulnerabilities can defeat language-enforced confidentiality.

Software mitigations are limited and may not fully prevent side-channel attacks.

Shift to process isolation is necessary for security in browsers like Chrome.

Abstract

The recent discovery of the Spectre and Meltdown attacks represents a watershed moment not just for the field of Computer Security, but also of Programming Languages. This paper explores speculative side-channel attacks and their implications for programming languages. These attacks leak information through micro-architectural side-channels which we show are not mere bugs, but in fact lie at the foundation of optimization. We identify three open problems, (1) finding side-channels, (2) understanding speculative vulnerabilities, and (3) mitigating them. For (1) we introduce a mathematical meta-model that clarifies the source of side-channels in simulations and CPUs. For (2) we introduce an architectural model with speculative semantics to study recently-discovered vulnerabilities. For (3) we explore and evaluate software mitigations and prove one correct for this model. Our analysis is informed by extensive offensive research and defensive implementation work for V8, the production JavaScript virtual machine in Chrome. Straightforward extensions to model real hardware suggest these vulnerabilities present formidable challenges for effective, efficient mitigation. As a result of our work, we now believe that speculative vulnerabilities on today's hardware defeat all language-enforced confidentiality with no known comprehensive software mitigations, as we have discovered that untrusted code can construct a universal read gadget to read all memory in the same address space through side-channels. In the face of this reality, we have shifted the security model of the Chrome web browser and V8 to process isolation.