The high-level benefits of low-level sandboxing

Sammler M, Garg D, Dreyer DR, Litak T (2019)


Publication Type: Journal article

Publication year: 2019

Journal

Article Number: 32

DOI: 10.1145/3371100

Open Access Link: https://dl.acm.org/doi/10.1145/3371100

Abstract

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.

Authors with CRIS profile

Involved external institutions

How to cite

APA:

Sammler, M., Garg, D., Dreyer, D.R., & Litak, T. (2019). The high-level benefits of low-level sandboxing. Proceedings of the ACM on Programming Languages. https://doi.org/10.1145/3371100

MLA:

Sammler, Michael, et al. "The high-level benefits of low-level sandboxing." Proceedings of the ACM on Programming Languages (2019).

BibTeX: Download