Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
Carmine Abate, Matteo Busi, Stelios Tsampas

TL;DR
This paper compares full abstraction and robust compilation in secure compilation, revealing limitations of existing approaches and proposing a new criterion that ensures both properties in a meaningful way.
Contribution
It introduces a novel secure compilation criterion within Mathematical Operational Semantics that unifies full abstraction and robust hyperproperty preservation.
Findings
Fully abstract compilation can satisfy trivial or meaningless hyperproperties.
Existing robust compilation may not adequately reflect meaningful hyperproperties.
The proposed criterion guarantees both full abstraction and robust hyperproperty preservation.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Logic, programming, and type systems · Advanced Malware Detection Techniques
