The High-Level Benefits of Low-Level Sandboxing
MICHAEL SAMMLER, MPI-SWS and Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
DEEPAK GARG, MPI-SWS, Germany
DEREK DREYER, MPI-SWS, Germany
TADEUSZ LITAK, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
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 isbuilt into our semantics. Then, we prove that safety properties of the trusted code (as enforced through a richtype 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 tointeract 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.
CCS Concepts: • Security and privacy → Logic and verification; • Theory of computation → Programming logic.
Additional Key Words and Phrases: Sandboxing, robust safety, Iris, type systems, logical relations, languagebased security
ACM Reference Format:
Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak. 2020. The High-Level Benefits of Low-Level
Sandboxing. Proc. ACM Program. Lang. 4, POPL, Article 32 (January 2020), 32 pages. https://doi.org/10.1145/
3371100

1 INTRODUCTION
The Internet makes it easy to download useful software components from untrusted authors.
While it is convenient to integrate such untrusted components into a trusted (i.e., otherwise safe)
application, doing so also incurs security risks. The untrusted code could violate the integrity ofthe trusted application’s private data structures, steal secrets, or take over the system and installmalicious software. In all these cases, the untrusted code violates expected safety properties of thetrusted application. Thus, it is important to ensure that an application maintains its expected safety
properties even when linked and co-executed with arbitrary untrusted code. This is often called
Authors’ addresses: Michael Sammler, MPI-SWS, Saarland Informatics Campus, Germany, msammler@mpi-sws.org,
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany; Deepak Garg, MPI-SWS, Saarland Informatics Campus, Germany, dg@mpi-sws.org; Derek Dreyer, MPI-SWS, Saarland Informatics Campus, Germany, dreyer@mpi-sws.org; Tadeusz
Litak, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany, tadeusz.litak@fau.de.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
This
work
licensed under a Creative Commons Attribution 4.0 International License.
contact
theisowner/author(s).
© 2020 Copyright held by the owner/author(s).
2475-1421/2020/1-ART32
https://doi.org/10.1145/3371100
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32

32:2

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

robust safety [Grumberg and Long 1994; Gordon and Jeffrey 2001; Fournet et al. 2007; Abadi 1997;
Bugliesi et al. 2011; Swasey et al. 2017].
One common engineering technique for ensuring secure interoperation between trusted anduntrusted code is to physically sandbox the untrusted parts of an application at coarse granularity
using hardware, kernel, or library support for isolation. Memory is partitioned into low and highcompartments, and the hardware and kernel enforce that untrusted codeÐsandboxed in the low
compartmentÐcannot directly access the memory in the high compartment (where trusted code
operates) even if it can guess private memory addresses of the trusted code [Koning et al. 2017].
Additionally, untrusted code cannot directly access system calls. Examples of such techniques aresoftware fault isolation by rewriting untrusted code [Yee et al. 2009], in-user-space sandboxing of
untrusted libraries [Mozilla 2019; Lamowski et al. 2017; Google 2019; Vahldiek-Oberwagner et al.
2019], use of multiple kernel-backed address spaces within an application [Litton et al. 2016], andthe use of modern features of CPUs like secure enclaves [McKeen et al. 2013; ARM Limited 2009].
Although sandboxing is widely used, and prior work has shown formally that specific sandboxing
techniques attain intrinsic properties like memory isolation, to the best of our knowledge there isno clear understanding of what end-to-end reasoning sandboxing affords programmers. Our goalin this paper is precisely to fill this gap: we show that sandboxing allows programmers to reason
about the robust safety of trusted code. As explained above, robust safety is a well-studied concept,
which means that the trusted code’s safety properties hold even when co-executing with arbitrary
untrusted code. In verification terms, sandboxing allows reasoning about the safety properties oftrusted code without having to consider the behavior of untrusted code during verification.
To formalize this, we start by designing an idealized but representative operational semantics
with built-in sandboxing. Next, we formally show that, if untrusted code is properly sandboxed,robust safety is an automatic (free) consequence of verifying safety properties of the trusted code
without any assumptions about the types of values it receives from untrusted code. Specifically, if
we verify a safety property of trusted code assuming that all its interactions with the untrusted
code are at a type we call anyÐwhich includes all values of the languageÐthen that safety property
also holds when the trusted code runs co-linked with any untrusted code.
As an add-on, we extend our formalization to another low-level engineering technique thatis commonly used in conjunction with sandboxing. This technique, often called łwrappingž orłmarshallingž [Mozilla 2019; Lamowski et al. 2017; Google 2019; Swasey et al. 2017], dynamicallyconverts values between types that two different components of an application use internally. In
the context of sandboxing, where we assume nothing of the untrusted code, wrapping can be used
to convert between types that the trusted code understands and the type any. This allows the
programmer to write typed interfaces between trusted and untrusted code; wrapping automaticallytakes care of checking and transforming values at runtime so that the actual interactions between
trusted and untrusted code are at type any, as required by our first result.
Although wrappers simplify the programmer’s task, they obviously move the onus of security to
the correctness of the wrappers. Thus, as a second contribution, we design and verify an (extensible)
library of wrappers that convert between the types of a rich type system and the type any. Our
wrappers go beyond existing work in two ways. First, our type system includes substructural (affine)features and ownership types to a limited extent, modeling some aspects of modern languages like
Rust [The Rust Developers 2019], and we show how dynamic wrapping can handle such features.
Second, sandboxing imposes low-level requirements on wrappersÐfor example, when exporting an
object from trusted to untrusted code, a wrapper must also copy the object from the high to the
low compartment, as untrusted code cannot access the high compartment.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:3

Relation to existing work. The idea of robust safety originated in the context of modular model
checking [Grumberg and Long 1994]. Early security-related work by Gordon and Jeffrey [2001]
presents a type system for the spi calculus wherein each program that can be typed at the special Un
type is robustly safe against arbitrary untrusted code. Several other papers use similar ideas [Fournet
et al. 2007; Abadi 1997; Bugliesi et al. 2011]. More recent work by Swasey et al. [2017] applies ideas
from robust safety to the verification of object capability patterns. They use a program logic basedon Iris [Jung et al. 2018b] to allow modular reasoning about the trusted code in a language similar
to JavaScript. However, all this previous work on robust safety focuses on languages with abstract
memory models, where it is possible to hide a secret memory location by simply not sharing it with
untrusted code. Sandboxing is not useful in this setting. In contrast, we are interested in robust
safety in the presence of a concrete (low-level) memory model where the untrusted code is more
powerful in that it can guess or compute memory addresses of the trusted code and dereference
them. This justifies the need for sandboxing.
There is also work on verification of sandboxing techniques like software-fault isolation [Besson
et al. 2019; Morrisett et al. 2012], architectural meta-data tagging (micro-policies) [de Amorim et al.
2015], and architectural memory capabilities [El-Korashy 2016]. However, these verification efforts
are directed at meta-theoretic correctness properties of the sandboxing mechanisms themselves,e.g., that sandboxed code cannot directly access memory outside the sandbox. In contrast, our work
establishes how sandboxing contributes to the robust verification of an application that uses the
sandbox. In fact, our operational semantics builds in a correct, abstract sandbox, and all our work
is done relative to this operational semantics.
Wrappers are a widely deployed software-engineering tool. They are primarily used to reduce development effort and improve software maintainability, but in some applications, notably Mozilla’s
Firefox [Mozilla 2019], wrappers are also used to improve security. Wrappers are often combinedwith sandboxing in practice, e.g., in Lamowski et al. [2017], but they are typically limited to marshalling and unmarshalling records of first-order values. In contrast, our wrappers cover a richtype system with affine and ownership types, and we show how these types can be wrapped
and unwrapped securely. The design of our wrappers is inspired by work on higher-order contracts [Findler and Felleisen 2002; Blume and McAllester 2004]. Prior work like that of Swasey et al.
[2017] has verified several common wrappers but in an abstract memory model. Our wrappers are
instead verified in a low-level memory model in the context of sandboxing, which results in very
different proof requirements.
Summary of contributions and technical work. We give the first formal account of the high-level(end-to-end) benefits of low-level sandboxing. We apply the idea of robust safety to sandboxing inthe setting of a concrete (low-level) memory model where addresses can be guessed or computed apriori, thus obtaining strong end-to-end guarantees about the behavior of trusted code when linked
with arbitrary sandboxed code. Additionally, through a library of verified wrappers, we show how
several common types (including affine and ownership types) can be wrapped and unwrapped at
sandbox boundaries, thus allowing seamless integration of untrusted code into the verification of atrusted application.
Our technical contributions are as follows:• We idealize and formalize memory and system call isolation using a small core calculus whichbuilds in two memory partitions and two compartments (one trusted and one untrusted)ś this is the simplest but also one of the most common settings for sandboxing. Section 3
introduces this language (called λ sandbox ) and its operational semantics.
• After introducing a rich affine type system for λ sandbox in Section 4, we show formally thatsandboxing yields a principle for robust verification of safety properties of a typed λ sandbox
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:4

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

main ≜ λ _.

mainsandbox ≜ λ _.
fork {gated_call(untrusted_main, ())};
let l = alloc(1);let l = alloc(1);l ← 42;l ← 42;
syscall(unsafe_print, !l)syscall(unsafe_print, !l)Fig. 1. Example applications without and with calling untrusted code.

program. Specifically, it is enough to verify (via typing) only the trusted compartment ofa program, so long as it assumes nothing about the values it is passed from the untrusted
compartment. Section 5 shows that every safety property we establish of the trusted compartment holds while it inter-operates with anything in the untrusted compartmentÐeven
code that can guess arbitrary memory locations.
• We introduce an extensible, verified system of wrappers between trusted and untrusted codethat allows typed interaction with untrusted code. While these type-directed wrappers are
not essential for security, they significantly simplify the integration of the untrusted code
into a typed, trusted application. Section 6 introduces the system for wrapping and shows
several examples of wrappers of varying complexity.
• In Section 7, we briefly justify the soundness of our formal development by describing asemantic model for the type system.
We conclude in Section 8 with a discussion of related work. All our technical work is fully mechanized in Coq on top of the Iris framework for higher-order concurrent separation logic [Jung et al.
2018b]. The Coq development is available online at [Sammler et al. 2019].
2 KEY IDEAS
In this section we introduce the key ideas of our work using two examples of concrete (trusted)
applications that interact with sandboxed untrusted code.
Unsafe printing. Our first example is contrived but illustrative. Assume that the operating systemprovides a system call unsafe_print that prints its numerical argument on the screen. This systemcall, however, has one fatal flaw: When called with a number with more than three decimal digits,
it will overflow an internal buffer of the kernel. Thus, the security goal ś a safety property ś is toensure that unsafe_print is never called with an argument greater than 999.
A reader familiar with the usual definition of safety in the programming languages literaturemight expect an additional condition that the program must not get stuck in a small-step operationalsemantics. However, it is not possible to fulfill this condition in our setting where programs may
include arbitrary untrusted code as such code could cause stuckness trivially by crashing the
program. Consequently, standard program safety (non-stuckness) is not what we are after. Instead,
we formalize our safety properties (only) on traces of externally visible behavior of the program,i.e., the sequences of system calls executed by the program. In our example, we will consider aprogram safe as long as any trace of system calls it creates does not include any unsafe_print withan argument greater than 999.
Consider two applications in Figure 1 calling unsafe_print. The first application, main, is clearlysafe since the argument to unsafe_print is a value read from a location l that previously had 42
written to it. The other application, mainsandbox , is similar to main except that it also runs a function
untrusted_main concurrently (treat the primitive gated_call simply as a call instruction in thelanguage for now). Importantly, untrusted_main is untrusted meaning that it can be arbitrary
and might try to violate the safety property outlined above. In particular, untrusted_main could
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:5

malicious untrusted code
untrusted_main1 ≜ λ _. syscall(unsafe_print, 1000)
untrusted_main2 ≜ λ _. let l = guess_location(); l ← 1000
Fig. 2. Malicious instantiations of the untrusted code.

directly invoke unsafe_print with an argument greater than 999, as illustrated by the instance
untrusted_main1 in Figure 2. Alternatively, it could guess the address of the location l and write avalue greater than 999 to it, causing the unsafe_print in the body of mainsandbox to be called withan argument greater than 999. This is illustrated by the instance untrusted_main2 in Figure 2. In
either case, the safety property is violated. Note that the second of these violations is only possible
in a low-level language, where references are computable. We deliberately choose this setting
as it is more challenging than a language with abstract references and is also closer to systems
programming languages like C.
The idea behind robust safety, as proposed in prior work, is to ensure that mainsandbox maintains
its safety property no matter what the untrusted function untrusted_main is. One way to attainthis property is to sandbox the execution of untrusted_main, i.e., to contain or limit its effects. The
primitive gated_call that wraps untrusted_main in Figure 1 in fact models such a sandbox in our
calculus. The details of the implementation of the sandbox are irrelevant for our purposes ś several
existing techniques were outlined in Section 1. Instead, we are interested in the following two
more foundational questions: (1) What properties are required of the sandbox to make mainsandbox
robustly safe, i.e., safe against any untrusted_main function provided by the untrusted code? (2)Given these properties of the sandbox, how can we prove that mainsandbox is robustly safe?
For the first question, it should be clear from the examples of Figure 2, that the sandbox must
provide at least two properties. (a) Memory isolation: The sandbox must prevent code in it fromaccessing memory locations private to code outside the sandbox. This prevents the safety violation
with untrusted_main2 by preventing this function from writing l. (b) System call isolation: To ruleout attacks like that in untrusted_main1 , the sandbox must prevent code running inside it frommaking system calls that could violate safety properties of interest. Since we would like to beable to enforce any safety property using the sandbox, it must, in fact, prevent code inside it frommaking any system call. There is still the question of whether the sandbox needs yet anotherproperty to ensure robust safety. In later sections, we answer this question in the negative for ageneral programming model with system calls and computable memory addresses. Thus, systemcall isolation and memory isolation suffice for robust safety even in a low-level setting.1
For the second question, we show in Section 5 that the use of a sandbox yields a strong principle
for verification of robust safety: if a safety property of trusted code is verified without making any
assumptions about the values it receives from untrusted code, then the safety property in fact holds
robustly. We formalize this principle by introducing a type system for verifying safety propertiesof trusted code and including a universal type any containing all values at which trusted code caninteract with untrusted code.
Wrappers. While system call isolation (with memory isolation) ensures robust safety, it can bevery restrictive for untrusted code as it disallows all access to system calls. In practice, we may
1 Prior work [Gordon and Jeffrey 2001; Fournet et al. 2007; Abadi 1997; Swasey et al. 2017] has established similar principles

for robust safety in high-level languages with abstract (non-computable) references. Our work extends those results to
low-level languages with computable references. The difference is substantial: with computable references, memory isolationmust be provided by the sandbox.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:6

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

want to give untrusted code access to system calls, but perhaps with some checks. One way to do
this is for the trusted code to expose to untrusted code an API that wraps system calls to make surethat the system calls do not violate safety properties. For instance, in our example, trusted code
may expose the following function checked_print to untrusted code.
checked_print ≜ λ x . if x < 1000 then syscall(unsafe_print, x) else stuck
This function calls unsafe_print with its argument but only if the argument is less than 1000. As aresult, it does not violate our safety property, no matter what argument is passed to it. Consequently,
this function, which is just a wrapper around unsafe_print, can be shared with untrusted code.
While it is possible to write such wrappers manually in principle, this can quickly become
unmanageable and buggy for large interfaces. It would be much less error-prone to write an API
function that describes the check x < 1000 using a type. For instance, suppose we define the type
LessThan1000 ≜ {z | z < 1000}.2 Then, a programmer could instead write the following function:
typed_print ≜ λ x : LessThan1000. syscall(unsafe_print, x)This function is much easier to write, less likely to have a bug (as it does not check its argument incode) and conveys the same intent as the function checked_print. The problem with this functionis that it maintains our safety property only when its caller passes it an argument that really is oftype LessThan1000, i.e., an argument that really is less than 1000. Since the caller here is untrusted
code, this is not guaranteed.
Ideally, we would like an automatic mechanism that converts the function typed_print, whose
argument is statically typed, into the function checked_print, whose argument may be anything(of the universal type) and which checks the expected type dynamically. This idea, which is quite
similar to runtime type checking in gradual and hybrid types [Flanagan 2006; Lehmann and Tanter2017], is often implemented in practice through a set of wrappers. A wrapper takes a function
with a typed interface (like typed_print) and converts it to a function whose argument and return
types are all universal (like checked_print), by inserting dynamic type-checks around the originalfunction.
Under the hood, wrappers rely on a type-indexed family of coercion functions τ .import : any → τand τ .export : τ → any to check the result and the arguments of the wrapped function being
exported from trusted to untrusted code. In particular, we can define the following macro that
implements a simple, generic wrapper:
wrap (v : τ → τ ′) ≜ λ x . (τ ′ .export)(v(τ .import(x))) : any → any
Each type can provide its own import and export functions. For example, import for LessThan1000
simply checks whether its argument is below 1000:
LessThan1000.import ≜ λ x . if x < 1000 then x else stuck : any → LessThan1000
However in the presence of sandboxing, the import/export function of a type may have to do morework than merely checking values. For example, the export function may have to copy the value
from the trusted code’s private memory, which is inaccessible to sandboxed untrusted code due tomemory isolation, to memory accessible in the sandbox. Further, as we show in the next example,
wrappers around affine types are particularly interesting. Such types are checked dynamically by
maintaining local state within the import/export functions. As a result, import/export functions
can be quite complex and it is imperative to verify their correctness. In Section 6, we describe suchverified import/export functions for a rich collection of types.
2 The notation and idea for this type are inspired by work on refinement types [Freeman and Pfenning 1991; Xi and Pfenning1998].

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:7

open(_) { z f∀z f .

start

closedopenread(z f ) { _close(z f ) { _Fig. 3. System call policy fileSP for file system calls.

do_open ≜ λ n. syscall(open, n) : int → file
do_read ≜ λ f . let r = syscall(read, f ); (f , r ) : file → Π(file, any)
do_close ≜ λ f . syscall(close, f ) : file → any
Fig. 4. Functions shared with untrusted code for file system example.

Wrappers with affine types. We now look at an example with a more interesting safety property.
Suppose our operating system offers three system calls to manipulate files ś open, close, and read.
The open call returns a file handle (an integer), while close and read take a previously opened
handle as argument. Importantly, if close or read are passed an invalid file handle ś one that haseither not been obtained from a previous open or one on which close has been called earlier śthen they can cause the operating system to crash. Consequently, our safety property is that thefile handle passed to read or close must have been obtained previously through open without
an intervening close on the handle. This safety property can be succinctly represented as a statemachine shown in Figure 3. The variable z f refers to a file handle and the universal quantification
at the beginning simply means that the property is really a product of the state machines for all
possible file handles.
As in the previous example, the trusted code would like to expose an API to the untrusted code
mirroring these three system calls, while ensuring robust safety. The question is what the types of
the API functions, say do_open, do_close, and do_read, should be. Since one of the concerns isthat read or close may be called with a file handle that was not obtained through open, an obvious
thing is to replace the concrete integer file handles with an abstract type file, whose instances canonly be obtained via do_open. The API can maintain a bijective association between instances offile and integer file handles using a private table.
However, this alone does not suffice. Additionally, the API must ensure that a handle on which
do_close has been called is not accidentally reused. For this, the API can declare the type fileaffine. The affineness can be enforced by removing the entry for the passed handle from the private
table in the import function of the file type and inserting it in the export function. The resulting
specification of the API (as written by the programmer) is shown in Figure 4, and the implementationof file.import and file.export is shown in Figure 5. The actual functions shared with untrusted codeare obtained by applying wrap to the three functions shown in Figure 4.
This implementation of file.import and file.export is inspired by a more general, widely-usedprogramming pattern called dynamic sealing [Morris 1973]. Prior work [Swasey et al. 2017] verified
the standard dynamic sealing pattern but to the best of our knowledge our version of dynamic
sealing with affine types is new. We verify this pattern in Section 6.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:8

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

m is a global table that maps instances of file to integer file handles:
file.import ≜ λ x . if x ∈ m then get_and_remove(m, x) else stuck : any → file
file.export ≜ λ x . let k = fresh_key(m); put(m, k, x); k : file → any
Fig. 5. Wrappers for file.

z∈Zs ∈ Name
Priv ∋ p ::= Low | HighLoc ∋ l ::= (p, zb , zo )Lit ∋ q ::= h | z | lVal ∋ v ::= q | rec f (x) = e
Expr ∋ e ::= x | v | e + e | e − e | e ≤ e | e = e | e.e | e (e) | !e | e ← e| CAS(e 0 , e 1 , e 2 ) | allocp (e) | free(e 0 , e 1 ) | case e of e | fork e| mk_location(ep , eb , eo ) | get_priv(e) | get_block(e) | get_offset(e)| syscall(s, e) | gated_call(s, e) | gated_ret(e)SurfaceExpr ∋ e ::= {e ∈ Expr | e does not contain gated_ret}
SurfaceVal ∋ v ::= {v ∈ Val | v does not contain gated_ret}
Ectx ∋ K ::= (standard left-to-right evaluation contexts)
Fig. 6. Definition of λ sandbox .

λ x . e ≜ rec _ (x) = e

let x = e 1 ; e 2 ≜ (λ x . e 2 ) (e 1 )

e 1 ; e 2 ≜ let _ = e 1 ; e 2

if e 1 then e 2 else e 3 ≜ case e 1 of e 2 , e 3

stuck ≜ 0 (0)Fig. 7. Standard derived forms.

3 LANGUAGE AND OPERATIONAL SEMANTICS
Notation. We use overline notation to denote a list (vector) of elements. If a statement contains
multiple overlines, they all represent lists of the same length.
Figure 6 shows the syntax of λ sandbox , which at its core is a standard concurrent lambda calculus
modeled after λ Rust [Jung et al. 2018a]. Standard abbreviations are displayed in Figure 7. λ sandbox
features standard binary operations and functions with multiple arguments. The heap is block-based
like in λ Rust and CompCert [Leroy et al. 2012]. Each location contains an integer block identifier
zb and an integer offset in the block zo . The expression alloc(z) allocates a fresh block of size z
initialized to the poison value h3 , free(z, l) frees the block at location l of size z, and l .z adds z to
the offset of the location l.
3 As in λRust , his a special value for uninitialized memory. All operations except storing and reading a poison value to andfrom memory get stuck.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxingfinh ∈ Heap ≜ Loc −⇀ Val

32:9

o ∈ Observation ≜ (Name, Lit, Lit) π ∈ Trace ≜ list Observationfin

I ∈ Interface ≜ (Priv, Name) −⇀ Val

A ∈ SyscallAssumptions ≜ Trace → Propp1 ⊑ p2p ⊑p

Low ⊑ HighI ⊢ h, π | e at p →A h ′, π ′ | e 1′ at p1′ , (e 2′ at p2′ )?
O-writeO-readh(l) = v ′h(l) = v
I ⊢ h, π | !l at p →A h, π | v at pl = (p ′, zb , zo )p′ ⊑ pI ⊢ h, π | l ← v at p →A h[l ← v], π | h at p

O-syscallHigh ⊑ p

A (π ++ [(s, qa , qr )])I ⊢ h, π | syscall(s, qa ) at p →A h, π ++ [(s, qa , qr )] | qr at p
O-gated-callp = High ⇔ p ′ = Low

I((p ′, s)) = v

I ⊢ h, π | gated_call(s, v) at p →A h, π | gated_ret(v (v)) at p ′O-gated-ret

p = High ⇔ p ′ = Low
I ⊢ h, π | gated_ret(v) at p →A h, π | v at p ′O-mk-locationp ′ = Low ⇔ zp = 0

zb ≥ 0l = (p ′, zb , zo )I ⊢ h, π | mk_location(zp , zb , zo ) at p →A h, π | l at p
O-get-priv

l = (p ′, zb , zo )p ′ = Low ⇒ zp = 0

p ′ = High ⇒ zp = 1

I ⊢ h, π | get_priv(l) at p →A h, π | zp at p
O-get-blockl = (p ′, zb , zo )I ⊢ h, π | get_block(l) at p →A h, π | zb at p
O-get-offset

l = (p ′, zb , zo )I ⊢ h, π | get_offset(l) at p →A h, π | zo at p
I ⊢ h, π | E −→A h ′, π ′ | E ′O-ThreadI ⊢ h, π | e at p →A h ′, π ′ | e 1′ at p1′ , (e 2′ at p2′ )?
I ⊢ h, π | E ++ [K[e] at p] ++ E ′ −→A h ′, π ′ | E ++ [K[e 1′ ] at p1′ ] ++ E ′ ++ [e 2′ at p2′ ]Fig. 8. Selected rules from the operational semantics of λ sandbox .
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:10Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

As motivated in the previous sections, we want to model strong adversaries that can guess arbitrary locations. Thus, λ sandbox provides the mk_location, get_priv, get_block, and get_offset
instructions, which allow composing/splitting a location from/into its parts. Using mk_location,
it is possible to implement the guess_location function from Section 2 by forging a high locationfrom arbitrary block and offset integers.
The non-standard rules of the thread reduction relationI ⊢ h, π | e at p →A h ′, π ′ | e 1′ at p1′ , (e 2′ at p2′ )?
are displayed in Figure 8.4 The elements of this judgment are explained below in more depth, but
at a high level it states that executing an expression e at privilege level p with the state consistingof the heap h and the trace of already-executed system calls π can result (after one step) in e 1′
at privilege level p1′ with potentially modified heap h ′ and trace π ′. Only the rule for fork uses
the optional second resulting expression (e 2′ at p2′ )? to signify that it spawned a new thread. The
functions that represent the interface between the trusted and untrusted code are contained in I.
The main reason for including concurrency in λ sandbox is to more faithfully model practicalisolation techniques, which typically operate in a concurrent setting [Mozilla 2019; Lamowski et al.
2017; Google 2019; Litton et al. 2016]. Consequently, as we will see in Section 6, we will need toverify that wrappers handle concurrent accesses correctly.
Privilege level. To differentiate code running inside the sandbox from code running outside it,
an expression e is always executed at a thread-local privilege level p. Specifically, e at High statesthat e is executing outside of the sandbox. Only the trusted code should run at High privilege.
Likewise, e at Low signifies that e runs inside the sandbox; untrusted code should always run at
Low privilege.
To switch the privilege level, λ sandbox provides a call gate mechanism, often employed by realworld sandboxing techniques [Lamowski et al. 2017; Google 2019; Litton et al. 2016; VahldiekOberwagner et al. 2019]. Namely, a switch of the privilege is combined with a call to a function
preregistered by the code on the other side of the sandbox. Such a mechanism also ensures wellbracketing of the switches, i.e., the call always returns to the code that initiated it and the privilege
is automatically switched back. This abstraction of a call gate is modeled in λ sandbox using thegated_call and gated_ret instructions. The preregistered functions are stored in the interfacefin

I : (Priv, Name) −⇀ Val
This interface I cannot be modified during run time but is fixed with the initial state of the program.
As can be seen in O-gated-call, gated_call switches the privilege from p to the opposite privilege
p ′ and calls the function registered under the name s in the interface of the target privilege p ′. The
application v (v) is wrapped into a gated_ret, which ensures that the privilege is switched backto the original privilege p once the called function finishes executing. The gated_call instruction
is bidirectional: it can be used either to enter the sandbox or to leave it.
The gated_ret instruction is an artifact of ensuring well-bracketing of the privilege switching
and thus is not a part of the surface language, existing only during execution of a program. Hence,a surface expression (surface value) is an expression (value) that does not contain a gated_ret.
Memory isolation. Now we look at how λ sandbox uses the privilege mechanism to prohibit theuntrusted code from overriding memory of the trusted code. λ sandbox models coarse-grained memory
isolation by splitting the heap into a high heap of the trusted code and a low heap of the untrusted
code via a privilege bit p in each location. A location that points to the high heap (i.e., whose
4 All rules of the operational semantics can be found in Appendix A.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:11

privilege bit is High) is called a high location, and similarly a location with p = Low is called a low
location. We chose to model coarse-grained memory isolation since it is used in most real-world
sandboxing techniques [Litton et al. 2016; Vahldiek-Oberwagner et al. 2019; Lamowski et al. 2017;
Google 2019]. The parameter p in allocp specifies in which heap the allocation lands.
O-write enforces the memory isolation by requiring that the current privilege p is no less thanthe privilege of the target location p ′, i.e., p ′ ⊑ p. Hence, code running at Low privilege that tries
to write to the high heap gets stuck. The operational semantics of alloc, free and CAS prevents
the code running at Low from modifying the high heap in a similar way.5 However, O-read allows
code running at Low to read the high heap. This means that while λ sandbox ’s memory isolation
enforces integrity of the high heap, it does not enforce confidentiality, as indeed the latter is notalways enforced by real-world isolation techniques. Moreover, our goal is to prove robust safety,
for which integrity is sufficient.
System calls and system call assumptions. Programs running on commodity operating systems
interact with their environment Ð like other programs, the file system, or the internet Ð via
system calls. Thus, from the outside the system calls of a program are its only relevant externallyvisible behavior. For this reason, λ sandbox contains a syscall instruction, which is used to define
well-behaved programs.
As O-syscall shows, system calls extend the trace π : list Observation with the observationo : (Name, Lit, Lit) consisting of the name of the system call s, the argument qa , and the value
returned by the system call qr . The set of system calls and their behavior are not fixed, but instead
they can change depending on the application that is verified. This is implemented by making the
stepping relation Ð and later also the type system Ð parametric in the system call assumptions
A : Trace → Prop, which encodes whatever assumptions the application makes about how system
calls behave. It is used to specify possible traces of system calls. This is not to be confused with thesystem call policy, which specifies good traces. For example, typing of the file-related systems callsin Figure 4 relies on the open system call returning fresh file handles, which we formalize using
the system call assumptions Afile :6
Afile ≜ λπ . ∀i 1 , i 2 , qa1 , qa2 , qr 1 , qr 2 .
πi 1 = (open, qa1 , qr 1 ) ∧ πi 2 = (open, qa2 , qr 2 ) ∧ i 1 , i 2 → qr 1 , qr 2
As motivated in Section 2, system call isolation is necessary to prevent the untrusted code fromdirectly issuing malicious system calls. This is enforced in O-syscall by checking that the current
privilege p is High. Prohibiting all system calls is very strict, and some sandboxes used in practiceallow the untrusted code to issue some system calls [Vahldiek-Oberwagner et al. 2019; Google
2019]. This can be modeled in λ sandbox by adding functions to the trusted interface that directly
execute a chosen subset of system calls.
System call policies. As previously motivated, system calls are the externally visible behavior ofa program. But how do we decide if the behavior is good or bad? In this paper, we characterize
behaviors, i.e., traces of system calls, as łgoodž if they conform to some system call policy, which
is a predicate on the trace. In contrast to the work by Swasey et al. [2017] we do not use a fixed
policy; rather, our program logic and type system are generic with respect to the system call policy,
which we specify using an automaton [Schneider 2000; Basin et al. 2013].
Definition 1. A system call policy SP is an automaton consisting of the (possibly infinite) stateospace S, an initial state st init ∈ S, and the transition function st →? st ′, which states that, upon
5 See Appendix A.
6 Actually, A

file also needs to ensure that open only returns integers, but we omit this here.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:12

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

startunsafe_print(z) { _z < 1000

Fig. 9. System call policy printSP for the unsafe_print system call.

seeing the observation o, the automaton in state st ∈ S steps to the state st ′ ∈ S ⊥ (i.e., S extended
with a łbadž state ⊥ < S). The automaton cannot leave the state ⊥, and any state except the badstate ⊥ is accepting.
For example, the system call policy governing the unsafe_print system call of Section 2 can beseen in Figure 9, and we have already seen the automaton for file-related system calls in Figure 3.
The notation s(qa ) { qr denotes the observation (s, qa , qr ). All transitions not depicted in the
diagram implicitly go to the non-accepting ⊥ state, which is also implicit.
oo
We write st →✓ st ′ to assert that st →? st ′ and st ′ is not ⊥. This can be extended to the judgmentπost →✓ st ′ on traces, which runs the automaton on the observations o in the trace π using →✓ .
This is used in the statement of the soundness theorem of the type system in Section 5, whichshows that all traces π of a program e fulfill the system call policy SP if e is well-typed with regard
to SP.
4 TYPE SYSTEM
Next we show how to verify that a λ sandbox application composed of both trusted and untrusted
code is safe. The untrusted code is assumed to be sandboxed using the semantics described in theprevious section, but the trusted code is not and needs to be verified for robust safety. As explained in
Section 2, our notion of safety is not program progress (non-stuckness), but an application-specificsafety property of system call traces (called the system call policy or SP).
To verify the trusted code, we design a semantic type system inspired by the one of λ Rust [Junget al. 2018a]. As in RustBelt, our typing judgments are defined semantically using a model built
on the Iris separation logic framework in Coq [Jung et al. 2018b]. (Also as in λ Rust , we employ anaffine type system, but we omit Rust-specific features like lifetimes and borrowing.) New types canbe added by defining their semantics in Iris, and all typing rules are then proven sound individually
as lemmas about the typing judgment. This makes it possible to easily extend our type system withnew types and typing rules over time. In this section, we describe the overall design of the typesystem, postponing the details of the model of types to Section 7.
The type system’s basic judgment, v ◁SP,A τ , states that the surface value v has the type τ . The
judgment is parameterized by a system call policy SP and system call assumptions A. As explainedin the previous section, A represents invariants that govern all system call traces, while SP is anapplication-specific safety policy. In the following we sometimes omit SP and A to reduce clutter.
Because we use a shallow embedding of typing judgments in our Coq formalization, typing
contexts do not bind variables. Rather they collect assumptions about meta-variables v, i.e., Coqvariables of type Val, which are implicitly universally quantified at the level of the typing rule. The
syntax of typing contexts is:
T SP,A ::= ∅ | T SP,A , v ◁SP,A τ
The typing judgment for expressions
T1 ⊨pSP,A e : τ | T2
states informally that, assuming the typing context T1 , the expression e is safe (for policy SP) at
privilege p and will also end its execution at privilege p. Further, if the execution results in a value
v, then the context for the continuation of e is context v ◁SP,A τ ,T2 .
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

T-weaken

32:13

T-copyT1 ⊨p e : τ | T2

T1 , v ◁ τ , v ◁ τ ⊨p e : τ | T2

τ copyT1 , v ◁ τ ⊨p e : τ | T2

T1 , v ◁ τ ⊨p e : τ | T2

T-val

v ◁τ
∅ ⊨p v : τ | ∅T-let

T-stuck

T1 ⊨p e 1 : τ1 | T2

e is stuck∅ ⊨p e : τ | T∀v. v ◁ τ1 ,T2 ,T ⊨p e 2 [v/x] : τ2 | T3

T1 ,T ⊨p let x = e 1 ; e 2 : τ2 | T3
Fig. 10. Structural typing rules.

T-any-copy

T-any

T-int-copy

T-int

T-add

any copyv ◁ any

int copyz ◁ intv 1 ◁ any, v 2 ◁ any ⊨High v 1 + v 2 : int | ∅T-alloc

T-free|any| = n

|τ | = n∅ ⊨High allocHigh (n) : Π(any) | ∅v ◁ Π(τ ) ⊨High free(n, v) : any | ∅T-writevw ◁ τw , vp ◁ Π(τp ) ⊨High vp .n ← vw : any | vp ◁ Π(τp [n ← τw ])T-read-copy

τn copy

T-readv ◁ Π(τ ) ⊨High !v.n : τn | v ◁ Π(τ )v ◁ Π(τ ) ⊨High !v.n : τn | v ◁ Π(τ [n ← any])

T-fn
T-fn-copy

T copy∀v f va . T , v f ◁ fn τa → τr , va ◁ τa ⊨High e[v f /f , va /x] : τr | ∅T ⊨High rec f (x) = e : fn τa → τr | ∅fn τa → τr copy
T-callv f ◁ fn τa → τr , va ◁ τa ⊨High v f (va ) : τr | ∅Fig. 11. Selected typing rules for the trusted code, τ [n ← τ ′ ] denotes τ with τn replaced by τ ′ .

There are two salient points about this judgment. First, it does not stipulate that e will makeprogress. It merely ensures safety with respect to SP, which is our only goal. Second, the judgment
specifies an output context T2 , since our type system is affine and thus the execution of e may result
in updates to the typing context.
Despite the type system’s general affineness, values of some types like integers can be copied
freely. We call these types copyable and write τ copy to mean that τ is copyable. This notion islifted to contexts: T copy means that all types in T are copyable.
Figure 10 shows structural typing rules. T-copy allows duplication of copyable types. T-val
embeds the typing judgments for values into that for expressions. T-stuck says that a stuck
expression e can be typed at any type. The rule is sound because a stuck expression cannot violate
the system call policy and will never evaluate to a value. In the rule T-let, the ∀v in the second
premise is meta-level quantification. It means that the judgment after it is parametric in v.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:14

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

Next, we turn to rules for specific types, shown in Figure 11. The most basic type is the universal
type any, which is inhabited by all values.7 As explained in Section 2, this type is crucial forinteraction with untrusted code. The copyable type int is the usual type of integers. (Groundintegers are denoted z.) The rule T-add exploits the fact that our type system is not designed toguarantee progress, so the arguments to + can be of type any.
λ sandbox models a low-level language so it does not have native products. Instead products are
emulated using the heap. The product type Π(τ ) is a pointer to a block of |τ | values, where thevalue at position n has the type τn . T-alloc and T-free in Figure 11 show how to allocate anddeallocate products. Writing to a product at offset n updates the corresponding type τn to the typeof the written value τw , as T-write shows. There are two rules for reading from a product. If theread type τn is copyable, it is possible to use T-read-copy, which keeps the product unchanged as
one would expect. However, if τn is not copyable, τn in the product must be replaced by any to
avoid duplication of a non-duplicable type, as T-read shows. Products themselves are not copyablebecause they own the memory that stores the elements and this ownership is non-duplicable.
Observe how T-free consumes the given argument v, reflecting this affineness.
Next, we come to the function type, written fn τa → τr . Rule T-fn says that a value is a well-typed
function of type fn τa → τr if the body of the function e substituted with values va of the argument
types τa is a well-typed expression of the return type τr . The body’s typing is also allowed toassume that all recursive occurrences f have the correct type. We insist that function types becopyable as this allows functions to be called multiple times, which is convenient in practice. Thismeans that the typing context T used to type the function in T-fn must be copyable.
System calls. An interesting aspect of typing is system calls, since this is where the policy SP and
the system call assumptions A become relevant. Clearly, it is impossible to write meaningful rules
for system calls independent of SP and A, but given a pair of SP and A, specific rules for system calls
can be proved sound. As an example, Figure 12 shows typing rules for the system calls introducedin Section 2 using the LessThan1000 and file types. Here, printSP and fileSP are the two safety
policies described in Section 2, and Afile is the system call assumptions for the file-related system
calls defined in Section 3, which ensures that open always returns a fresh identifier.
The rule for unsafe_print is self-explanatory. The rules for open, read, and close make use of thefact that the concrete representation of the abstract type file in our model coincides with the typeof file handles returned by open. Hence, we can type these system calls using the type file. The
rules also prevent the use of a closed file instance since close consumes its argument. Under thehood, the soundness of these rules relies on Iris-level ghost state. For instance, we use this ghost
state to track the set of file handles that are currently open. The interpretation of file owns oneof the file handles in this set, and close removes the file handle from this set, so we know in theprecondition of read and close that the passed handle could not have been closed previously. fileis not copyable since the ownership of the file handle cannot be duplicated. We defer the formal
details of this proof to Section 7.
Interacting with untrusted code. A second interesting aspect of our type system is the rule
for interacting with untrusted code. To call untrusted code, trusted code uses the gated_call
instruction with the following typing rule:
T-gated-callv ◁ any ⊨High gated_call(s, v) : any | ∅The rule says that it is safe (for any safety property SP) to call arbitrary code, as long as the called
code is sandboxed (forced by gated_call) and nothing is assumed about the result (the result is
7 Technically, any is inhabited only by all surface values, but this is implicit since v ◁ τ is only defined for surface values v.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:15

T-lessthan1000

z < 1000z ◁ LessThan1000

T-print
printSPv ◁ LessThan1000 ⊨High

syscall(unsafe_print, v) : any | ∅T-file-open
filev ◁ int ⊨fileSP,Asyscall(open, v) : file | ∅High

T-file-readfilev ◁ file ⊨fileSP,Asyscall(read, v) : any | v ◁ fileHighT-file-close
filesyscall(close, v) : any | ∅v ◁ file ⊨fileSP,A
High

Fig. 12. Typing rules for printSP and fileSP.

of type any). Intuitively, the rule is sound because sandboxing prevents the untrusted code fromdirectly making any system calls (system call isolation) or modifying any private memory of thetrusted code (memory isolation). We expand this intuition formally in Section 5.
Our Coq development [Sammler et al. 2019] contains many other types like sums, maps, andmutexes, the details of which we omit here due to lack of space.
5 ROBUST SAFETY OF THE TYPE SYSTEM
Robust safety of our type system has two parts. First, we justify the typing rule T-gated-callby proving in Theorem 2 that any surface expression is semantically well-typed at Low privilege.
This allows well-typed programs to make gated calls to untrusted code. Second, Theorem 3, thesoundness theorem of our type system, shows that a program that is well-typed w.r.t. a system callpolicy SP will uphold that policy no matter what code runs inside the sandbox. Together, these
theorems entail that well-typed code is robustly safe, i.e., is guaranteed to uphold the system callpolicy even when interacting with arbitrary untrusted code via gated_call.
To show that arbitrary code is safe to run inside the sandbox, we prove that all surface expressions
e are typeable at Low. We do not know anything about the value that e will evaluate to, so we canonly assign the type any:
Theorem 2 (Soundness of the sandbox). For all surface expressions e, the following rule is sound:∅ ⊨Low e : any | ∅The proof of Theorem 2 requires several assumptions about the model of the type system:(1) The trusted code may only have invariants on the high heap, not on the low heap. We needthis restriction since memory isolation only protects the high heap, and the untrusted code
can manipulate the low heap in arbitrary ways.
(2) The functions in the interface of the trusted code are safe to call at any time with any value,i.e., are of type fn any → any.
With these assumptions it is possible to show Theorem 2 by induction over e since the memory
isolation protects the invariants of the trusted code on the high heap, system call isolation prevents
the untrusted code from issuing malicious system calls, and assumption (2) ensures that eachgated_call of the untrusted code can be handled safely.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:16

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

Soundness of T-gated-call follows directly from Theorem 2. After executing the gated_callwith O-gated-call, the privilege is Low and given a function retrieved from the interface I, onemust show that its application to the supplied arguments v is safe to execute. However, this isexactly what Theorem 2 shows. Its safe execution results in a value of type any, which is returnedto the trusted code after the privilege switches back to High due to the gated_ret.
Robust safety. Now we can state the robust safety theorem, i.e., the soundness theorem for ourtype system, which is a variant what is typically called ładequacyž in semantic soundness proofs.
It shows that the trace of all executions of a well-typed program satisfies the system call policy forarbitrary untrusted code inside the sandbox:
Theorem 3 (Robust Safety). For• any untrusted code represented as arbitrary surface values vu with names su ,• any exposed functions vt of the trusted code with names st ,init ,• any system call policy SP with initial state st SP• any system call assumptions A,fin• any map from block names to initial values of global variables m : Name −⇀ list Lit,
• any value main, and• any initial context Tinit ,the following rule is sound:(1) Tinit copy(2) InitFromHeap(m,Tinit )v : fn any → any | ∅(3) Tinit ⊨SP,A
main
:
fn
[
]
→
any
|
∅
(4) ∀v ∈ vt . Tinit ⊨SP,A
High
High
(5) I = [(Low, su ) 7→ vu , (High, st ) 7→ vt ]∗(6) I ⊢ h init m, [ ] | main () at High −→Ah, π | Eπinit(7) ∃st . st SP
→✓
SP st

The main goal of this theorem is to show that every trace π produced by executing main
(assumption (6)) fulfills the system call policy SP (conclusion (7)), which is the definition of good
execution used in this paper. The rest of the theorem is a mouthful, so let us walk through it.
Assumption (5) tells us that the trusted code exposes the functions vt , while the untrusted code
consists of the surface values vu . When using this theorem, as we are going to do in Section 6, one
provides concrete values for vt while keeping vu universally quantified. This means that main isrobustly safe against linking with arbitrary untrusted code vu . Assumptions (3) and (4) state thatthe trusted code must be well-typed and thus verified; the latter is necessary to fulfill assumption(2) of Theorem 2.
Assumptions (1), (2), Tinit , and m are used to implement global variables. Some wrappers (e.g.,
dynamic sealing) need global variables to retrieve trusted state (e.g., the global sealing table), as
seen in Section 2. These global variables are represented as hard-coded locations in the trusted
code via the function g2l : Name → Loc, which turns the name of the global variable into thecorresponding location. The map m specifies the initial values for the global variables, which areused to create the initial heap h init m. The global variables can be used in (3) and (4) via the initial
context Tinit . InitFromHeap(m,Tinit ) in (2) informally states that Tinit can be established from theinitial heap h init m. Assumption (1) is necessary in order to copy Tinit so that it can be used in both
(3) and (4), and T-fn in Figure 11 requires Tinit to be copyable anyways.
Given our careful technical setup, Theorem 3 is not actually difficult to prove since the semantic
model of typing (see Section 7) is defined to make it fall out naturally. In particular, typability ofmain implies it is safe to execute and thus upholds the system call policy.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:17

6 WRAPPERS
The previous section showed that the whole program is safe if all interaction with untrusted code
happens at the any type. However, the any type is difficult to work with because it does not provide
any useful information. In order to more effectively integrate the sandbox into a typed application,
we want to make it possible for trusted code to interact with untrusted code using more richly
typed interfaces, but without sacrificing robust safety.
To this end, we propose a system of automatic checks and transformations that allows a programmer to write a trusted function with an informative type fn τa → τr and automatically lift it toa function of the type fn any → any, which can be shared with untrusted code. Dually, it allows an
untrusted function of type fn any → any to be lifted automatically to the type fn τa → τr , which
can then be applied safely at that type by trusted code.
This lifting mechanism works through a system of wrappers converting values to (or from) the
any type. We provide several examples of wrappers as a library, but the programmer can define andverify custom wrappers for whatever new types they define, thus making those types available for
automatic transformation between trusted and untrusted code (this is a one-time effort for every
new type). The verification of a wrapper works by proving that it semantically inhabits a specificfunction type.
More concretely, one can associate one or both of the following functions with each type τ :• τ .import ◁ fn any → τ : A type τ can provide an import function, which is used to check andtransform values that the untrusted code passes to the trusted code. Such a type is then called
importable. Simple types like LessThan1000 from Section 2 can be imported by checking if
the untrusted code passed a value of the type τ and either passing the value to the trusted
code or getting stuck.
• τ .export ◁ fn τ → any: By providing an export function a type τ can state how it shouldbe transformed when values of this type are passed from the trusted to the untrusted code.
Such a type is then called exportable. It is always possible to implement τ .export as theidentity function since any is inhabited by all values. However, we will see that export is still
useful, e.g., for transforming values to a representation which works inside the sandbox orconverting them to a form that can be checked by import.
If a function uses import or export of a type parameter, this function implicitly is only defined if thetype parameter is importable or exportable, respectively. The Coq formalization implements thismechanism by providing Import and Export type classes that can be implemented for importableand exportable types. For example, an implementation in Rust could use traits to associate a function
with a type.
Note that import and export can be arbitrary functions, so long as they are well-typed. This isunlike the setting of higher-order contracts [Findler and Felleisen 2002; Blume and McAllester2004] and gradual typing where, usually, wrappers can only check values but cannot modify them,and must maintain some additional properties, e.g., that importing an exported value should return
the original value [New and Ahmed 2018]. In our setting such restrictions would rule out usefulwrappers like dynamic sealing, as we will see later.
Figure 13 shows how the wrappers are used. The wrap_import macro can be used by thetrusted code when it wants to call the function s exposed by the untrusted code. It first calls thecorresponding τa .export function on each argument to transform all values in x to any. Thenwrap_import calls the untrusted code using gated_call. This call is safe due to T-gated-call andreturns a value of type any, which is checked and transformed to a value of type τr using τr .import.
In total, this means that wrap_import can be typed at type fn τa → τr , as Figure 13 shows.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:18Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

wrap_import s τa τr ≜ λ x . let x = τa .export(x); let r = gated_call(s, x); τr .import (r )wrap_export v τa τr ≜ λ x . let x = τa .import(x); let r = v (x); τr .export (r )T-wrap-import

Ta ,Tr copy
Tr ⊨High τr .import : fn any → τr | ∅Ta ⊨High τa .export : fn τa → any | ∅Ta ,Tr ⊨High wrap_import s τa τr : fn τa → τr | ∅T-wrap-export

Ta ,Tv ,Tr copy
Tv ⊨High v : fn τa → τr | ∅Ta ⊨High τa .import : fn any → τa | ∅Tr ⊨High τr .export : fn τr → any | ∅Ta ,Tv ,Tr ⊨High wrap_export v τa τr : fn any → any | ∅Fig. 13. Applying wrappers to functions. The overline notation is explained in the main text.

any.import ≜ λ x . x ◁ fn any → any int.import ≜ λ x . x + 0 ◁ fn any → int
any.export ≜ λ x . x ◁ fn any → any int.export ≜ λ x . x ◁ fn int → any
Fig. 14. import and export wrappers for any and int.
T-low-copy

T-alloc-low

T-free-low

LowPtr copy

∅ ⊨p allocLow (z) : LowPtr | ∅v ◁ LowPtr ⊨p free(z, v) : any | ∅T-write-low

T-read-low

vw ◁ any, vp ◁ LowPtr ⊨p vp .z ← vw : any | ∅v ◁ LowPtr ⊨p !v.z : any | ∅Fig. 15. Typing rules for LowPtr

The trusted code can use wrap_export when it wants to expose a function v to the untrusted
code. The sequence of arguments x is checked and transformed to values of the correct type using
τa .import. One can thus call v, which expects arguments of types τa . After the function call the
result r is exported to the untrusted code using τr .export. All in all, the signature of a function
wrapped by wrap_export is fn any → any, which can be safely exposed to the untrusted code.
We define wrap_import and wrap_export using overline notation to support an arbitrary numberof arguments. For example, the over-lined let x = τa .export(x) macro expands tolet x 1 = τa,1 .export(x 1 ); let x 2 = τa,2 .export(x 2 ); . . .
Examples of wrappers. Some of the simplest wrappers are the wrappers for any and int, which
can be seen in Figure 14. The wrappers for any are trivial since both are just the identity function.
The wrapper for importing an integer adds 0 to the value passed by the untrusted code. This
ensures that it is an integer since addition gets stuck otherwise. Thus int.import ◁ fn any → int by
T-add. Exporting an int simply returns it unchanged to the untrusted code.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:19

LowPtr.import ≜ λ x . if get_priv(x) then stuck else x ◁ fn any → LowPtr
LowPtr.export ≜λ x. x◁ fn LowPtr → any
Fig. 16. import and export wrappers for LowPtr.

LowPtr. Importing locations is more difficult than importing integers because the untrusted
code can confuse the trusted code by passing a high location where the trusted code expects a
low location. The memory isolation does not prevent the trusted code from writing to the location
since it is running at High privilege.
To prevent this confused deputy attack [Hardy 1988] we use our extensible type system to define
a new type LowPtr of low locations:T-low-ptr

l = (Low, _, _)l ◁ LowPtr

The typing rules for LowPtr are shown in Figure 15. Since there are no invariants on the low heap,
it is safe to read from and write to a LowPtr using T-read-low and T-write-low. However, thetrusted code cannot expect that a LowPtr points to any specific value even after reading it since
the untrusted code can concurrently change the value on the low heap. Thus T-read-low returns
any. This means that working with LowPtr requires some care, and it is mainly useful as a building
block for implementing import and export for other types, as we will see when introducing thewrappers for Π(τ ).
Crucially, LowPtr is importable as Figure 16 shows. LowPtr.import uses get_priv to check thatthe untrusted code actually passed in a low location and gets stuck otherwise.
There are two subtle points about LowPtr that we wish to highlight here. First, LowPtr.importrelies on the get_priv instruction; thus, a concrete sandboxing technique that wants to use theresults of this work must provide a way to distinguish a low location from a high one. Second,
LowPtr relies on the fact that a low location will never become high, even if it is deallocated andlater reallocated. Otherwise there would be a possibility of a time-of-check to time-of-use attack[Abbott et al. 1976] between LowPtr.import and a subsequent write to the LowPtr. A similar point
was made by de Amorim et al. [2018] regarding pointer reuse in memory-safe languages.
Both requirements are trivially fulfilled when using an isolation technique based on multiple
address spaces, since each pointer is permanently associated with one address space. However,programmers usually also respect these requirements even with single address-space isolation
techniques as it simplifies informal reasoning about the code [Vahldiek-Oberwagner et al. 2019].
For example, the Linux kernel has a fixed partitioning of the address space into a user range and akernel range and uses this to check pointers passed from the untrusted (user-space) code.
Products. The wrappers for the Π(τ ) type can be seen in Figure 17. Its import reads |τ | values
from the low heap, imports them with the imports of the corresponding types, and writes theimported values to a product on the high heap. Its export works the other way around by writing
the exported values of the product to the low heap. The original product is freed because thecaller gave ownership of the product to the wrapper, and thus also the responsibility for freeing its
allocation.
Notice that Π(τ ).import (and Π(τ ).export) is a macro similar to wrap_import and wrap_export
to support products of arbitrary size. The expression l .i ← τ .import(!u.i) is repeated for all types τin τ with i referring to the index of τ in τ .
The most obvious difference from the previous wrappers is that the Π(τ ).export function is notjust the identity. Products are implemented as allocations on the high heap. Simply passing a highProc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:20Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

Π(τ ).import ≜ λ x .
let u = LowPtr.import(x);let l = allocHigh (|τ |);l .i ← τ .import(!u.i);free(|τ |, u);lT copyΠ(τ ).export ≜ λ x .
let l = allocLow (|τ |);l .i ← τ .export(!x .i);free(|τ |, x);
LowPtr.export(l)T ⊨High τ .import : fn any → τ | ∅T ⊨High Π(τ ).import : fn any → Π(τ ) | ∅T copyT ⊨High τ .export : fn τ → any | ∅T ⊨High Π(τ ).export : fn Π(τ ) → any | ∅Fig. 17. import and export wrappers for Π(τ ).

location to the untrusted code is not very useful since the untrusted code could neither write to
it nor free it. Hence, the export function copies the exported values to the low heap so that theuntrusted code can manipulate them freely. This copying, which is also done by default by existing
tools [Google 2019; Lamowski et al. 2017], can be expensive, and depending on the use-case more
optimized patterns like dynamic sealing are possible.
The import function follows a similar pattern to export, but here it is vital for safety to copy thevalues from the low to the high heap, because otherwise the values could be changed after they
were checked. To check the components of the product, Π(τ ).import uses the import function ofτ ∈ τ . This generic approach to wrapping means that the wrappers compose nicely and Π(τ ) is
importable (exportable) if all types in τ are importable (exportable).
unsafe_print example. Now we have everything in place to revisit the unsafe_print example ofSection 2 and show that mainfile function is safe to execute for arbitrary untrusted code vu inside
the sandbox when exposing the wrapped typed_print function. Applying Theorem 3 with an empty
set of global variables, an empty initial context, and no system call assumptions (i.e., A ≜ λ π . True)
results in the obligations
mainsandbox ◁printSP,A fn [ ] → any

typed_print ◁printSP,A fn LessThan1000 → any

which are easy to show with the typing rules described so far. All in all, we get
I = [(Low, su ) 7→ vu , (High, typed_print) 7→ wrap_export [LessThan1000] any typed_print]∗
I ⊢ ∅, [ ] | mainsandbox () at High −→Ah, π | Eπinit→✓∃st . st printSP
printSP st

This says that if we execute mainsandbox (), which invokes the untrusted_main function of thearbitrary untrusted code vu 8 , which in turn may invoke the wrapped version of typed_print, then
the trace π of that execution adheres to the system call policy printSP.
Dynamic sealing. As motivated in Section 2 with the file example, there are types where simple
inspection cannot determine whether a value belongs to the type, e.g., integers representing valid
file handles. A popular solution to enforce the invariants of objects that are passed to untrusted
8 If the untrusted code does not expose a function named untrusted_main, this call gets stuck, which is not a problem.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:21

Sealeds,τ .import ≜ λ x .
let seal = int.import(x);let mutex_map = acquire(g2l s);
let map_unsealed = map_take(!mutex_map.1, seal);
release(!mutex_map.0, !map_unsealed.0);
unwrap(!map_unsealed.1)
Sealeds,τ .export ≜ λ x .
let mutex_map = acquire(g2l s);
let map_seal = map_put(!mutex_map.1, x);release(!mutex_map.0, !map_seal.0);
int.export(!map_seal.1)
T-sealed-importg2l s ◁ mutexmapτ ⊨High Sealeds,τ .import : fn any → Sealeds,τ | ∅T-sealed-export

g2l s ◁ mutexmapτ ⊨High Sealeds,τ .export : fn Sealeds,τ → any | ∅Fig. 18. import and export wrappers for Sealeds,τ .

mutexτ copy
type
mutexτ /guardτmapτ
optionτfunctionacquire ◁ fn mutexτ → Π(guardτ , τ )release ◁ fn guardτ , τ → any
map_put ◁ fn mapτ , τ → Π(mapτ , int)
map_take ◁ fn mapτ , int → Π(mapτ , optionτ )unwrap ◁ fn optionτ → τ

Fig. 19. Types and functions used by wrappers for Sealeds,τ .

code is to use dynamic sealing [Morris 1973]. In this approach, one passes an opaque handle insteadof the object itself. This handle is passed back to the trusted code to invoke methods on the object.
In the following we show how this pattern can be implemented in our framework in a generic way.
For this we define a new type Sealeds,τ . Block s stores the map necessary for the dynamic sealing
as will be explained later. Sealeds,τ is inhabited by the same values as τ . We employ the usual
notation for bidirectional inference rules:v ◁τT-sealed================v ◁ Sealeds,τ
The important point about Sealeds,τ is that it is importable and exportable for all types τ , evenif τ is not importable or exportable itself. It can be seen as a marker type for wrap_import andwrap_export to specify that some arguments or return values should be wrapped via dynamic
sealing instead of their own wrappers (if they have any). T-sealed makes sure that Sealeds,τ can betreated as a value of type τ during verification and thus Sealeds,τ does not influence the verificationof the trusted code.
Figure 18 shows how Sealeds,τ implements import and export using a global map that is stored
as a global variable in block s. The function export puts the exported value in the map and gets a
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:22

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

fresh seal in return. This seal is then returned to the untrusted code. The function import interprets
its argument as a seal and looks it up in the map. If this lookup succeeds, import takes the sealed
value out of the map and returns it to the trusted code. If the untrusted code passed an invalid seal
(a seal that is not in the global map), import gets stuck. Thus, the untrusted code can only pass backseals for values that have been handed out by the trusted code earlier. Since import and export
might be called concurrently, a mutex is necessary to guard access to the map.
Figure 19 shows the additional types and functions used by the wrappers for Sealeds,τ .
• mutexτ is a simple spin lock based mutex, which guards a value of type τ . The value can betaken out of the mutex with acquire, which spins until it can lock the mutex. In addition to
the value of type τ , acquire also returns a guardτ , which release uses to put back a valueof type τ into the mutex. The logic of the mutex ensures that only one thread at a time canaccess the guarded value and thus mutexτ is copyable independent of τ copy.
• mapτ is a map from integer keys to values of type τ . The function map_put stores a value oftype τ in the map and returns the updated map and the index of the newly inserted value.
The function map_take can then be used to take the value at the specified key out of the map.
It returns optionτ because the key might not be in the map. The function unwrap returns
the value contained in the option if there is any, and gets stuck otherwise.
The implementations and proofs for these types and functions can be found in the Coq development[Sammler et al. 2019]. Let us revisit the file system example of Section 2 to see how these wrappers
for dynamic sealing are used in action. The goal is to show that it is safe to expose the wrapped
do_open, do_read, and do_close functions to arbitrary untrusted code inside the sandbox.
Sealeds,τ uses a global variable to store the map used for sealing. We pick the block denoted by
the name file to store this map and fill this block in the initial heap with an empty map q init :m ≜ {file 7→ q init }This means that we have to show
 (Low, st ) 7→ vu , (High, do_open) 7→ wrap_export [int] Sealedfile,file do_open,



I=

(High,
do_read)→7
wrap_export[Sealed]Π(Sealed,
any)
do_read,file,file
file,file (High, do_close) 7→ wrap_export [Sealedfile,file ] any do_close



∗
′
I ⊢ h init m, [ ] | mainfile () at High −→A
h
,
π
|
E
file
π

init
∃st . st fileSP→✓
fileSP st

where the main function mainfile directly calls the untrusted code
mainfile ≜ λ _. gated_call(untrusted_main, ())
After applying Theorem 3 and establishing the initial context
Tinit ≜ g2l file ◁ mutexmapfile
one can use T-wrap-export together with the typing rules for the wrappers to type the exposed
functions. Tinit is used by T-sealed-import and T-sealed-export. Then it is only necessary toshow the following:
mainfile ◁fileSP,Afile fn [ ] → any

do_read ◁fileSP,Afile fn Sealedfile,file → Π(Sealedfile,file , any)

do_open ◁fileSP,Afile fn int → Sealedfile,filedo_close ◁fileSP,Afile fn Sealedfile,file → any

The type of mainfile follows from T-gated-call; the others are easy to show by first replacing
Sealedfile,file with file using T-sealed and then using the typing rules in Figure 12.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:23

7 MODEL OF THE TYPE SYSTEM
This section describes the model of the type system that we use to prove the rules from the previous
sections sound. The idea of using such a semantic type system and the model itself are heavily
inspired by RustBelt [Jung et al. 2018a], which was in turn inspired by prior work on Foundational
Proof-Carrying Code [Ahmed et al. 2010]. However, our model is significantly simpler since we do
not deal with Rust-specific features like lifetimes or borrowing.
As in Jung et al. [2018a], types are predicates on values in a separation logic based on Iris
[Jung et al. 2018b], a framework for building higher-order concurrent separation logics in Coq. We
instantiate Iris with λ sandbox to attain the program logic Irissandbox . Like the type system, Irissandbox
and thus also the type of its propositions iPropSP,A
are parameterized by a system call policy SP
sandboxand system call assumptions A.
. We write v ◁SP,A τ forDefinition 4. A type τ is a predicate Jτ KSP,A ∈ SurfaceVal → iPropSP,A
sandbox
SP,A
9
Jτ K
v.
Defining types as predicates in Iris makes the type system affine since Iris is an affine separation
logic, which means that it enjoys the weakening rule P ∗ Q ⇒ P [Jung et al. 2018b] used to show
T-weaken in Figure 10. Iris and thus Irissandbox provide an extensible notion of ghost state, which
can be used in the definition of types. For example, ghost state is useful to define the file type from
Section 2, as we will see later. Here, we will not explain exactly how ghost state is modeled, butrather refer interested readers to the paper of Jung et al. [2018b] for the details.
As usual in an affine setting, some typing rules given in earlier sections involved the notion of
copyability. Recall from Section 4 that a type τ is copyable if v ◁ τ is freely duplicable. In the model
this is realized by defining a type τ as copyable if v ◁ τ is persistent (in Iris lingo), which means it
does not express exclusive ownership of resources and thus can be freely duplicated.
The semantic interpretation of a typing context JT K is defined as the separating conjunction of
all v ◁ τ in T . The definition of the typing judgment for expressions is based on Iris Hoare triples.
Definition 5. The typing judgment for an expression e is defined as follows:
T1 ⊨pSP,A e : τ | T2≜

{JT1 KSP,A } e at p {v at p. v ◁SP,A τ ∗ JT2 KSP,A }?

The Hoare triple asserts that e is safe to run at privilege p if JT1 K holds. If the execution of eterminates in a value v, the privilege will be p, v will have type τ , and JT2 K will hold. The ? in
Definition 5 signifies that e is allowed to get stuck. Safe to run means that e upholds all invariants.
In particular, upholding the system call policy SP is an invariant of Irissandbox , which means that nowell-typed expression can violate SP. This is the main ingredient for the proof of Theorem 3. These
definitions are already enough to show the typing rules in Figure 10 sound.
The definitions of any and int are straightforward as they are defined to be inhabited by all
surface values and all integers, respectively:
JanyK ≜ λ v. True

JintK ≜ λ v. ∃z : Z. v = z

As motivated in Section 4, products are stored on the high heap. As usual in separation logic,
Irissandbox expresses ownership on the heap using the points-to-predicate l 7→ v, which asserts thatl points to the consecutive values v. This predicate allows the trusted code to keep invariants on
the heap, which are upheld when executing the untrusted code inside the sandbox. However, inIrissandbox , l 7→ v is only defined for high locations l. Thus, it is not possible to have invariants on
9v ◁ SP, A τ for values that are not surface values is defined as False.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:24

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

the low heap, which is necessary to fulfill assumption (1) of Theorem 2. Using this predicate, Π(τ )is defined as follows:JΠ(τ )K ≜ λ v. ∃l . v = l ∗ ∃vp . l 7→ vp ∗ vp ◁ τ ∗ DeallocSize(l, |τ |)The proposition DeallocSize(l, |τ |) is the same as in Jung et al. [2018a]; it manages the right todeallocate the location l.
The type of functions fn τa → τr is defined in the same way as in Jung et al. [2018a] and closely
follows T-fn in Figure 11:10
Jfn τa → τr K ≜ λ v. □ ∃f xe. v = (rec f (x) = e) ∗ ∀va . va ◁ τa ⊨High e[v/f , va /x] : τr | ∅The modality □ ensures that only persistent resources are used in the proof of v ◁ fn τa → τr ,which is necessary to show T-fn-copy. The Coq formalization [Sammler et al. 2019] shows how
the typing rules in Figure 11 can be proven sound using these definitions.
As T-low-ptr already suggests, LowPtr is defined as all low locations:
JLowPtrK ≜ λ v. ∃l . v = l ∗ l = (Low, _, _)The soundness of the typing rules in Figure 15 follows from the fact that low locations cannot be
owned and getting stuck is safe.
Typing of system calls. As the concluding part of our tour of the model of the type system, welook at how one can prove typing rules for system calls like T-print and the file-related typing
rules in Figure 12. As mentioned in Section 4, there is no generic typing rule for system calls; rather,
one proves typing rules for specific system calls by reasoning in the model.
Showing that a system call is safe to execute reduces to a proof that the automaton of the systemcall policy can make the corresponding step for the supplied arguments. In the case of T-print, forexample, this is easy because one knows that v is a value less than 1000, which is always safe topass to unsafe_print.
In contrast, safety of an execution of read or close depends on the state of the system call policy.
The typing rules T-file-read and T-file-close rely on the file type, which represents an open
file. But how to define such a type in the model? The solution to this problem is to extend thespecification of each system call policy SP with an invariant on the state of SP:
SP,A
I SP : S SP → iPropsandbox

Using I SP , it is possible to show the following simplified proof rule for system calls:11
P-syscallP(s, qa , Φ) ≜ ∀qr , st . I SP st ⇛ ∃st ′ . st(s,q a ,q r )✓→ S P st ′ ∗ I SP st ′ ∗ Φ qr

{P(s, qa , Φ)} syscall(s, qa ) at High {qr at High. Φ qr }?
This rule states that a system call s with argument qa is safe to execute if, assuming I SP holds forthe current state st of the system call policy, SP accepts s for all return values qr by stepping to a
new state st ′ , ⊥ and I SP holds for the new state st ′.
The state of fileSP is the finite set of open file handles st ∈ P(Z). To define I fileSP and the file
type, we use two new kinds of ghost state called file_auth st and file_token z f , which are governed
10 For purposes of presentation, we suppress the ▷ modality, which is necessary to prove T-fn for recursive functions.
11 To a first approximation, readers unfamiliar with Iris can read the view shift ⇛ as if it were the magic wand −∗.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:25

by the following rules:12
P-file-open

z f < stP-file-in

file_auth st ⇛ file_auth (st ∪ {z f }) ∗ file_token z f

file_auth st ∗ file_token z f −∗ z f ∈ st

P-file-close

file_auth st ∗ file_token z f ⇛ file_auth (st \ {z f })Conceptually, file_auth st asserts that the set of open files is currently st and file_token z f statesthat z f is in this set (as P-file-in shows) and thus represents an open file. To close a file, whichmeans removing it from st, one has to provide the corresponding file_token z f , as can be seen in
P-file-close. I fileSP maintains file_auth st, and file is defined using file_token z f :I fileSP ≜ λ st . file_auth st

JfileK ≜ λ v. ∃z f . v = z f ∗ file_token z f

With these definitions we have everything in place to prove T-file-read and T-file-close. For
T-file-read, after unfolding the definition of the typing judgment and applying P-syscall, one
combines file_token z f from v ◁ file with file_auth st from I fileSP to learn that the argument z f toread is in the open state and thus fileSP can make a step. The proof of T-file-close is almost thesame except that close removes z f from the set of open files and thus one must use P-file-close to
update file_auth st to file_auth (st \ {z f }). This consumes file_token z f , which is the reason why
T-file-close consumes v ◁ file.
Unfortunately, the simplified version of P-syscall stated above is not quite strong enough toprove T-file-open. To use P-file-open we must show that z f is not already an open file. Otherwise
we could use P-file-open to generate arbitrarily many file_token z f and use them to close thesame file handle multiple times. Thus, we need to assume that the open system call returns fresh
file handles using the system call assumptions Afile defined in Section 3. However, as stated above,
P-syscall does not make use of Afile , and thus to prove T-file-open we will need a stronger versionof P-syscall.
Before giving the stronger P-syscall-full rule, we first need to introduce two new kinds ofghost state for reasoning about the trace:• full_trace π asserts that the current trace of the execution so far is π . It also contains thepermission to extend the trace and thus cannot be duplicated.
• in_trace i o states that the observation at index i of the current trace is o. Since the trace isappend-only, in_trace i o is a persistent assertion, which can be freely duplicated.
The important property of full_trace π and in_trace i o is that they can be combined to learn πi = o.
P-in-trace

full_trace π ∗ in_trace i o −∗ πi = o

Next, we need to update I fileSP so that it records that we have seen an open system call for all
files that are currently open.
I fileSP ≜ λ st . file_auth st ∗ ∃i. (∀i ∈ i. ∃o. in_trace i o) ∗ ∀z f ∈ st . ∃i ∈ i. in_trace i (open, _, z f )In this extended version, I fileSP explicitly keeps track of a list i of valid indices into the trace, andensures that for any currently open file handle z f , there exists some index i ∈ i such that theobservation at that index in the trace witnesses the call to open that produced z f .
12 The definition of file_auth st and file_token z

fand the proofs of their rules can be found in the Coq development[Sammler et al. 2019].
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:26

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

Now we can generalize the proof rule for syscall to its final form, which allows us to use thesystem call assumptions A.13
P-syscall-full∀qr st π . I SP st −∗∃i. (∀i ∈ i. ∃o. in_trace i o) ∗P(s, qa , Φ) ≜∀ i new > max(i). in_trace i new (s, qa , qr ) −∗ full_trace π −∗ A π ⇛(s,q a ,q r )✓′′∃st ′ . st →SP st ∗ I SP st ∗ full_trace π ∗ Φ q r{P(s, qa , Φ)} syscall(s, qa ) at High {qr at High.Φ qr }?
Let’s walk through this rule: After applying P-syscall-full, one learns that the system callinvariant holds for the current state (I SP st). Then one has to provide a list of indices i which haveoccurred in the trace (∀i ∈ i. ∃o. in_trace i o). In the proof for T-file-open this is instantiated withi from I fileSP .
Afterwards one receives an index i new which is greater than all indices in i (which implies
i new < i), and one knows that this index is now in the trace with the data of the current systemcall (in_trace i new (s, qa , qr )). Furthermore, one gets the full_trace π predicate and learns that thesystem call assumptions A hold for the current trace π . The rest is the same as P-syscall except that
one has to return ownership of full_trace π for it to be available again when using P-syscall-full
the next time.
The proof for T-file-open uses the information from P-syscall-full in combination with theupdated I fileSP and Afile to conclude that the file handle z f returned by open is not in st. Then
P-file-open is used to create file_token z f Ðwhich is used to establish the JfileK corresponding to
the file returned by T-file-openÐand the in_trace i (s, qa , qr ) provided by P-syscall-full is used
to re-establish I fileSP .
8 RELATED WORKIn Section 1, we already discussed related work on robust safety and sandboxing. In this section,
we revisit related work on robust safety for a more technical comparison, and then discuss otherrelated areas of research.
Robust safety. As mentioned in the introduction, many prior type systems and program logics
enforce robust safety [Fournet et al. 2007; Bugliesi et al. 2011; Gordon and Jeffrey 2001; Swasey et al.
2017], but in abstract memory models where the untrusted code cannot guess locations that are notexplicitly given to it. In contrast, we work with a low-level memory model where untrusted code
can cast an integer to a pointer and dereference it. Sandboxing becomes relevant in this setting.
Another difference from prior work is the type at which the untrusted code is allowed to interact
with verified code. In prior work, this type, called Un [Fournet et al. 2007; Bugliesi et al. 2011;
Gordon and Jeffrey 2001] or Low [Swasey et al. 2017], includes only those values to which it is safe
for untrusted code to have access, i.e., values from which it should not be possible to obtain accessto a (high-privilege) location that trusted code has placed invariants on. This Un/Low type has
a fairly complex semantic interpretation because it is not obvious from looking solely at a value
whether or not one can use it to gain access to a high-privilege location. In contrast, in our setting,owing to physical memory isolation, the trusted and untrusted code can pass arbitrary surface
values back and forth, and hence the analogue of the type Un/Low in our setting is simply theuniversal type, any.
Further differences arise in how safety properties are modeled. In our setting, we define safety
properties in terms of traces of system calls. Prior approaches have used various different setups
13 Here the maximum of the empty list is defined as -1.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:27

that fit their specific settings best. For example, Fournet et al. [2007] define safety in terms of setsof prior events, while Swasey et al. [2017] define safety as non-failure of inlined assertions.
Automatic enforcement of types. Enforcing types at the boundary of strongly typed and lessstrongly typed (or untyped) code has been extensively studied in the literature on decidable higherorder contracts [Findler and Felleisen 2002; Blume and McAllester 2004]. Contracts have even been
examined for the interaction between substructural and standard types [Tov and Pucella 2010].
While inspired by such work, our wrappers go one step further as they not only check values, butalso transform them. This allows us to implement and verify dynamic sealing in our framework,whereas it is built into the operational semantics of Tov and Pucella [2010]. Also, owing to our
setting involving low-level untrusted code, the requirements on our wrappers are different ś someof our wrappers also translate between different representations, e.g., the wrapper for Π(τ ).
Gradual typing. Interaction between typed and untyped code has also been studied in theliterature on gradual typing [Siek and Taha 2006; Wadler and Findler 2009; Igarashi et al. 2017;
Lehmann and Tanter 2017; New and Ahmed 2018]. In gradual typing, some parts of a program
contain type annotations that are statically checked by the type checker, whereas other parts are
not statically type-checked and, in those parts, types are enforced at run time. A value passed
from an untyped part to a typed part is dynamically cast to the expected type. At a high level, ourwrappers can be viewed as a replacement for such casts. However, the casts in gradual typing areusually expected to fulfill certain properties like restoration of the original value after it is passed in
one direction and then back [New and Ahmed 2018]. We explicitly do not want this cancellativity
property between import and export since it would disallow useful wrappers like Sealeds,τ whereimporting a seal created by export might fail (by design) if the seal was already used. A further
difference is that our wrappers copy values between low and high heaps, which is not requiredin conventional gradual typing. Moreover, our types are semantically defined and thus extensible.
Consequently, the set of wrappers (casts) is also extensible.
Linear capabilities for fully abstract compilation of separation-logic-verified code. In concurrent
work, Van Strydonck et al. [2019] provide a fully abstract compiler from a language with separation
logic specifications on untrusted functions to a capability machine with linear capabilities. The
compiler inserts checks around the untrusted functions that fulfill a role similar to our wrappers.
However, the implementations of these checks differ a great deal from our wrappers due to thedifferent isolation techniques used (fine-grained linear capabilities in their work vs. coarse-grained
memory isolation in ours). Besides, since Van Strydonck et al. [2019] prove full abstraction, their
checks need to be both correct (i.e., programs distinguishable in the source language must be distinguishable in the target language after compilation) and secure (i.e., programs whose compilations
are distinguishable in the target language must be distinguishable in the source language). The
well-typedness requirement for our wrappers corresponds to the security direction. However, we
do not require correctness, as this would rule out wrappers like dynamic sealing.
Formalizing the security guarantees of compartmentalizing compilation. There is existing workon formal, high-level properties of compartmentalization in the context of compilation. Juglaret
et al. [2016] and Abate et al. [2018] investigate how a compiler can transfer properties of a compartmentalized source language application to the target language. While this work also relies on thenotion of robust properties (at least superficially), it is actually complementary. Our paper focuses
on establishing robust properties of the source application, whereas this line of work could be used
to transfer those properties to the compiled program. Properly aligning our work and existing work
to compose nicely in this way remains an open avenue for future research.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:28A

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

OPERATIONAL SEMANTICS OF λ sandbox

This appendix contains the complete operational semantics of λ sandbox .
finh ∈ Heap ≜ Loc −⇀ Valo ∈ Observation ≜ (Name, Lit, Lit) π ∈ Trace ≜ list Observationfin

I ∈ Interface ≜ (Priv, Name) −⇀ Val A ∈ SyscallAssumptions ≜ Trace → Prop
Like in λ Rust [Jung et al. 2018a], in λ sandbox two locations where at least one is not allocated canboth compare as equal and as unequal.
h ⊢ q1 = q2, h ⊢ q1 , q2
h ⊢l =ll 1 < dom(h) ∨ l 2 < dom(h)z1 , z2

l1 , l2h ⊢ l1 = l2h ⊢ z1 , z2h ⊢ l1 , l2h⊢z =zp1 ⊑ p2p ⊑p

Low ⊑ HighIn the rules for the operational semantics, h[l ← v] denotes the heap h with l updated to v, andh[l ← ⊥] is the heap h with the entry at location l deleted. The notation l + z denotes the location
l with the offset shifted by z.
I ⊢ h, π | e at p → h ′, π ′ | e 1′ at p1′ , (e 2′ at p2′ )?
O-add

O-sub

z1 + z2 = z ′z1 − z2 = z ′I ⊢ h, π | z 1 + z 2 at p →A h, π | z ′ at p

I ⊢ h, π | z 1 − z 2 at p →A h, π | z ′ at p

O-le-trueO-le-false

z1 ≤ z2

z1 > z2I ⊢ h, π | z 1 ≤ z 2 at p →A h, π | 1 at p

I ⊢ h, π | z 1 ≤ z 2 at p →A h, π | 0 at p

O-eq-trueO-eq-falseh ⊢ q1 = q2

h ⊢ q1 , q2

I ⊢ h, π | q 1 = q 2 at p →A h, π | 1 at p

I ⊢ h, π | q 1 = q 2 at p →A h, π | 0 at p

O-offsetl′ = l + z

I ⊢ h, π | l .z at p →A h, π | l ′ at p
O-app

I ⊢ h, π | (rec f (x) = e)(v) at p →A h, π | e[rec f (x) = e/f , v/x] at p
O-writeO-readh(l) = v ′h(l) = v
I ⊢ h, π | !l at p →A h, π | v at p
O-allocz>0

l = (p ′, zb , zo )l = (p ′, zb , zo )p′ ⊑ pI ⊢ h, π | l ← v at p →A h[l ← v], π | h at p{(p ′, zb )} × Z # dom(h)p′ ⊑ pI ⊢ h, π | allocp ′ (z) at p →A h[l + m ← h | 0 ≤ m < z], π | l at p
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:29

O-freel = (p ′, zb , zo )z>0dom(h) ∩ {(p ′, zb )} × Z = {(p ′, zb )} × {m|zo ≤ m < zo + z}

p′ ⊑ pI ⊢ h, π | free(z, l) at p →A h[l + m ← ⊥ | 0 ≤ m < z], π | h at p
O-cas-failh(l) = q ′h ⊢ q′ , ql = (p ′, zb , zo )p′ ⊑ pI ⊢ h, π | CAS(l, q, v) at p →A h, π | 0 at p
O-cas-such(l) = q ′h ⊢ q′ = q

l = (p ′, zb , zo )p′ ⊑ pI ⊢ h, π | CAS(l, q, v) at p →A h[l ← v], π | 1 at p
O-caseO-forkI ⊢ h, π | case z of e at p →A h, π | ez at p

I ⊢ h, π | fork e at p →A h, π | h at p, e at p

O-syscallHigh ⊑ p

A (π ++ [(s, qa , qr )])I ⊢ h, π | syscall(s, qa ) at p →A h, π ++ [(s, qa , qr )] | qr at p
O-gated-callp = High ⇔ p ′ = Low

I((p ′, s)) = v

I ⊢ h, π | gated_call(s, v) at p →A h, π | gated_ret(v (v)) at p ′O-gated-ret

p = High ⇔ p ′ = Low

I ⊢ h, π | gated_ret(v) at p →A h, π | v at p ′O-mk-locationp ′ = Low ⇔ zp = 0

zb ≥ 0l = (p ′, zb , zo )I ⊢ h, π | mk_location(zp , zb , zo ) at p →A h, π | l at p
O-get-priv

l = (p ′, zb , zo )p ′ = Low ⇒ zp = 0

p ′ = High ⇒ zp = 1

I ⊢ h, π | get_priv(l) at p →A h, π | zp at p
O-get-blockl = (p ′, zb , zo )I ⊢ h, π | get_block(l) at p →A h, π | zb at p
O-get-offset

l = (p ′, zb , zo )I ⊢ h, π | get_offset(l) at p →A h, π | zo at p

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:30Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

I ⊢ h, π | E −→A h ′, π ′ | E ′O-ThreadI ⊢ h, π | e at p →A h ′, π ′ | e 1′ at p1′ , (e 2′ at p2′ )?

I ⊢ h, π | E ++ [K[e] at p] ++ E ′ −→A h ′, π ′ | E ++ [K[e 1′ ] at p1′ ] ++ E ′ ++ [e 2′ at p2′ ]ACKNOWLEDGMENTS
We wish to thank David Swasey and Ralf Jung for their feedback and helpful discussions. This
research was supported in part by a European Research Council (ERC) Consolidator Grant for the
project łRustBeltž, funded under the European Union’s Horizon 2020 Framework Programme (grant
agreement no. 683289) and by the German Science Foundation (DFG) through the Collaborative
Research Center łMethods and Tools for Understanding and Controlling Privacyž (SFB 1223).
REFERENCES
Martín Abadi. 1997. Secrecy by typing in security protocols. In Theoretical Aspects of Computer Software, Third International
Symposium, TACS ’97, Sendai, Japan, September 23-26, 1997, Proceedings (Lecture Notes in Computer Science), Martín Abadi
and Takayasu Ito (Eds.), Vol. 1281. Springer, 611ś638. https://doi.org/10.1007/BFb0014571
Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo
Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. 2018. When good components go bad: Formallysecure compilation despite dynamic compromise. In Proceedings of the 2018 ACM SIGSAC Conference on Computer andCommunications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018. 1351ś1368. https://doi.org/10.1145/3243734.
3243745
R.P. Abbott, J. S. Chin, J. E. Donnelley, W. L. Konigsford, S. Tokubo, and D. A. Webb. 1976. Security analysis and enhancementsof computer operating systems. Technical Report. Institute for Computer Sciences and Technology, National Bureau ofStandards, Washington,D.C. https://nvlpubs.nist.gov/nistpubs/Legacy/IR/nbsir76-1041.pdf
Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, and Daniel C. Wang. 2010. Semantic
foundations for typed assembly languages. ACM Trans. Program. Lang. Syst. 32, 3 (2010), 7:1ś7:67. https://doi.org/10.
1145/1709093.1709094
ARM Limited. 2009. ARM Security Technology. Technical Report. http://infocenter.arm.com/help/topic/com.arm.doc.prd29genc-009492c/PRD29-GENC-009492C_trustzone_security_whitepaper.pdf
David A. Basin, Vincent Jugé, Felix Klaedtke, and Eugen Zalinescu. 2013. Enforceable security policies revisited. ACM Trans.
Inf. Syst. Secur. 16, 1 (2013), 3:1ś3:26. https://doi.org/10.1145/2487222.2487225
Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, and Pierre Wilke. 2019. Compiling sandboxes: Formallyverified software fault isolation. In Programming Languages and Systems - 28th European Symposium on Programming,
ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech
Republic, April 6-11, 2019, Proceedings. 499ś524. https://doi.org/10.1007/978-3-030-17184-1_18
Matthias Blume and David A. McAllester. 2004. A sound (and complete) model of contracts. In Proceedings of the NinthACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21,
2004, Chris Okasaki and Kathleen Fisher (Eds.). ACM, 189ś200. https://doi.org/10.1145/1016850.1016876
Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2011. Resource-aware authorization policies forstatically typed cryptographic protocols. In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF
2011, Cernay-la-Ville, France, 27-29 June, 2011. IEEE Computer Society, 83ś98. https://doi.org/10.1109/CSF.2011.13
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky,
and Andrew Tolmach. 2015. Micro-policies: Formally verified, tag-based security monitors. In 2015 IEEE Symposium on
Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015. IEEE Computer Society, 813ś830. https://doi.org/10.
1109/SP.2015.55
Arthur Azevedo de Amorim, Catalin Hritcu, and Benjamin C. Pierce. 2018. The meaning of memory safety. In Principles of
Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory andPractice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science),
Lujo Bauer and Ralf Küsters (Eds.), Vol. 10804. Springer, 79ś105. https://doi.org/10.1007/978-3-319-89722-6_4
Akram El-Korashy. 2016. A Formal Model for Capability Machines: An Illustrative Case Study towards Secure Compilation to
CHERI. Master’s thesis. Universität des Saarlandes. http://hdl.handle.net/11858/00-001M-0000-002C-41CA-B
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

The High-Level Benefits of Low-Level Sandboxing

32:31

Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In Proceedings of the Seventh ACM
SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002.,
Mitchell Wand and Simon L. Peyton Jones (Eds.). ACM, 48ś59. https://doi.org/10.1145/581478.581484
Cormac Flanagan. 2006. Hybrid type checking. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett andSimon L. Peyton Jones (Eds.). ACM, 245ś256. https://doi.org/10.1145/1111037.1111059
Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2007. A type discipline for authorization policies. ACM Trans.
Program. Lang. Syst. 29, 5 (2007), 25. https://doi.org/10.1145/1275497.1275500
Timothy S. Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN’91 Conference
on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, David S. Wise
(Ed.). ACM, 268ś277. https://doi.org/10.1145/113445.113468
Google. 2019. Sandboxed Api. https://github.com/google/sandboxed-api.
Andrew D. Gordon and Alan Jeffrey. 2001. Authenticity by typing for security protocols. In 14th IEEE Computer Security
Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada. 145ś159. https://doi.org/10.
1109/CSFW.2001.930143
Orna Grumberg and David E. Long. 1994. Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16, 3(1994), 843ś871. https://doi.org/10.1145/177492.177725
Norman Hardy. 1988. The confused deputy (or why capabilities might have been invented). Operating Systems Review 22, 4(1988), 36ś38. https://doi.org/10.1145/54289.871709
Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On polymorphic gradual typing. PACMPL 1, ICFP (2017), 40:1ś40:29.
https://doi.org/10.1145/3110284
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. 2016. Beyond good and evil:
Formalizing the security guarantees of compartmentalizing compilation. In IEEE 29th Computer Security Foundations
Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016. 45ś60. https://doi.org/10.1109/CSF.2016.11
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018a. Rustbelt: Securing the foundations of theRust programming language. PACMPL 2, POPL (2018), 66:1ś66:34. https://doi.org/10.1145/3158154
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018b. Iris from theground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20.
https://doi.org/10.1017/S0956796818000151
Koen Koning, Xi Chen, Herbert Bos, Cristiano Giuffrida, and Elias Athanasopoulos. 2017. No need to hide: Protecting
safe regions on commodity hardware. In Proceedings of the Twelfth European Conference on Computer Systems, EuroSys
2017, Belgrade, Serbia, April 23-26, 2017, Gustavo Alonso, Ricardo Bianchini, and Marko Vukolic (Eds.). ACM, 437ś452.
https://doi.org/10.1145/3064176.3064217
Benjamin Lamowski, Carsten Weinhold, Adam Lackorzynski, and Hermann Härtig. 2017. Sandcrust: Automatic sandboxingof unsafe components in Rust. In Proceedings of the 9th Workshop on Programming Languages and Operating Systems,
Shanghai, China, October 28, 2017, Julia Lawall (Ed.). ACM, 51ś57. https://doi.org/10.1145/3144555.3144562
Nico Lehmann and Éric Tanter. 2017. Gradual refinement types. In Proceedings of the 44th ACM SIGPLAN Symposium on
Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 775ś788. http://dl.acm.org/citation.
cfm?id=3009856
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert Memory Model, Version 2.
Research report RR-7987. INRIA. http://hal.inria.fr/hal-00703441
James Litton, Anjo Vahldiek-Oberwagner, Eslam Elnikety, Deepak Garg, Bobby Bhattacharjee, and Peter Druschel. 2016.
Light-weight contexts: An OS abstraction for safety and performance. In 12th USENIX Symposium on Operating Systems
Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016., Kimberly Keeton and Timothy Roscoe(Eds.). USENIX Association, 49ś64. https://www.usenix.org/conference/osdi16/technical-sessions/presentation/littonFrank McKeen, Ilya Alexandrovich, Alex Berenzon, Carlos V. Rozas, Hisham Shafi, Vedvyas Shanbhogue, and Uday R.
Savagaonkar. 2013. Innovative instructions and software model for isolated execution. In HASP 2013, The Second Workshop
on Hardware and Architectural Support for Security and Privacy, Tel-Aviv, Israel, June 23-24, 2013, Ruby B. Lee and Weidong
Shi (Eds.). ACM, 10. https://doi.org/10.1145/2487726.2488368
James H. Morris, Jr. 1973. Protection in programming languages. Commun. ACM 16, 1 (1973), 15ś21. https://doi.org/10.
1145/361932.361937
Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, and Edward Gan. 2012. Rocksalt: Better, faster, stronger
SFI for the x86. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing,
China - June 11 - 16, 2012. 395ś404. https://doi.org/10.1145/2254064.2254111
Mozilla. 2019. Script security. Technical Report. https://developer.mozilla.org/en-US/docs/Mozilla/Gecko/Script_security
Max S. New and Amal Ahmed. 2018. Graduality from embedding-projection pairs. PACMPL 2, ICFP (2018), 73:1ś73:30.
https://doi.org/10.1145/3236768
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.

32:32

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak. 2019. The high-level benefits of low-level sandboxing ś
Artifact. https://doi.org/10.5281/zenodo.3533037 Latest version: https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq.
Fred B. Schneider. 2000. Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 1 (2000), 30ś50. https://doi.org/10.
1145/353323.353382
Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming
Workshop, Vol. 6. 81ś92.
David Swasey, Deepak Garg, and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns.
PACMPL 1, OOPSLA (2017), 89:1ś89:26. https://doi.org/10.1145/3133913
The Rust Developers. 2019. The Rust programming language. https://rust-lang.org.
Jesse A. Tov and Riccardo Pucella. 2010. Stateful contracts for affine types. In Programming Languages and Systems, 19th
European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practiceof Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (Lecture Notes in Computer Science), Andrew D.
Gordon (Ed.), Vol. 6012. Springer, 550ś569. https://doi.org/10.1007/978-3-642-11957-6_29
Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno O. Duarte, Michael Sammler, Peter Druschel, and Deepak Garg. 2019.
ERIM: Secure, efficient in-process isolation with protection keys (MPK). In 28th USENIX Security Symposium, USENIX
Security 2019, Santa Clara, CA, USA, August 14-16, 2019, Nadia Heninger and Patrick Traynor (Eds.). USENIX Association,
1221ś1238. https://www.usenix.org/conference/usenixsecurity19/presentation/vahldiek-oberwagner
Thomas Van Strydonck, Frank Piessens, and Dominique Devriese. 2019. Linear capabilities for fully abstract compilation of
separation-logic-verified code. Proc. ACM Program. Lang. 3, ICFP, Article 84 (July 2019), 29 pages. https://doi.org/10.
1145/3341688
Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can’t be blamed. In Programming Languages and Systems,
18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practiceof Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. 1ś16. https://doi.org/10.1007/978-3-642-00590-9_1
Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In Proceedings of the ACM
SIGPLAN ’98 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998,
Jack W. Davidson, Keith D. Cooper, and A. Michael Berman (Eds.). ACM, 249ś257. https://doi.org/10.1145/277650.277732
Bennet Yee, David Sehr, Gregory Dardyk, J. Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, andNicholas Fullagar. 2009. Native Client: A sandbox for portable, untrusted x86 native code. In 30th IEEE Symposium
on Security and Privacy (S&P 2009), 17-20 May 2009, Oakland, California, USA. IEEE Computer Society, 79ś93. https://doi.org/10.1109/SP.2009.25

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 32. Publication date: January 2020.