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

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

PGFUZZ: Policy-Guided Fuzzing for Robotic Vehicles

Hyungsub Kim (Purdue University), Muslum Ozgur Ozmen (Purdue University), Antonio Bianchi (Purdue University), Z. Berkay Celik (Purdue University), Dongyan Xu (Purdue University)

Read More

ROV++: Improved Deployable Defense against BGP Hijacking

Reynaldo Morillo (University of Connecticut), Justin Furuness (University of Connecticut), Cameron Morris (University of Connecticut), James Breslin (University of Connecticut), Amir Herzberg (University of Connecticut), Bing Wang (University of Connecticut)

Read More

Debunking Exposure Notification

Serge Vaudenay, EPFL, Switzerland

Read More