60 citations · 119 across the 21 of their papers we have counts for
9 papers · 1 filter
Automated Template-free Synthesis of Instruction-Centric Leakage Contracts for Black-Box CPUs
Elvira Moreno, Tiziano Marinaro, Ryan Williams +4
Side-channel attacks pose a significant security threat for modern computing platforms, because they exploit subtle discrepancies in CPU behaviors to leak sensitive information. To…
Detecting speculative leaks with compositional semantics
Xaver Fabian, Marco Guarnieri, Boris Köpf +4
Speculative execution enhances processor performance by predicting intermediate results and executing instructions based on these predictions. However, incorrect predictions can le…
Computationally Bounded Robust Compilation and Universally Composable Security
Robert Künnemann, Marco Patrignani, Ethan Cecchetti
Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and…
Robust Constant-Time Cryptography
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi +4
The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory…
Secure Composition of Robust and Optimising Compilers
Matthis Kruse, Michael Backes, Marco Patrignani
To ensure that secure applications do not leak their secrets, they are required to uphold several security properties such as spatial and temporal memory safety as well as cryptogr…
Automatic Detection of Speculative Execution Combinations
Xaver Fabian, Marco Guarnieri, Marco Patrignani
Modern processors employ different prediction mechanisms to speculate over different kinds of instructions. Attackers can exploit these prediction mechanisms simultaneously in orde…
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya +7
Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm -- and a…
Contract-Aware Secure Compilation
Marco Guarnieri, Marco Patrignani
Microarchitectural attacks exploit the abstraction gap between the Instruction Set Architecture (ISA) and how instructions are actually executed by processors to compromise the con…
Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract)
Deepak Garg, Catalin Hritcu, Marco Patrignani +2
We map the space of soundness criteria for secure compilation based on the preservation of hyperproperties in arbitrary adversarial contexts, which we call robust hyperproperty pre…