Write a Blog >>
APLAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Sun 17 Oct 2021 14:20 - 14:35 at Zurich D - Compilation / Transformation Chair(s): Sam Lindley
Sun 17 Oct 2021 22:20 - 22:35 at Zurich D - Compilation / Transformation (mirror) Chair(s): Xin Zhang

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 paper, we initially set out to compare these two approaches to secure compilation. To that end, we provide an exact description of the hyperproperties that are robustly satisfied by programs compiled with a fully abstract compiler, and show that they can be meaningless or trivial. We then propose a novel criterion for secure compilation formulated in the framework of Mathematical Operational Semantics (MOS), guaranteeing both full abstraction and the preservation of robust satisfaction of hyperproperties in a more sensible manner.

Sun 17 Oct

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

13:50 - 15:10
Compilation / TransformationResearch Papers at Zurich D +8h
Chair(s): Sam Lindley The University of Edinburgh, UK
13:50
15m
Talk
A Dictionary-Passing Translation of Featherweight GoVirtual
Research Papers
Martin Sulzmann Karlsruhe University of Applied Sciences, Germany, Stefan Wehr Offenburg University of Applied Sciences
14:05
15m
Talk
A compilation method for dynamic typing in MLVirtual
Research Papers
Atsushi Ohori Tohoku University, Japan, Katsuhiro Ueno Tohoku University
14:20
15m
Talk
Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual
Research Papers
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
14:35
15m
Talk
Hybrid quantum-classical circuit simplification with the ZX-calculusVirtual
Research Papers
Agustín Borgna Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France and Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91405, Orsay, France, Simon Perdrix Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay
14:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

21:50 - 23:10
Compilation / Transformation (mirror)Research Papers at Zurich D
Chair(s): Xin Zhang Peking University
21:50
15m
Talk
A Dictionary-Passing Translation of Featherweight GoVirtual
Research Papers
Martin Sulzmann Karlsruhe University of Applied Sciences, Germany, Stefan Wehr Offenburg University of Applied Sciences
22:05
15m
Talk
A compilation method for dynamic typing in MLVirtual
Research Papers
Atsushi Ohori Tohoku University, Japan, Katsuhiro Ueno Tohoku University
22:20
15m
Talk
Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual
Research Papers
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
22:35
15m
Talk
Hybrid quantum-classical circuit simplification with the ZX-calculusVirtual
Research Papers
Agustín Borgna Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France and Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91405, Orsay, France, Simon Perdrix Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay
22:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers