The High-Level Benefits of Low-Level Sandboxing

Sandboxing is a common technique for allowing 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 what exactly are the end-to-end guarantees that sandboxing affords programmers. In this paper, we fill this gap by exploring formally how sandboxing ensures the robust safety of trusted code, i.e. safety in the presence of arbitrary untrusted code. First, we present an idealized operational semantics for a language that combines trusted code with sandboxed untrusted code. 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 the “any” type, we develop a mechanism for automatically converting values between the “any” type and much richer types. All results of this paper are mechanized in the Coq proof assistant.