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

Deceptive Deletions for Protecting Withdrawn Posts on Social Media...

Mohsen Minaei (Visa Research), S Chandra Mouli (Purdue University), Mainack Mondal (IIT Kharagpur), Bruno Ribeiro (Purdue University), Aniket Kate (Purdue University)

Read More

icLibFuzzer: Isolated-context libFuzzer for Improving Fuzzer Comparability

Yu-Chuan Liang, Hsu-Chun Hsiao (National Taiwan University)

Read More

EarArray: Defending against DolphinAttack via Acoustic Attenuation

Guoming Zhang (Zhejiang University), Xiaoyu Ji (Zhejiang University), Xinfeng Li (Zhejiang University), Gang Qu (University of Maryland), Wenyuan Xu (Zhejing University)

Read More

What Remains Uncaught?: Characterizing Sparsely Detected Malicious URLs on...

Sayak Saha Roy, Unique Karanjit, Shirin Nilizadeh (The University of Texas at Arlington)

Read More