Fully-abstract compilation by approximate back-translation
Fully-abstract compilation by approximate back-translation
复制标题
通过近似反向翻译进行完全抽象编译
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Frank Piessens
中科院分区：
文献类型：
--
作者：
Dominique Devriese;Marco Patrignani;Frank Piessens
如果从源语言程序到目标语言程序的编译反映并保持了行为等价性，则编译器是完全抽象的。这种编译器具有重要的安全益处，因为它们将攻击者与目标语言程序交互的能力限制为攻击者与源语言程序交互的能力。然而，证明编译器的完全抽象性是相当复杂的。一种常见的证明技术是基于将目标级程序上下文反向转换为行为上等价的源级上下文。然而，当源语言不足以嵌入目标语言的编码时，构建这样的回译是有问题的。例如，当从简单类型的λ演算(λτ)编译为非类型的λ演算(λu)时，λτ中缺少递归类型会阻止这种反向转换。我们为这个问题提出了一个通用而优雅的解决方案。关键的洞察力是，它足以构建一个近似的回译。这种近似只有在一定的步数以下才是准确的，在这之后是保守的，因为回译产生的语境可能会在原文不会发散的情况下出现分歧，但反之亦然。基于这一认识，我们描述了一种证明编译器完全抽象的通用技术，并在从λτ到λu的编译器上进行了演示。该证明使用了非对称的跨语言逻辑关系，并创新性地使用了步进索引来表达语境与其近似回译之间的关系。我们相信这种证明技术可以扩展到具有挑战性的设置，并使编译器完全抽象的证明更简单、更具可伸缩性。
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interacting with the program in the target language to that of an attacker interacting with the program in the source language. Proving compiler full-abstraction is, however, rather complicated. A common proof technique is based on the back-translation of target-level program contexts to behaviourally-equivalent source-level contexts. However, constructing such a back-translation is problematic when the source language is not strong enough to embed an encoding of the target language. For instance, when compiling from the simply-typed λ-calculus (λτ) to the untyped λ-calculus (λu), the lack of recursive types in λτ prevents such a back-translation. We propose a general and elegant solution for this problem. The key insight is that it suffices to construct an approximate back-translation. The approximation is only accurate up to a certain number of steps and conservative beyond that, in the sense that the context generated by the back-translation may diverge when the original would not, but not vice versa. Based on this insight, we describe a general technique for proving compiler full-abstraction and demonstrate it on a compiler from λτ to λu . The proof uses asymmetric cross-language logical relations and makes innovative use of step-indexing to express the relation between a context and its approximate back-translation. We believe this proof technique can scale to challenging settings and enable simpler, more scalable proofs of compiler full-abstraction.