60 citations · 71 across the 5 of their papers we have counts for
5 papers
Corten - Foundational Verification of Rust Programs
František Farka, Carmine Abate, Sven Linker +1
We present Corten, a foundational verification framework for Rust programs in the Rocq theorem prover, built on the Iris separation logic framework. Corten provides the first seman…
Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
Carmine Abate, Matteo Busi, Stelios Tsampas
The most prominent formal criterion for secure compilation is full abstraction, the preservation and reflection of contextual equivalence. Recent work introduced robust compilation…
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…