SPECTECTOR: Principled detection of speculative information flows

Abstract

Since the advent of SPECTRE, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. We present a novel, principled approach for reasoning about software defenses against SPECTRE-style attacks. Our approach builds on speculative non-interference, the first semantic notion of security against speculative execution attacks. We develop SPECTECTOR, an algorithm based on symbolic execution for automatically proving speculative non-interference, or detecting violations. We implement SPECTECTOR in a tool, and we use it to detect subtle leaks – and optimizations opportunities – in the way major compilers place SPECTRE countermeasures.

Publication
In 41st IEEE Symposium on Security and Privacy.
Marco Guarnieri
Marco Guarnieri
Assistant professor

My research focuses on the design, analysis, and implementation of secure systems.