Lesly-Ann Daniel (CEA, List, France), Sébastien Bardin (CEA, List, France), Tamara Rezk (Inria, France)

Spectre are microarchitectural attacks which were made public in January 2018. They allow an attacker to recover secrets by exploiting speculations. Detection of Spectre is particularly important for cryptographic libraries and defenses at the software level have been proposed. Yet, defenses correctness and Spectre detection pose challenges due on one hand to the explosion of the exploration space induced by speculative paths, and on the other hand to the introduction of new Spectre vulnerabilities at different compilation stages. We propose an optimization, coined Haunted RelSE, that allows scalable detection of Spectre vulnerabilities at binary level. We prove the optimization semantically correct w.r.t. the more naive explicit speculative exploration approach used in state-of-the-art tools. We implement Haunted RelSE in a symbolic analysis tool, and extensively test it on a well-known litmus testset for Spectre-PHT, and on a new litmus testset for Spectre-STL, which we propose. Our technique finds more violations and scales better than state-of-the-art techniques and tools, analyzing real-world cryptographic libraries and finding new violations. Thanks to our tool, we discover that index-masking, a standard defense for Spectre-PHT, and well-known gcc options to compile position independent executables introduce Spectre-STL violations. We propose and verify a correction to index-masking to avoid the problem.

View More Papers

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

Demo #3: Detecting Illicit Drone Video Filming Using Cryptanalysis

Ben Nassi, Raz Ben-Netanel (Ben-Gurion University of the Negev), Adi Shamir (Weizmann Institute of Science), and Yuval Elovic (Ben-Gurion University of the Negev)

Read More

QPEP: An Actionable Approach to Secure and Performant Broadband...

James Pavur (Oxford University), Martin Strohmeier (armasuisse), Vincent Lenders (armasuisse), Ivan Martinovic (Oxford University)

Read More

Manipulating the Byzantine: Optimizing Model Poisoning Attacks and Defenses...

Virat Shejwalkar (UMass Amherst), Amir Houmansadr (UMass Amherst)

Read More