Fully abstract compilation to JavaScript
Fully abstract compilation to JavaScript
复制标题
完全抽象编译为 JavaScript
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
B. Livshits
中科院分区：
文献类型：
--
作者：
C. Fournet;N. Swamy;Juan Chen;Pierre;Pierre;B. Livshits
许多工具允许程序员使用高级语言开发应用程序，并通过编译为JavaScript将其部署到Web浏览器中。虽然实用且广泛使用，但这些编译器是临时的：不能保证它们对整个程序的正确性，也不能保证它们对在任意JavaScript上下文中执行的程序的安全性。本文提出了一个具有这种保证的编译器。我们编译了一个类似ML的语言，使用高阶函数和对JavaScript的引用，同时保留了所有源程序属性。依赖于基于类型的不变量和应用性双相似性，我们显示了充分的抽象：两个程序在所有源上下文中是等价的，当且仅当它们的包装翻译在所有JavaScript上下文中是等价的。我们评估我们的编译器上的示例程序，包括一系列的安全库。
Many tools allow programmers to develop applications in high-level languages and deploy them in web browsers via compilation to JavaScript. While practical and widely used, these compilers are ad hoc: no guarantee is provided on their correctness for whole programs, nor their security for programs executed within arbitrary JavaScript contexts. This paper presents a compiler with such guarantees. We compile an ML-like language with higher-order functions and references to JavaScript, while preserving all source program properties. Relying on type-based invariants and applicative bisimilarity, we show full abstraction: two programs are equivalent in all source contexts if and only if their wrapped translations are equivalent in all JavaScript contexts. We evaluate our compiler on sample programs, including a series of secure libraries.