2020/06/26 by Carmine Abate, Abate, Carmine, Matteo Busi +3
Computer Science · #Security and Verification in Computing #Logic, programming, and type systems #Cryptography and Data Security
paper · pdf · doi:10.48550/arxiv.2006.14969
The most prominent formal criterion for secure compilation is full\nabstraction, the preservation and reflection of contextual equivalence. Recent\nwork introduced robust compilation, defined as the preservation of robust\nsatisfaction of hyperproperties, i.e., their satisfaction against arbitrary\nattackers. In this paper, we initially set out to compare these two approaches\nto secure compilation. To that end, we provide an exact description of the\nhyperproperties that are robustly satisfied by programs compiled with a fully\nabstract compiler, and show that they can be meaningless or trivial. We then\npropose a novel criterion for secure compilation formulated in the framework of\nMathematical Operational Semantics (MOS), guaranteeing both full abstraction\nand the preservation of robust satisfaction of hyperproperties in a more\nsensible manner.\n