60 citations · 119 across the 21 of their papers we have counts for
23 papers
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…
Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
Xaver Fabian, Marco Patrignani, Marco Guarnieri +1
Mainstream compilers implement different countermeasures to prevent specific classes of speculative execution attacks. Unfortunately, these countermeasures either lack formal guara…
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…
Modular Information Flow through Ownership
Will Crichton, Marco Patrignani, Maneesh Agrawala +1
Statically analyzing information flow, or how data influences other data within a program, is a challenging task in imperative languages. Analyzing pointers and mutations requires…
Robust Safety for Move
Marco Patrignani, Sam Blackshear
A program that maintains key safety properties even when interacting with arbitrary untrusted code is said to enjoy \emph{robust safety}. Proving that a program written in a mainst…
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…
On the Semantic Expressiveness of Iso- and Equi-Recursive Types
Dominique Devriese, Eric Mark Martin, Marco Patrignani
Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists)…
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle
Akram El-Korashy, Stelios Tsampas, Marco Patrignani +3
Capability machines such as CHERI provide memory capabilities that can be used by compilers to provide security benefits for compiled code (e.g., memory safety). The existing C to…
Why Should Anyone use Colours? or, Syntax Highlighting Beyond Code Snippets
Marco Patrignani
Syntax highlighting in the form of colours and font diversification, is an excellent tool to provide clarity, concision and correctness to writings. Unfortunately, this practice is…
Memory Safety Preservation for WebAssembly
Marco Vassena, Marco Patrignani
WebAssembly (Wasm) is a next-generation portable compilation target for deploying applications written in high-level languages on the web. In order to protect their memory from unt…
Universal Composability is Robust Compilation
Marco Patrignani, Robert Künnemann, Riad S. Wahby
This paper discusses the relationship between two frameworks: universal composability (UC) and robust compilation (RC). In cryptography, UC is a framework for the specification and…
Exorcising Spectres with Secure Compilers
Marco Patrignani, Marco Guarnieri
Attackers can access sensitive information of programs by exploiting the side-effects of speculatively-executed instructions using Spectre attacks. To mitigate theses attacks, popu…
Trace-Relating Compiler Correctness and Secure Compilation
Carmine Abate, Roberto Blanco, Stefan Ciobaca +6
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equiva…
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
Carmine Abate, Roberto Blanco, Deepak Garg +3
(CROPPED TO FIT IN ARXIV'S SILLY LIMIT. SEE PDF FOR COMPLETE ABSTRACT.) We are the first to thoroughly explore a large space of formal secure compilation criteria based on robust p…
Robustly Safe Compilation or, Efficient, Provably Secure Compilation
Marco Patrignani, Deepak Garg
Secure compilers generate compiled code that withstands many target-level attacks such as alteration of control flow, data leaks or memory corruption. Many existing secure compiler…
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…
Modular, Fully-abstract Compilation by Approximate Back-translation
Dominique Devriese, Marco Patrignani, Frank Piessens +1
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have import…
On Modular and Fully-Abstract Compilation -- Technical Appendix
Marco Patrignani, Dominique Devriese, Frank Piessens
Secure compilation studies compilers that generate target-level components that are as secure as their source-level counterparts. Full abstraction is the most widely-proven propert…