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

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 Institute of Technology), Yonghwi Jin (Georgia Institute of Technology), Taesoo Kim (Georgia Institute of Technology)

Read More

Awakening the Web's Sleeper Agents: Misusing Service Workers for...

Soroush Karami (University of Illinois at Chicago), Panagiotis Ilia (University of Illinois at Chicago), Jason Polakis (University of Illinois at Chicago)

Read More

Bitcontracts: Supporting Smart Contracts in Legacy Blockchains

Karl Wüst (ETH Zurich), Loris Diana (ETH Zurich), Kari Kostiainen (ETH Zurich), Ghassan Karame (NEC Labs), Sinisa Matetic (ETH Zurich), Srdjan Capkun (ETH Zurich)

Read More