Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly

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.