SPECTECTOR: Principled Detection of Speculative Information Flows

SPECTECTOR: Principled Detection of Speculative Information Flows
Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, Andrés Sánchez
(Submitted on 20 Dec 2018)

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.

https://arxiv.org/abs/1812.08639

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s