Write a Blog >>

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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

10:30 - 11:35: Research Papers - Verification in Proof Assistants at Ile de France III (IDF III)
Chair(s): Sandrine BlazyUniv Rennes- IRISA
POPL-2020-Research-Papers10:30 - 10:51
Mengqi LiuYale University, Lionel RiegVerimag, Zhong ShaoYale University, Ronghui GuColumbia University, David CostanzoYale University, Jung-Eun KimYale University, Man-Ki YoonYale University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers10:51 - 11:13
Michael SammlerMPI-SWS, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8
Link to publication DOI Media Attached
POPL-2020-Research-Papers11: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 Pennsylvania
Link to publication DOI Media Attached File Attached