preservation and reflection of contextual equivalence. Recent work introduced robust
compilation, defined as the preservation of robust satisfaction of hyperproperties, ie, 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 …