Sat 22 Jan 2022 15:30 - 15:55 at Independence - Secure compilation theory Chair(s): Arthur Azevedo de Amorim

Proving secure compilation of partial programs typically requires back-translating a target attack against the compiled program to an attack against the source program. To prove this back-translation step, one can syntactically translate the target attacker to a source one—i.e., syntax-directed back-translation—or show that the interaction traces of the target attacker can also be produced by source attackers—i.e., trace-directed back-translation.

Syntax-directed back-translation is not suitable when the target attacker uses unstructured control flow that the source language cannot directly represent. Trace-directed back-translation works with such syntactic dissimilarity because only the external interactions of the target attacker have to be mimicked in the source, not its internal control flow. Revealing only external interactions is, however, inconvenient when sharing memory via unforgeable pointers, since information about stashed pointers to shared memory gets lost. This made prior proofs complex, since the generated attacker had to stash all reachable pointers.

In this work, we introduce more informative data-flow traces, which allow us to combine the best of syntax-directed and trace-directed back-translation. Our data-flow back-translation is simple, handles both syntactic dissimilarity and memory sharing well, and we have proved it correct in Coq.

We, moreover, develop a novel turn-taking simulation relation and use it to prove a recomposition lemma, which is key to reusing compiler correctness in such secure compilation proofs. We are the first to mechanize such a recomposition lemma in a proof assistant in the presence of memory sharing.

We put these two key innovations to use in a secure compilation proof for a code generation compiler pass between a safe source language with pointers and components, and a target language with unstructured control flow.

Extended Abstract (paper.pdf)365KiB

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:05 - 16:20
Secure compilation theoryPriSC at Independence
Chair(s): Arthur Azevedo de Amorim Boston University
Composing Secure CompilersRemote
Matthis Kruse CISPA Helmholtz Center for Information Security, Marco Patrignani CISPA Helmholtz Center for Information Security / Stanford University
File Attached
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking SimulationRemote
Akram El-Korashy Max Planck Institute for Software Systems (MPI-SWS), Roberto Blanco Max Planck Institute for Security and Privacy (MPI-SP), Jérémy Thibault MPI-SP, Adrien Durier Max Planck Institute for Security and Privacy (MPI-SP), Cătălin Hriţcu MPI-SP, Deepak Garg MPI-SWS
Pre-print Media Attached File Attached
The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How to Reconcile the Two, AbstractlyRemote
Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8
DOI Pre-print File Attached