Name
Abstract | ||
|---|---|---|
Since the advent of Spectre, a number of counter-measures 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.In this paper (1) we put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and (2) 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. A scalability analysis indicates that checking speculative non-interference does not exhibit fundamental bottlenecks beyond those inherited by symbolic execution. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1109/SP40000.2020.00011 | 2020 IEEE Symposium on Security and Privacy (SP) |
Keywords | DocType | Volume |
Spectector,principled detection,speculative information flows,speculative execution attacks,symbolic execution,Spectre countermeasures,speculative noninterference,vioation detection,scalability analysis | Journal | abs/1812.08639 |
ISSN | ISBN | Citations |
1081-6011 | 978-1-7281-3498-7 | 7 |
PageRank | References | Authors |
0.45 | 0 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marco Guarnieri | 1 | 7 | 1.46 |
| Boris Köpf | 2 | 599 | 25.51 |
| José F. Morales | 3 | 88 | 11.95 |
| Jan Reineke | 4 | 223 | 13.87 |
| Andrés Sánchez | 5 | 7 | 0.45 |