60 citations · 85 across the 6 of their papers we have counts for
6 papers
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
Akram El-Korashy, Roberto Blanco, Jérémy Thibault +3
Proving secure compilation of partial programs typically requires back-translating an attack against the compiled program to an attack against the source program. To prove back-tra…
Formalizing Stack Safety as a Security Property
Sean Noble Anderson, Roberto Blanco, Leonidas Lampropoulos +2
The term stack safety is used to describe a variety of compiler, run-time, and hardware mechanisms for protecting stack memory. Unlike "the heap," the ISA-level stack does not corr…
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…
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…
Proof Outlines as Proof Certificates: A System Description
Roberto Blanco, Dale Miller
We apply the foundational proof certificate (FPC) framework to the problem of designing high-level outlines of proofs. The FPC framework provides a means to formally define and che…