论文标题
完全抽象和稳健的汇编以及如何调和两者，抽象
Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
论文作者
论文摘要
安全汇编最突出的正式标准是完全抽象，保存和反映上下文对等。最近的工作引入了强大的汇编，定义为保留对超专业的强大满意度，即他们对任意攻击者的满意度。在本文中，我们最初着手比较这两种确保汇编的方法。为此，我们提供了对使用完全抽象的编译器编译的程序来牢固满足的超专业的确切描述，并表明它们可以毫无意义或微不足道。然后，我们提出了一个新的标准，用于在数学操作语义（MOS）的框架中提出的安全汇编，以保证以更明智的方式保证完全抽象和保留对超普罗代理的强大满意度。
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.
