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
Germany (DE)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