近似反向翻译实现的模块化、完全抽象编译
摘要：编译器的全抽象性是指从源语言程序到目标语言程序的编译反映和保持行为等价性。这种编译器具有重要的安全性优势，因为它限制了与目标语言程序交互的攻击者的能力，以与与源语言程序交互的攻击者相同。然而，证明编译器的全抽象性非常复杂。一种常见的证明技术基于将目标级别的程序上下文反向转换为行为等价的源级别上下文。然而，当源语言不足以嵌入目标语言的编码时，构造这样的反向转换是有问题的。例如，当从简单类型lambda演算（STLC）编译到无限优先级lambda演算（ULC）时，前者缺乏递归类型，因此无法进行这样的反向转换。 我们提出了一个通用而优雅的解决方案来解决这个问题。关键的洞察力是只需要构建一个近似的反向转换即可。这个近似只在一定数量的步骤上准确，而在此之上保守，即由反向转换生成的上下文在原始上下文不会发散，但反之亦然。基于这个洞察力，我们描述了一种通用的技术来证明编译器的全抽象性，并在从STLC到ULC的编译器上进行了演示。该证明使用了不对称跨语言逻辑关系，并创新地使用步骤索引来表达上下文及其近似的反向转换之间的关系。该证明可轻松扩展到常见的编译器模式，如模块化编译，并且据我们所知，这是第一个在Coq中完全机械化的编译器全抽象性证明。我们相信这种证明技术可以应用于具有挑战性的情况，并使编译器全抽象性的证明更简单、更可扩展。
作者：Dominique Devriese, Marco Patrignani, Frank Piessens, Steven Keuchel
论文ID：1703.09988
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22