AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

The recent Spectre attacks exploit speculative execution and microarchitectural side channels, such as caches, to leak sensitive information. Since the underlying hardware vulnerabilities are here to stay in billions of deployed devices, software countermeasures have been developed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. We put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and we develop Spectector, an algorithm based on symbolic execution to automatically prove speculative non-interference, or to detect violations. We implement Spectector in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place Spectre countermeasures.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only