8 citations · 14 across the 7 of their papers we have counts for
4 papers · 1 filter
FSLH: Flexible Mechanized Speculative Load Hardening
Jonathan Baumann, Roberto Blanco, Léon Ducruet +2
The Spectre speculative side-channel attacks pose formidable threats for security. Research has shown that code following the cryptographic constant-time discipline can be efficien…
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco +8
We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become…
Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract)
Guglielmo Fachini, Catalin Hritcu, Marco Stronati +5
We propose a new formal criterion for secure compilation, providing strong security guarantees for components written in unsafe, low-level languages with C-style undefined behavior…
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…