Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual
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 OctDisplayed 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 15mTalk | 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 15mTalk | A compilation method for dynamic typing in MLVirtual Research Papers | ||
14:20 15mTalk | 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 15mTalk | 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 20mLive 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 15mTalk | 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 15mTalk | A compilation method for dynamic typing in MLVirtual Research Papers | ||
22:20 15mTalk | 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 15mTalk | 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 20mLive Q&A | Q&A and discussionVirtual Research Papers |