Lesly-Ann Daniel (CEA List), Sébastien Bardin (CEA List, Université Paris-Saclay), Tamara Rezk (INRIA)

Spectre attacks are microarchitectural attacks exploiting speculative execution in processors that were made public in 2018. Since then, several tools have been proposed to detect vulnerabilities to Spectre attacks in software. However, most of these tools do not scale on real world binary code---especially for the Spectre-STL, or Spectre-v4, variant exploiting store-to-load dependencies. We propose an optimization for symbolic execution to make it more efficient for Spectre analysis, implement it in a tool, Binsec/Haunted, and evaluate it on cryptographic libraries.

In this talk, we focus on the experimental part of our work. In particular, we discuss several concerns regarding Spectre vulnerability detection: how to make the result not too difficult to interpret, how to validate our results while ground truth is not easily accessible, etc. More generally, we also address experimental methodology relevant to binary-level analysis and symbolic execution: how to specify secret/public input at binary level, how to evaluate our choices regarding the solver and the construction of the formula, etc.

Speaker's biographies

Lesly-Ann Daniel is a third year PhD student at CEA List, working under the supervision of Sébastien Bardin and Tamara Rezk. She is interested in the application of formal methods for software security, in particular in the context of binary analysis. Currently, she works on designing automatic verification tools for security properties at binary level, with applications to constant-time cryptography, secret-erasure, and detection of Spectre attacks. She received her master’s degree in 2018 from the University of Rennes (France).

View More Papers

(Short) Spoofing Mobileye 630’s Video Camera Using a Projector

Ben Nassi, Dudi Nassi, Raz Ben Netanel and Yuval Elovici (Ben-Gurion University of the Negev)

Read More

Google/Apple Exposure Notification Due Diligence

Douglas Leith and Stephen Farrell (Trinity College Dublin)

Read More

Evaluating Personal Data Control In Mobile Applications Using Heuristics

Alain Giboin (UCA, INRIA, CNRS, I3S), Karima Boudaoud (UCA, CNRS, I3S), Patrice Pena (Userthink), Yoann Bertrand (UCA, CNRS, I3S), Fabien Gandon (UCA, INRIA, CNRS, I3S)

Read More

Oblivious DNS over HTTPS (ODoH): A Practical Privacy Enhancement...

Sudheesh Singanamalla*†, Suphanat Chunhapanya*, Jonathan Hoyland*, Marek Vavruša*, Tanya Verma*, Peter Wu*, Marwan Fayed*, Kurtis Heimerl†, Nick Sullivan*, Christopher Wood* (*Cloudflare Inc. †University of Washington)

Read More