1

AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures
In recent years, several hardware-based countermeasures proposed to mitigate Spectre attacks have been shown to be insecure. To enable …
Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, Gururaj Saileshwar
PDF Cite Project
Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks
Mainstream compilers implement different countermeasures to prevent specific classes of speculative execution attacks. Unfortunately, …
Xaver Fabian, Marco Patrignani, Marco Guarnieri, Michael Backes
PDF Cite Code Project arXiv version
Testing side-channel security of cryptographic implementations against future microarchitectures
How will future microarchitectures impact the security of existing cryptographic implementations? As we cannot keep reducing the size …
Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom
PDF Cite Code Project arXiv version Distinguished paper award
Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors
Microarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as …
Gideon Mohr, Marco Guarnieri, Jan Reineke
PDF Cite Code Project Project arXiv version
Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts
Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such …
Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, Marco Guarnieri
PDF Cite Code Project Extended version (arXiv) Distinguished paper award
Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing
Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing …
Oleksii Oleksenko, Marco Guarnieri, Boris Köpf, Mark Silberstein
PDF Cite Code Project Extended version (arXiv)
Automatic Detection of Speculative Execution Combinations
Modern processors employ different speculation mechanisms to speculate over different kinds of instructions. Attackers can exploit …
Xaver Fabian, Marco Patrignani, Marco Guarnieri
PDF Cite Code Project Extended version (arXiv) Distinguished paper award
Anosy: Approximated Knowledge Synthesis with Refinement Types for Declassification
Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is …
Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker
PDF Cite Code DOI Extended version (arXiv)
Hardware-Software Contracts for Secure Speculation
Since the discovery of Spectre, a large number of hardware mechanisms for secure speculation have been proposed. Intuitively, more …
Marco Guarnieri, Boris Köpf, Jan Reineke, Pepe Vila
PDF Cite Code Project Project Poster Slides Video Extended version (arXiv) Preview video Best paper award
Exorcising Spectres with Secure Compilers
Attackers can access sensitive information of programs by exploiting the side-effects of speculatively-executed instructions using …
Marco Patrignani, Marco Guarnieri
PDF Cite Project Extended version (arXiv)