一句话：提出只需构造近似反向翻译的通用技术，使源语言无法嵌入目标语言时仍能证明编译器完全抽象。
编译器完全抽象（full abstraction）能保证目标语言攻击者的能力不超过源语言攻击者，具有重要安全价值，但其证明通常很复杂。常见证明技术是把目标层程序上下文反向翻译为行为等价的源层上下文，然而当源语言不足以嵌入目标语言的编码时（例如从 STLC 编译到 ULC，源语言缺少递归类型）该技术失效。本文提出只需构造近似反向翻译即可：该翻译在一定步数内是精确的，超出后则是保守的，即生成的上下文可能在原上下文不发散时发散，但反之不成立。作者基于非对称的跨语言逻辑关系，并创新性地使用 step-indexing 来刻画上下文与其近似反向翻译之间的关系，给出了通用的完全抽象证明技术。该技术在 STLC 到 ULC 的编译器上得到演示，可轻松扩展到模块化编译等常见模式，并且据作者所知是首个在 Coq 中完全机器化的编译器完全抽象证明。
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 STLC to ULC, the lack of recursive types in the former 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 STLC to ULC. 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. The proof extends easily to common compiler patterns such as modular compilation and it, to the best of our knowledge, it is the first compiler full abstraction proof to have been fully mechanised in Coq. We believe this proof technique can scale to challenging settings and enable simpler, more scalable proofs of compiler full-abstraction.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{DevriesePPK17,
title = {Modular, Fully-abstract Compilation by Approximate Back-translation},
author = {Dominique Devriese and Marco Patrignani and Frank Piessens and Steven Keuchel},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:2)2017}
}