Détails sur le séminaire

Room 206 (2nd floor, badged access)

10 octobre 2019 - 15h00
Spectector: Principled detection of speculative information flows
par Jan Reineke de Universität des Saarlandes

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. 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.

Les tranparents de la presentation.

Contact | Plan du site | Site réalisé avec SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4001342