Spectector: Principled Detection of Speculative Information Flows

From bibtex.

Abstract

We develop a novel, principled approach for detecting information flows introduced by speculative execution, and for reasoning about software defenses against Spectre-style attacks. Our approach is backed by a semantic notion of security against speculative execution attacks, and it comes with an algorithm, based on symbolic execution, for proving the absence of speculative leaks. Defining security: The foundation of our approach is speculative non-interference, a novel semantic notion of security against speculative execution attacks. Speculative noninterference is based on comparing a program with respect to two different semantics: • The first is a standard, non-speculative semantics. We use this semantics as a proxy for the intended program behavior. • The second is a novel, speculative semantics that can follow mispredicted branches for a bounded number of steps before backtracking. We use this semantics to capture the effect of speculatively executed instructions. In a nutshell, speculative non-interference requires that speculatively executed instructions do not leak more information into the microarchitectural state than what the intended behavior does, i.e., than what is leaked by the standard, non-speculative semantics. To capture “leakage into the microarchitectural state”, we consider an observer of the program execution that sees the locations of memory accesses and jump targets.