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

WINNIE : Fuzzing Windows Applications with Harness Synthesis and...

Jinho Jung (Georgia Institute of Technology), Stephen Tong (Georgia Institute of Technology), Hong Hu (Pennsylvania State University), Jungwon Lim (Georgia...

Read More

My Past Dictates my Present: Relevance, Exposure, and Influence...

Shujaat Mirza, Christina Pöpper (New York University)

Read More

Sn4ke: Practical Mutation Analysis of Tests at Binary Level

Mohsen Ahmadi (Arizona State University), Pantea Kiaei (Worcester Polytechnic Institute), Navid Emamdoost (University of Minnesota)

Read More

Why Do Programmers Do What They Do? A Theory...

Lavanya Sajwan, James Noble, Craig Anslow (Victoria University of Wellington), Robert Biddle (Carleton University)

Read More