一句话：证明沙箱化可使受信任代码在任意不可信代码存在时仍保持类型安全（鲁棒安全），并在Coq中机械化验证。
先前工作仅关注沙箱化的底层内存隔离保证，未回答其对程序员的端到端保证。本文证明沙箱化使程序能推理鲁棒安全（robust safety）：受信任代码在存在任意不可信代码时仍安全。作者首先为一个结合受信任与不可信代码的语言提出理想化操作语义，并将沙箱化内建其中。然后证明：只要与不可信代码的所有交互都发生在“any”类型（所有值所属的类型），受信任代码通过丰富类型系统实施的安全属性在任意不可信代码存在下仍得以保持。为减轻只能以“any”类型交互的负担，作者形式化并证明若干包装器（wrappers）的安全性，可自动在“any”类型与更丰富类型间转换值。所有结果均在 Coq 证明助手中机械化。
Sandboxing is a common technique that allows low-level, untrusted components to safely interact with trusted code. However, previous work has only investigated the low-level memory isolation guarantees of sandboxing, leaving open the question of the end-to-end guarantees that sandboxing affords programmers. In this paper, we fill this gap by showing that sandboxing enables reasoning about the known concept of robust safety , i.e. , safety of the trusted code even in the presence of arbitrary untrusted code. To do this, we first present an idealized operational semantics for a language that combines trusted code with untrusted code. Sandboxing is built into our semantics. Then, we prove that safety properties of the trusted code (as enforced through a rich type system) are upheld in the presence of arbitrary untrusted code, so long as all interactions with untrusted code occur at the “any” type (a type inhabited by all values). Finally, to alleviate the burden of having to interact with untrusted code at only the “any” type, we formalize and prove safe several wrappers , which automatically convert values between the “any” type and much richer types. All our results are mechanized in the Coq proof assistant.
@article{paperbot572,
title = {The high-level benefits of low-level sandboxing},
author = {Michael Sammler and Deepak Garg and Derek Dreyer and Tadeusz Litak},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371100}
}