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.
Fri 24 Jan
|10:30 - 10:51|
Mengqi LiuYale University, Lionel RiegVerimag, Zhong ShaoYale University, Ronghui GuColumbia University, David CostanzoYale University, Jung-Eun KimYale University, Man-Ki YoonYale UniversityLink to publication DOI Media Attached File Attached
|10:51 - 11:13|
Michael SammlerMPI-SWS, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8Link to publication DOI Media Attached
|11:13 - 11:35|
Li-yao XiaUniversity of Pennsylvania, Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Gregory MalechaBedRock Systems, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of PennsylvaniaLink to publication DOI Media Attached File Attached