Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 19:00 - 19:18 at PriSC - Formal analysis & proof techniques Chair(s): Marco Patrignani, Jonathan Protzenko

Many secure compilation chains aim at ensuring that if there is no attack a source context can mount against a source program then there is no attack an adversarial target context can mount against the compiled program. One may, for instance, try to prevent attacks against trace properties (e.g., safety), hyperproperties (e.g., noninterference), or relational hyperproperties (e.g., observational equivalence).

Proving that these compilation chains are secure is, however, challenging. For any target attack one has to exhibit a source context mounting the same attack against the source program. Such back-translations can be highly complex, especially for hyperproperties and relational hyperproperties.

We describe a novel back-translation technique that results in simpler proofs, which can be more easily mechanized in a proof assistant like Coq. Given any number of finite trace prefixes, our back-translation builds a single source context producing these prefixes. We see the finite set of trace prefixes as a tree of events, and use state in the back-translated context to record the current position in this tree. The back-translation is done in many small steps, each adding to the tree new information describing how the location should change depending on how the context regains control. To prove such a back-translation correct we give semantics to every intermediate tree language and prove many small forward simulations, basically seeing the back-translation as a verified nanopass compiler.

This technique allows us to prove in Coq a strong secure compilation criterion for an existing simple compilation chain that was previously only proved to satisfy a weaker criterion.

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

19:00 - 20:30
Formal analysis & proof techniquesPriSC at PriSC
Chair(s): Marco PatrignaniStanford University, USA / CISPA, Germany, Jonathan ProtzenkoMicrosoft Research, Redmond
19:00
18m
Talk
Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs
PriSC
Pre-print Media Attached
19:18
18m
Talk
Explicit Leakage: Handling Side-Channel Behavior in Program Rewriting and Analysis
PriSC
Marc GourjonHamburg University of Technology and NXP Semiconductors Germany GmbH
Media Attached
19:36
18m
Talk
Secure Optimization Through Opaque Observations
PriSC
Son Tuan VuSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert CohenGoogle, Karine HeydemannSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Arnaud de GrandmaisonARM, Christophe GuillonSTMicroelectronics
Pre-print Media Attached File Attached
19:54
18m
Talk
The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
PriSC
Carmine AbateMax Planck Institute for Security and Privacy, Bochum, Germany, Matteo BusiUniversità di Pisa - Dipartimento di Informatica
Pre-print Media Attached File Attached
20:12
18m
Talk
Toward Complete Stack Safety for Capability Machines
PriSC
Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University
Media Attached File Attached