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

The most prominent formal criterion for secure compilation is full abstraction, the preservation and reflection of contextual equivalence. Recent work introduced robust compilation, defined as the preservation of robust satisfaction of hyperproperties, i.e., their satisfaction against arbitrary attackers. In this extended abstract we provide a high-level presentation of our findings in comparing these two approaches to secure compilation. Our goal is to make our results accessible to an audience interested in formal methods for secure compilation, but non necessarily familiar with some of the required background from category theory.

Extended abstract (main.pdf)489KiB
Slides (prisc22.pdf)689KiB

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