# Isolation Without Taxation

Near-Zero-Cost Transitions for WebAssembly and SFI

Matthew Kolosick  UC San DiegoUSA<EMAIL_ADDRESS>,  Shravan Narayan
UC San DiegoUSA<EMAIL_ADDRESS>,  Evan Johnson  UC San DiegoUSA
<EMAIL_ADDRESS>,  Conrad Watt  University of CambridgeUK
<EMAIL_ADDRESS>,  Michael LeMay  0000-0001-6206-9642 Intel LabsUSA
<EMAIL_ADDRESS>,  Deepak Garg  Max Planck Institute for Software
SystemsGermany<EMAIL_ADDRESS>,  Ranjit Jhala  UC San DiegoUSA
<EMAIL_ADDRESS>and  Deian Stefan  UC San DiegoUSA<EMAIL_ADDRESS>
(2022)

###### Abstract.

Software sandboxing or software-based fault isolation (SFI) is a lightweight
approach to building secure systems out of untrusted components. Mozilla, for
example, uses SFI to harden the Firefox browser by sandboxing third-party
libraries, and companies like Fastly and Cloudflare use SFI to safely co-
locate untrusted tenants on their edge clouds. While there have been
significant efforts to optimize and verify SFI enforcement, context switching
in SFI systems remains largely unexplored: almost all SFI systems use
_heavyweight transitions_ that are not only error-prone but incur significant
performance overhead from saving, clearing, and restoring registers when
context switching. We identify a set of _zero-cost conditions_ that
characterize when sandboxed code has sufficient structured to guarantee
security via lightweight _zero-cost_ transitions (simple function calls). We
modify the Lucet Wasm compiler and its runtime to use zero-cost transitions,
eliminating the undue performance tax on systems that rely on Lucet for
sandboxing (e.g., we speed up image and font rendering in Firefox by up to
29.7% and 10% respectively). To remove the Lucet compiler and its correct
implementation of the Wasm specification from the trusted computing base, we
(1) develop a _static binary verifier_ , VeriZero, which (in seconds) checks
that binaries produced by Lucet satisfy our zero-cost conditions, and (2)
prove the soundness of VeriZero by developing a logical relation that captures
when a compiled Wasm function is semantically well-behaved with respect to our
zero-cost conditions. Finally, we show that our model is useful beyond Wasm by
describing a new, purpose-built SFI system, SegmentZero32, that uses x86
segmentation and LLVM with mostly off-the-shelf passes to enforce our zero-
cost conditions; our prototype performs on-par with the state-of-the-art
Native Client SFI system.

software fault isolation, sandboxing, WebAssembly, verification

††copyright: rightsretained††journal: PACMPL††journalyear:
2022††journalvolume: 6††journalnumber: POPL††article: 27††publicationmonth:
1††doi: 10.1145/3498688††ccs: Security and privacy Formal security
models††ccs: Security and privacy Systems security

##  1\. Introduction

Memory safety bugs are the single largest source of critical vulnerabilities
in modern software. Recent studies found that roughly 70% of all critical
vulnerabilities were caused by memory safety bugs (Miller, 2019; Chromium
Team, 2020) and that malicious attackers are exploiting these bugs before they
can be patched (Google Project Zero, 2021; Metrick et al., 2020). Software
sandboxing— or software-based fault isolation (SFI)— promises to reduce the
impact of such memory safety bugs (Tan et al., 2017; Wahbe et al., 1993). SFI
toolkits like Native Client (NaCl) (Yee et al., 2009) and WebAssembly (Wasm)
allow developers to restrict untrusted components to their own _sandboxed_
regions of memory thereby isolating the damage that can be caused by bugs in
these components. Mozilla, for example, uses Wasm to sandbox third-party C
libraries in Firefox (Narayan et al., 2020; Froyd, 2020); SFI allows the
browser to use libraries like libgraphite (font rendering), libexpat (XML
parsing), libsoundtouch (audio processing), and hunspell (spell checking)
without risking whole-browser compromise due to library vulnerabilities.
Others have used SFI to isolate code in OS kernels (Erlingsson et al., 2006;
Castro et al., 2009; Herder et al., 2009; Seltzer et al., 1996), databases
(Ford and Cox, 2008; Ford, 2005; Wahbe et al., 1993), browsers (Lucco et al.,
1995; Yee et al., 2009; Haas et al., 2017), language runtimes (Siefers et al.,
2010; Niu and Tan, 2014), and serverless clouds (McMullen, 2020; Varda, 2018;
Gadepalli et al., 2020).

SFI toolkits enforce memory isolation by placing untrusted code into a
sandboxed environment within which every memory access is dynamically checked
to be safe. For example, NaCl and Wasm toolkits (e.g., Lucet (Bytecode
Alliance, 2020a) and WAMR (Bytecode Alliance, 2020b)) instrument memory
accesses to ensure they are within the sandbox region and add runtime checks
to ensure that all control flow is confined to the sandboxed paths with
instrumented memory accesses. There is a large body of work that ensures the
runtime checks are _fast_ on different architectures, e.g., x86 (McCamant and
Morrisett, 2006; Yee et al., 2009; Ford and Cox, 2008; Payer and Gross, 2011),
x86-64 (Sehr et al., 2010), SPARC® (Adl-Tabatabai et al., 1996), and ARM®
(Zhao et al., 2011; Zhou et al., 2014; Sehr et al., 2010), as otherwise they
incur unacceptable overheads on the code executing in the sandbox. Similarly,
there is a considerable literature that establishes that the checks are
_correct_ (Morrisett et al., 2012; Kroll et al., 2014; Johnson et al., 2021;
Besson et al., 2018, 2019), as even a single missing check can let the
attacker escape the sandbox.

However, the security and overhead of software sandboxing also crucially
depends on the correctness and cost of context switching — the _trampolines_
and _springboards_ used to transition into and out of sandboxes. Almost all
SFI systems, from (Wahbe et al., 1993)’s original SFI implementation to recent
Wasm SFI toolkits (Bytecode Alliance, 2020a, b), use _heavyweight transitions_
for context switching.111The one exception is WasmBoxC (Zakai, 2020),
discussed in Section 9. These transitions (1) switch protection domains by
tying into the underlying memory isolation mechanism (e.g., by setting segment
registers (Yee et al., 2009), memory protection keys (Vahldiek-Oberwagner et
al., 2019; Hedayati et al., 2019), or sandbox context registers (Bytecode
Alliance, 2020a, b)), and (2) save, scrub, and restore machine state (e.g. the
stack pointer, program counter, and callee-save registers) across the
boundary. This code is complicated and hard to get right, as it has to account
for the particular quirks of different architectures and operating system
platforms (Alder et al., 2020). Consequently, bugs in transition code have led
to vulnerabilities in both NaCl and Wasm— from sandbox breakouts (Nacl Issue
1607, 2011; Nacl Issue 1633, 2011), to information leaks (Nacl Issue 775,
2010; Nacl Issue 2919, 2012), and application state corruption (Rydgard,
2020). Furthermore, in applications with high application-sandbox context
switching rates, the cost of transitions dominates the overall sandboxing
overhead. For example, heavyweight transitions prohibitively slowed down font
rendering in Firefox, preventing Mozilla from shipping a sandboxed libgraphite
(Narayan et al., 2020).

In this paper, we develop the principles and pragmatics needed to implement
SFI systems with near-zero-cost transitions, thereby realizing the three-
decade-old vision of reducing the cost of SFI context switches to (almost)
that of a function call. We do this via five contributions:

1\. Formal model of secure transitions (§3). Simply eliminating heavyweight
transitions is unsafe, potentially allowing an attacker to escape the SFI
sandbox. To understand this threat, our first contribution is the first
formal, declarative, and high-level model that elucidates the role of
transitions in making SFI secure. Intuitively, our model shows how secure
transitions protect the integrity and confidentiality of machine state across
the domain transition by providing _well-bracketed_ control flow, i.e.,
ensuring that returns actually return to their call sites.

2\. Zero-cost conditions for isolation (§4). Heavyweight transitions provide
security by wrapping cross-domain calls and returns to ensure that sandboxed
code cannot, for example, read secret registers or tamper with the stack
pointer. While this wrapping is necessary when sandboxing arbitrary code, our
insight is these wrappers can be made redundant when the code enjoys
additional structure, not dissimilar to the additional structure typically
imposed by most SFI systems to ensure memory isolation. For example, NaCl uses
_coarse-grained_ control-flow integrity (CFI) to restrict the sandbox’s
control flow to its own code region (Tan et al., 2017; Yee et al., 2009; Haas
et al., 2017).

We concretize this insight via our second contribution, a precise definition
of _zero-cost conditions_ that guarantee that sandboxed code can safely use
zero-cost transitions. In particular, we show that transitions can be
eliminated when sandboxed code follows a _type-directed_ CFI discipline, has
well-bracketed control flow, enforces local state (stack and register)
encapsulation, and ensures registers and stack slots are initialized before
use. Our notion of zero-cost conditions is inspired, in part, by techniques
that use type- and memory-safe languages to isolate code via language-level
enforcement of well-bracketed control flow and local state encapsulation
(Maffeis et al., 2010; Mettler et al., 2010; Grimmer et al., 2015; Miller et
al., 2008; Hunt and Larus, 2007; Morrisett et al., 1999a). However, instead of
requiring developers to rewrite millions of lines of code in high-level
languages (Tan et al., 2017), our zero-cost conditions distill the semantic
guarantees provided by high-level languages to allow retrofitting zero-cost
transitions in the SFI setting. In other part, our work is inspired by Besson
et al. (2018), who define a defensive semantics for SFI that captures a notion
of sandboxing via simple function calls with a stack shared between the
sandbox and host application. Our work builds on this work by addressing two
shortcomings: First, their definition does not account for confidentiality of
application data, and implementations based on their system would thus need
heavyweight transitions to prevent such attacks. Second, their defensive
semantics makes fundamental use of guard zones, which limits the flexibility
of the framework. Our definitions of zero-cost transitions have no such
limitations and fully realize their goal of defining flexible, secure SFI with
zero-cost transitions between application and sandbox.

3\. Instantiating the zero-cost model (§5). We demonstrate the retrofitting of
zero-cost transitions via our third contribution, an instantiation of our
zero-cost model to two SFI systems: Wasm and SegmentZero32. Previous work has
shown how Wasm can provide SFI by compiling untrusted C/C++ libraries to
native code using Wasm as an IR (Bosamiya et al., 2020; Zakai, 2020; Narayan
et al., 2019, 2020). We show that Wasm satisfies our zero-cost conditions, and
replace the heavyweight transitions used by the industrial Lucet Wasm SFI
toolkit with zero-cost transitions. Wasm imposes more structure than required
by our zero-cost conditions (and Wasm compilers are still relatively new and
slow (Jangda et al., 2019)), so, in order to compare the overhead of our zero-
cost model to the still fastest SFI implementation— NaCl (Yee et al., 2009)—
we design a new prototype SFI system (SegmentZero32) that: (1) enforces our
zero-cost conditions through LLVM-level transformations, and (2) enforces
memory isolation in hardware, using 32-bit x86 segmentation.222While the
prevalence of 32-bit x86 systems is declining, it nevertheless still
constitutes over 20% of the Firefox web browser’s user base (over forty
million users) (Mozilla, 2021); SegmentZero32 would allow for high performance
library sandboxing on these machines.

4\. Verifying security at the binary level (§6). Our fourth contribution is a
_static verifier_ , VeriZero, that checks whether a potentially malicious
binary produced by the Lucet toolkit satisfies our zero-cost conditions. This
removes the need to trust the Lucet compiler when, for example, compiling
third-party Firefox libraries (Narayan et al., 2020) or untrusted tenant code
running on Fastly’s serverless cloud (McMullen, 2020). To prove the soundness
of VeriZero, we develop a logical relation that captures when a compiled Wasm
function is well-behaved with respect to our zero-cost conditions and use it
to prove that the checks of VeriZero guarantee that the zero-cost conditions
are met. We implement VeriZero by extending VeriWasm (Johnson et al., 2021)
and show that in just a few seconds, it can (1) verify sandboxed libraries
that ship (or are in the process of being shipped) with Firefox, Wasm-compiled
SPEC CPU® 2006 benchmarks, and 100,000 programs randomly generated by Csmith
(Yang et al., 2011), and (2) catch previous NaCl and Wasm vulnerabilities
(§7.4). VeriZero is being integrated into the Lucet industrial Wasm compiler
(Johnson, 2021).

5\. Implementation and evaluation (§7). Our last contribution is an
implementation of our zero-cost sandboxing toolkits, and an evaluation of how
they improve the performance of a transition micro-benchmark and two macro-
benchmarks— image decoding (libjpeg) and font rendering (libgraphite) in
Firefox. First, we demonstrate the potential performance of a purpose-built
zero-cost SFI system, by evaluating SegmentZero32 on SPEC CPU® 2006 and our
macro-benchmarks. We find that SegmentZero32 imposes at most 25% overhead on
SPEC CPU® 2006 (nc), and at most 24% on image decoding and 22.5% on font
rendering. These overheads are lower than the state-of-art NaCl SFI system. On
the macro-benchmarks, SegmentZero32 even outperforms an idealized SFI system
that enforces memory isolation for free but requires heavyweight transitions.
Second, we find that zero-cost transitions speed up Wasm-sandboxed image
decoding by (up to) 29.7% and font rendering by 10%. The speedup resulting
from our zero-cost transitions allowed Mozilla to ship the Wasm-sandboxed
libgraphite library in production.

Open source and data. Our code and data will be made available under an open
source license.

##  2\. Overview

In this section we describe the role of transitions in making SFI secure, give
an overview of existing heavyweight transitions, and introduce our zero-cost
model, which makes it possible for SFI systems to replace heavyweight
transitions with simple function calls.

###  2.1. The need for secure transitions

As an example, consider sandboxing an untrusted font rendering library (e.g.,
libgraphite) as used in a browser like Firefox:

⬇

1void onPageLoad(int* text) {

2 ...

3 int* screen = ...; // stored in r12

4 int* temp_buf = ...;

5 gr_get_pixel_buffer(text, temp_buf);

6 memcpy(screen, temp_buf, 100);

7 ...

8}

This code calls the libgraphite gr_get_pixel_buffer function to render text
into a temporary buffer and then copies the temporary buffer to the variable
screen to be rendered.

Using SFI to sandbox this library ensures that the browser’s memory is
isolated from libgraphite— memory isolation ensures that gr_get_pixel_buffer
cannot access the memory of onPageLoad or any other parts of the browser stack
and heap. Unfortunately, memory isolation alone is not enough: if transitions
are simply function calls, attackers can violate the calling convention at the
application-library boundary (e.g., the gr_get_pixel_buffer call and its
return) to break isolation. Below, we describe the different ways a
compromised libgraphite can do this.

Clobbering callee-save registers. Suppose the screen variable in the above
onPageLoad snippet is compiled down to the register r12. In the System V
calling convention r12 is a _callee-saved_ register (Lu et al., 2018), so if
gr_get_pixel_buffer clobbers r12, then it is also supposed to restore it to
its original value before returning to onPageLoad. A compromised libgraphite
doesn’t have to do this; instead, the attacker can poison the register:

⬇

1mov r12, ☣

2ret

Since r12 (screen) in our hypothetical example is then used on Line 6 to
memcpy the temp_buf from the sandbox memory, this gives the attacker a write
gadget that they can use to hijack Firefox’s control flow. To prevent such
attacks, we need _callee-save register integrity_ , i.e., we must ensure that
sandboxed code restores callee-save registers upon returning to the
application.

Leaking scratch registers. Dually, _scratch registers_ can potentially leak
sensitive information into the sandbox. Suppose that Firefox keeps a secret
(e.g., an encryption key) in a scratch register. Memory isolation alone would
not prevent an attacker-controlled libgraphite from using uninitialized
registers, thereby reading this secret. To prevent such leaks, we need
_scratch register confidentiality_.

Reading and corrupting stack frames. Finally, if the application and sandboxed
library share a stack, the attacker could potentially read and corrupt data
(and pointers) stored on the stack. To prevent such attacks, we need _stack
frame encapsulation_ , i.e., we need to ensure that sandboxed code cannot
access application stack frames.

###  2.2. Heavyweight transitions

SFI toolchains— from NaCl (Yee et al., 2009) to Wasm native compilers like
Lucet (Bytecode Alliance, 2020a) and WAMR (Bytecode Alliance, 2020b)— use
_heavyweight transitions_ to wrap calls and returns and address the
aforementioned attacks. These heavyweight transitions are secure transitions.
They provide:

1\. Callee-save register integrity. The _springboard_ — the transition code
which wraps calls— saves callee-save registers to a separate stack stored in
protected application memory. When returning from the library to the
application, the _trampoline_ — the code which wraps returns— restores the
registers.

2\. Scratch register confidentiality. Since any scratch register may contain
secrets, the springboard clears _all_ scratch registers before transitioning
into the sandbox.

3\. Stack frame encapsulation. Most (but not all) SFI systems provision
separate stacks for trusted and sandboxed code and ensure that the trusted
stack is not accessible from the sandbox. The springboard and trampoline
account for this in three ways. First, they track the separate stack pointers
at each transition in order to switch stacks. Second, the springboard copies
arguments passed on the stack to the sandbox stack, since sandboxed code
cannot access arguments stored on the application stack. Finally, the
trampoline tracks the actual return address on transition by keeping it in the
protected memory, so that the sandboxed library cannot tamper with it.

The cost of wrappers. Heavyweight springboards and trampolines guarantee
secure transitions but have two significant drawbacks. First, they impose an
overhead on SFI— calls into the sandboxed library become significantly more
expensive than simple application function calls (§7). Heavyweight transitions
conservatively save and clear more state than might be necessary, essentially
reimplementing aspects of an OS process switch and duplicating work done by
well-behaved libraries. Second, springboards and trampolines must be
customized to different platforms, i.e., different processors and calling
conventions, and, in extreme cases such as in Vahldiek-Oberwagner et al.
(2019), even different applications. Implementation mistakes can— and have
(Native Client team, 2009; Nacl Issue 2919, 2012; Nacl Issue 775, 2010; Nacl
Issue 1607, 2011; Nacl Issue 1633, 2011; Bartel and Doe, 2018)— resulted in
sandbox escape attacks.

###  2.3. Zero-cost transitions

Heavyweight transitions are conservative because they make few assumptions
about the structure (or possible behavior) of the code running in the sandbox.
SFI systems like NaCl and Wasm _do_ , however, impose structure on sandboxed
code to enforce memory isolation. In this section we show that by imposing
structure on sandboxed code we can make transitions less conservative.
Specifically, we describe a set of _zero-cost conditions_ that impose _just
enough_ internal structure on sandboxed code to ensure that it will behave
like a high-level, compositional language while maintaining SFI’s high
performance. SFI systems that meet these conditions can safely elide almost
all the extra work done by heavyweight springboards and trampolines, thus
moving toward the ideal of SFI transitions as simple, fast, and portable
function calls.

Zero-cost conditions. We assume that the sandboxed library code is split into
functions and that each function has an expected number of arguments. We
_formalize_ the internal structure required of library code via a _safety
monitor_ that checks the zero-cost conditions, i.e., the local requirements
necessary to ensure that calls-into and returns-from the untrusted library
functions are “well-behaved” and, hence, that they satisfy the secure
transition requirements.

1\. Callee-save register restoration. First, our monitor enforces function-
call level adherence to callee-save register conventions: our monitor tracks
callee-save state and checks that it has been correctly restored upon
returning. Importantly, satisfying the monitor means that application calls to
a well-behaved library function do not require a transition which separately
saves and restores callee-save registers, since the function is known to obey
the standard calling convention.

2\. Well-bracketed control-flow. Second, our monitor requires that the library
code adheres to well-bracketed return edges. Abstractly, calls and returns
should be well-bracketed: when `f` calls `g` and then `g` calls `h`, `h` ought
to return to `g` and then `g` ought to return to `f`. However, untrusted
functions may subvert the control stack to implement arbitrary control flow
between functions. This unrestricted control flow is at odds with
compositional reasoning, preventing _local_ verification of functions.
Further, subverting well-bracketing could enable an attacker to cause `h` to
return directly to `f`. Then, even if `h` and `f` both restore their callee-
save registers, those of `g` would be left unrestored. Accordingly, we require
two properties of the library to ensure that calls and returns are well-
bracketed. First, each jump must stay within the same function. This limits
inter-function control flow to function calls and returns. Second, the
(specification) monitor maintains a “logical” call stack, which is used to
ensure that returns go only to the preceding caller.

3\. Type-directed forward-edge CFI. Our monitor also requires that library
code obeys type-directed forward-edge CFI. That is, for every call instruction
encountered during execution, the jump target address is the start of a
library function and the arguments passed match those expected by the called
function. This ensures that each function starts from a (statically) known
stack shape, preventing a class of attacks where a benign function can be
tricked into overwriting other stack frames or hijacking control flow because
it is passed too few (or too many) arguments. If this were not the case, a
locally well-behaved function that was passed too few arguments could write to
a saved register or the saved return address, expecting that stack slot to be
the location of an argument.

4\. Local state encapsulation. Our monitor establishes _local state
encapsulation_ by checking that all stack reads and writes are within the
current stack frame. This check allows us to _locally_ , i.e., by checking
each function in isolation, ensure that a library function correctly saves and
restores callee-save registers upon entry and exit. To see why local state
encapsulation is needed, consider the following idealized assembly function
library_func:

⬇

1library_func: library_helper:

2 push r12 store sp - 1 := ☣

3 mov r12 $\leftarrow$ 1 ret

4 load r1 $\leftarrow$ sp - 1

5 add r1 $\leftarrow$ r12

6 call library_helper

7 pop r12

8 ret

If library_helper is called it will overwrite the stack slot where
library_func saved r12, and library_func will then “restore” r12 to the
attacker’s desired value. Our monitor prohibits such cross-function tampering,
thus ensuring that all subsequent reasoning about callee-save integrity can be
carried out locally in each function.

5\. Confidentiality. Finally, our monitor uses dynamic information flow
control (IFC) tracking to define the confidentiality of scratch registers. The
monitor tracks how (secret application) values stored in scratch registers
flow through the sandboxed code, and checks that the library code does not
leak this information. Concretely, our implementations enforce this by
ensuring that, within each function’s localized control flow, all register and
local stack variables are initialized before use.

The individual properties making up our zero-cost conditions are well-known to
be beneficial to software security, and their enforcement in low-level code
has been extensively studied (§9): our insight— made manifest in the monitor
soundness proofs of Section 4.2— is that in conjunction these conditions are
_sufficient_ to eliminate heavyweight transitions in SFI systems, which can
currently be a source of significant overhead when sandboxing arbitrary code.
Indeed, in Section 5.1 we show that the Wasm type system is strict enough to
ensure that a Wasm compiler generates native code that already meets these
conditions. To increase the trustworthiness of this zero-cost compatible Wasm,
in Section 6 we describe a verifier that statically checks that compiled Wasm
code meets the zero-cost conditions. In Section 6.1 we describe our proof of
soundness for the verifier, proving that the verifier’s checks ensure monitor
safety and therefore zero-cost security. Further, in Section 5.2 we
demonstrate how the zero-cost conditions can be used to design a new SFI
scheme by combining hardware-backed memory isolation with existing LLVM
compiler passes.

##  3\. A Gated Assembly Language

|  | $n$ | $\in$ | $\mathbb{N}$
---|---|---|---|---
$\mathit{Priv}$ | $\ni$ | $p$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathtt{app}\mid\mathtt{lib}$
$\mathit{Val}$ | $\ni$ | $v$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $n$
$\mathit{Reg}$ | $\ni$ | $r$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathtt{r}_{n}\mid sp\mid pc$
$\mathit{Region}$ | $\ni$ | $k$ | $\in$ | $\mathbb{N}\rightharpoonup\mathbb{N}$
$\mathit{Expr}$ | $\ni$ | $e$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $r\mid v\mid e\oplus e$
$\mathit{Command}$ | $\ni$ | $c$ | $\mathrel{\vcentcolon\vcentcolon=}$ | ${r}\leftarrow\mathtt{pop}_{p}\mid\mathtt{push}_{p}\ {e}\mid\mathtt{jmp}_{{k}}\ {e}\mid{r}\leftarrow\mathtt{load}_{k}\ {e}\mid\mathtt{store}_{k}\ {e}\mathbin{\vcentcolon=}{e}\mid$
|  |  |  | $\mathtt{gatecall}_{n}\ {e}\mid\mathtt{gateret}\mid{r}\leftarrow\mathtt{mov}\ {e}\mid\mathtt{call}_{{k}}\ {e}\mid\mathtt{ret}_{{k}}\mid$
|  |  |  | ${r}\leftarrow\mathtt{movlabel}_{p}\mid\mathtt{storelabel}_{p}\ {e}$
$\mathit{Code}$ | $\ni$ | $C$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathbb{N}\rightharpoonup\mathit{Priv}\times\mathit{Command}$
$\mathit{RegVals}$ | $\ni$ | $R$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathit{Reg}\rightarrow\mathit{Val}$
$\mathit{Memory}$ | $\ni$ | $M$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathbb{N}\rightarrow\mathit{Val}$
$\mathit{State}$ | $\ni$ | $\Psi$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\mathtt{error}\mid\\{pc\mathrel{\vcentcolon}\mathbb{N},sp\mathrel{\vcentcolon}\mathbb{N},R\mathrel{\vcentcolon}\mathit{RegVals},M\mathrel{\vcentcolon}\mathit{Memory},C\mathrel{\vcentcolon}\mathit{Code}\\}$
Figure 1. Syntax

We formalize zero-cost transitions via an assembly language, SFIasm, that
captures key notions of an application interacting with a sandboxed library,
focusing on capturing properties of the transitions between the application
and sandboxed library.

Code. Figure 1 summarizes the syntax of SFIasm: a Risc-style language with
natural numbers ($\mathbb{N}$) as the sole data type. Code ($C$) and data
($M$) memory are separated, and, to capture the separation of application code
from sandboxed library code, $C$ is an (immutable) partial map from
$\mathbb{N}$ to pairs of a privilege ($p$) ($\mathtt{app}$ or $\mathtt{lib}$)
and a command ($c$), where $\mathtt{app}$ and $\mathtt{lib}$ are our _security
domains_.

States. Memory is a (total) map from $\mathbb{N}$ to values ($v$). We assume
that the memory is subdivided into disjoint regions ($M_{p}$) so that the
application and library have separate memory. Each of these regions is further
divided into a disjoint heap $H_{p}$ and stack $S_{p}$. We write $\Psi$ to
denote the states or machine configurations, which comprise code, memory, and
a fixed, finite set of registers mapping register names $(r_{n})$ to values,
with a distinguished stack pointer ($sp$) and program counter ($pc$) register.
We write ${\Psi}\llparenthesis{c}\rrparenthesis_{p}$ for
$\Psi.C(\Psi.pc)=(p,c)$, that is that the current instruction is $c$ in
security domain $p$. We write $\Psi_{0}\in\mathit{Program}$ to mean that
$\Psi_{0}$ is a valid initial program state. The definition of validity varies
between different SFI techniques (e.g., heavyweight transitions make
assumptions about the initial state of the separate stack).

Gated calls and returns. We capture the transitions between the application
and the library by defining a pair of instructions $\mathtt{gatecall}_{n}\
{e}$ and $\mathtt{gateret}$, that serve as the _only_ way to switch between
the two security domains (that is, $\mathtt{call}$ and $\mathtt{ret}$ check
that the target is in the same security domain). The first,
$\mathtt{gatecall}_{n}\ {e}$, represents a call from the application into the
sandbox or a callback from the sandbox to the application with the $n$
annotation representing the number of arguments to be passed. The second,
$\mathtt{gateret}$, represents the corresponding return from sandbox to
application or vice-versa. We leave the reduction rule for both
_implementation specific_ in order to capture the details of a given SFI
system’s trampolines and springboards.

Memory isolation. SFIasm provides abstract mechanisms for enforcing SFI memory
isolation by equipping the standard $\mathtt{load}$, $\mathtt{store}$,
$\mathtt{push}$, and $\mathtt{pop}$ with (optional) statically annotated
checks. To capture different styles of enforcement we model these checks as
partial functions that map a pointer to its new value or are undefined when a
particular address is invalid. This lets us, for instance, capture NaCl’s
coarse grained, dynamically enforced isolation (sandboxed code may read and
write anywhere in the sandbox memory) by requiring that all loads and stores
are annotated with the check $k(n)|_{n\in M_{\mathtt{lib}}}=n$. This captures
that NaCl’s memory isolation does not remap addresses but traps when an
address is outside the sandbox memory region ($M_{\mathtt{lib}}$).333NaCl
implements memory protection differently on different platforms. The 32-bit
implementation traps whereas the 64-bit implementation masks addresses. We
focus on the former. The rule for $\mathtt{load}$ below demonstrates the use
of these region annotations in the semantics.

Control-flow integrity. SFIasm also provides abstract control-flow integrity
enforcement via annotations on $\mathtt{jmp}$, $\mathtt{call}$, and
$\mathtt{ret}$. These are also enforced dynamically. However, we require that
the standard control flow operations remain within their own security domain
so that $\mathtt{gatecall}$ and $\mathtt{gateret}$ remain the only way to
switch security domains.

Operational semantics. We capture the dynamic behavior via a deterministic
small-step operational semantics ($\Psi\mathrel{\rightarrow}\Psi^{\prime}$).
The rules are standard; we show the rule for $\mathtt{load}$ here:

$\displaystyle\displaystyle{\hbox{\hskip
106.73965pt\vbox{\hbox{\hskip-106.73964pt\hbox{\hbox{$\displaystyle\displaystyle
addr=\mathcal{V}_{\Psi}({e})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
addr^{\prime}=k(addr)$}\hskip
18.00003pt\hbox{\hskip-67.95428pt\hbox{\hbox{$\displaystyle\displaystyle
v=\Psi.M(addr^{\prime})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle R^{\prime}=\Psi.R[r\mapsto
v]$}}}}}}}\vbox{\hbox{\hskip-67.95428pt\hbox{\hbox{$\displaystyle\displaystyle
v=\Psi.M(addr^{\prime})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle R^{\prime}=\Psi.R[r\mapsto
v]$}}}}\vbox{}}}}\over\hbox{\hskip
56.65796pt\vbox{\vbox{}\hbox{\hskip-56.65796pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{{r}\leftarrow\mathtt{load}_{k}\
{e}}\rrparenthesis\mathrel{\rightarrow}{\Psi}^{++}[R\mathbin{\vcentcolon=}R^{\prime}]$}}}}}}$

$\mathcal{V}_{\Psi}({e})$ evaluates the expression based on the register file
and ${\Psi}^{++}$ increments $pc$, checking that it remains within the same
security domain and returning an error otherwise. If the function $k(addr)$ is
undefined ($addr$ is not within bounds), the program will step to a
distinguished, terminal state $\mathtt{error}$.
${\Psi}\llparenthesis{c}\rrparenthesis$ is simply shorthand for
${\Psi}\llparenthesis{c}\rrparenthesis_{p}$ when we do not care about the
security domain. Lastly, we do not include a specific halt command, instead
halting when $pc$ is not in the domain of $C$.

###  3.1. Secure transitions

Next, we use SFIasm to _declaratively_ specify high-level properties that
capture the intended security goals of transition systems. This lets us use
SFIasm both as a setting to study zero-cost transitions and to explore the
correctness of implementations of springboards and trampolines. As a
demonstrative example we prove that NaCl-style heavyweight transitions satisfy
the high-level properties (§B).

$\displaystyle\displaystyle{\hbox{\hskip
68.73412pt\vbox{\hbox{\hskip-68.7341pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{1}\mathrel{\rightarrow}\Psi_{2}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{1}}\llparenthesis{c_{1}}\rrparenthesis_{p_{1}}$}\hskip
18.00003pt\hbox{\hskip-44.5175pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{c_{2}}\rrparenthesis_{p_{2}}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{1}=p_{2}=p$}}}}}}}\vbox{\hbox{\hskip-44.5175pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{c_{2}}\rrparenthesis_{p_{2}}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{1}=p_{2}=p$}}}}\vbox{}}}}\over\hbox{\hskip
14.03409pt\vbox{\vbox{}\hbox{\hskip-14.03409pt\hbox{\hbox{$\displaystyle\displaystyle\Psi_{1}\mathrel{\xrightarrow{p}}\Psi_{2}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
12.20708pt\vbox{\hbox{\hskip-12.20708pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{p}}\Psi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
12.69302pt\vbox{\vbox{}\hbox{\hskip-12.69302pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\square}}\Psi^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
14.94304pt\vbox{\hbox{\hskip-14.94302pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
12.69302pt\vbox{\vbox{}\hbox{\hskip-12.69302pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\square}}\Psi^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
71.64082pt\vbox{\hbox{\hskip-71.64082pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\rightarrow}\Psi_{1}\mathrel{\xrightarrow{\\!\square}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{2}\mathrel{\rightarrow}\Psi^{\prime}$}\hskip
18.00003pt\hbox{\hskip-64.83546pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{i}}\rrparenthesis$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$}}}}}}\vbox{\hbox{\hskip-64.83546pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi}\llparenthesis{\mathtt{gatecall}_{n}\
{i}}\rrparenthesis$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\Psi_{2}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$}}}}\vbox{}}}}\over\hbox{\hskip
14.94304pt\vbox{\vbox{}\hbox{\hskip-14.94302pt\hbox{\hbox{$\displaystyle\displaystyle\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$}}}}}}$
Figure 2. Well-Bracketed Transitions

Well-bracketed gated calls. SFI systems may allow arbitrary _nesting_ of calls
into and callbacks out of the sandbox. Thus, it is insufficient to define that
callee-save registers have been properly restored by simply equating register
state upon entry to the sandbox and the following exit. Instead we make the
notion of an entry and its _corresponding_ exit precise, by using SFIasm’s
$\mathtt{gatecall}$ and $\mathtt{gateret}$ to define a notion of _well-
bracketed gated calls_ that serve as the backbone of transition integrity
properties. A well-bracketed gated call, which we write
$\Psi\mathrel{\xrightarrow{\\!\text{wb}}}\Psi^{\prime}$ (Figure 2), captures
the idea that $\Psi$ is a gated call from one security domain to another,
followed by running in the new security domain, and then $\Psi^{\prime}$ is
the result of a gated return that balances the gated call from $\Psi$. This
can include potentially recursive but properly bracketed gated calls. Well-
bracketed gated calls let us relate the state before a gated call with the
state after the _corresponding_ gated return, capturing when the library has
fully returned to the application.

Integrity. Relations between the states before calling into the sandbox and
then after the corresponding return capture SFI transition system _integrity_
properties. We identify two key integrity properties that SFI transitions must
maintain:

_1\. Callee-save register integrity_ requires that callee-save registers are
restored after returning from a gated call into the library. This ensures that
an attacker cannot unexpectedly modify the private state of an application
function.

_2\. Return address integrity_ requires that the sandbox  (1) returns to the
instruction after the $\mathtt{gatecall}$,  (2) does not tamper with the stack
pointer, and  (3) does not modify the call stack itself.  Together these
ensure that an attacker cannot tamper with the application control flow.

These integrity properties are crucial to ensure that the sandboxed library
cannot break application invariants. To capture them formally, we first define
an abstract notion of integrity across a well-bracketed gated call. This not
only allows us to cleanly define the above properties, but also provides a
general framework that can capture integrity properties for different
architectures.

Specifically, we define an integrity property by a predicate
$\mathcal{I}:\mathit{Trace}\times\mathit{State}\times\mathit{State}\rightarrow\mathbb{P}$
that captures when integrity is preserved across a call ($\mathbb{P}$ is the
type of propositions). The first argument is a trace, a sequence of steps that
our program has taken before making the gated call. The next two arguments are
the states before and after the well-bracketed gated call. $\mathcal{I}$
defines when these two states are properly related. This leads to the
following definition of $\mathcal{I}$-Integrity:

###### Definition 0 ($\mathcal{I}$-Integrity).

Let
$\mathcal{I}:\mathit{Trace}\times\mathit{State}\times\mathit{State}\rightarrow\mathbb{P}$.
We say that an SFI transition system has $\mathcal{I}$-integrity if
$\Psi_{0}\in\mathit{Program}$,
$\pi=\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi_{1}$,
${\Psi_{1}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$, and
$\Psi_{1}\mathrel{\xrightarrow{\\!\text{wb}}}\Psi_{2}$ imply that
$\mathcal{I}(\pi,\Psi_{1},\Psi_{2})$.

We instantiate this to define our two integrity properties:

Callee-save register integrity. We define callee-save register integrity as an
$\mathcal{I}$-integrity property that requires the callee-save registers’
values to be equal in both states:

###### Definition 0 (Callee-Save Register Integrity).

Let $\mathbb{CSR}$ be the callee-save registers and define
$\mathcal{CSR}(\\_,\Psi_{1},\Psi_{2})\triangleq\Psi_{2}.R(\mathbb{CSR})=\Psi_{1}.R(\mathbb{CSR})$.
If an SFI transition system has $\mathcal{CSR}$-integrity then we say it has
callee-save register integrity.

Return address integrity. We specify that the library returns to the expected
instruction as a relation between $\Psi_{1}$ and $\Psi_{2}$, namely that
$\Psi_{2}.pc=\Psi_{1}.pc+1$. Restoration of the stack pointer is similarly
specified as $\Psi_{2}.sp=\Psi_{1}.sp$. Specifying call stack integrity is
more involved as $\Psi_{1}$ lacks information on where return addresses are
saved: they look like any other stack data. Instead, return addresses are
defined by the history of calls and returns leading up to $\Psi_{1}$, which we
capture with the trace argument $\pi$. We thus define a function
$\operatorname{return-address}(\pi)$ (see Figure 18 in the appendix) that
computes the locations of return addresses from a trace. The third clause of
return address integrity is then that these locations’ values are preserved
from $\Psi_{1}$ to $\Psi_{2}$, yielding:

###### Definition 0 (Return Address Integrity).

$\displaystyle\mathcal{RA}(\pi,\Psi_{1},\Psi_{2})$
$\displaystyle\triangleq\Psi_{2}.pc=\Psi_{1}.pc+1\wedge\Psi_{2}.sp=\Psi_{1}.sp$
$\displaystyle\wedge\Psi_{2}.M(\operatorname{return-
address}(\pi))=\Psi_{1}.M(\operatorname{return-address}(\pi))$

If an SFI transition system has $\mathcal{RA}$-integrity then we say the
system has return address integrity.

Confidentiality. SFI systems must ensure that secrets cannot be leaked to the
untrusted library, i.e., they must provide _confidentiality_. We specify
confidentiality as noninterference, which informally states that “changing
secret inputs should not affect public outputs.” In the context of library
sandboxing, application data is secret whereas library data is non-secret
(public).444This could also be extended to a setting with mutually distrusting
components. To capture this formally, we pair programs with a confidentiality
policy,
$\mathbb{C}\in\mathit{State}\rightharpoonup(\mathbb{N}\mathrel{+}\mathit{Reg}\rightarrow\mathit{Priv})$,
that labels all memory and registers as $\mathtt{app}$ or $\mathtt{lib}$ at
each gated call into the library. These labels form a lattice:
$\mathtt{lib}\sqsubseteq\mathtt{app}$ (non-secret _can_ “flow to” secret) and
$\mathtt{app}\not\sqsubseteq\mathtt{lib}$ (secret _cannot_ “flow to” non-
secret).555Details can be found in Section A.1.2.

To prove noninterference, that changing secret data does not affect public (or
non-secret) outputs, we need to define public outputs. We over-approximate
public outputs as the set of values _exposed_ to the application. This
includes all arguments to a $\mathtt{gatecall}$ callback, the return value
when returning to the application via $\mathtt{gateret}$, and all values
stored in the sandboxed library’s heap ($H_{\mathtt{lib}}$) (which may be
referenced by other returned values).

Alas, this is not enough: in a callback, the application may choose to
declassify secret data. For instance, a sandboxed image decoding library
might, after parsing the file header, make a callback requesting the data to
decode the rest of the image. This application callback will then transfer
that data (which was previously confidential) to the sandbox, declassifying it
in the transfer.

To account for such intentional declassifications, we follow Matos and Boudol
(2005) and define confidentiality as _disjoint noninterference_. We use
$\Psi=_{\mathbb{C}}\Psi^{\prime}$ to mean that $\Psi$ and $\Psi^{\prime}$
agree on all values labeled $\mathtt{lib}$ by the confidentiality policy,
capturing varying secret inputs. We further write $\Psi=_{\mathtt{call}\
m}\Psi^{\prime}$ when $\Psi$ and $\Psi^{\prime}$ agree on all sandboxed heap
values, the program counter, and the $m$ arguments passed to a callback and
$\Psi=_{\mathtt{ret}}\Psi^{\prime}$ when $\Psi$ and $\Psi^{\prime}$ agree on
all sandboxed heap values, the program counter, and the value in the return
register (written $r_{ret}$).666Full definitions are in Appendix A Definition
4 and Definition 5. This lets us formally define noninterference as follows:

###### Definition 0 (Disjoint Noninterference).

We say that an SFI transition system has the disjoint noninterference property
if, for all initial configurations and their confidentiality properties
$(\Psi_{0},\mathbb{C})\in\mathit{Program}$, traces
$\Psi_{0}\mathrel{\mathrel{\rightarrow}^{\ast}}\Psi_{1}\mathrel{\rightarrow}\Psi_{2}\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}\mathrel{\rightarrow}\Psi_{4}$,
where $\Psi_{1}$ is a gated call into the library
(${\Psi_{1}}\llparenthesis{\mathtt{gatecall}_{n}\
{e}}\rrparenthesis_{\mathtt{app}}$), and
$\Psi_{3}\mathrel{\rightarrow}\Psi_{4}$ leaves the library and reenters the
application (${\Psi_{4}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$),
and, for all $\Psi_{1}^{\prime}$ such that
$\Psi_{1}=_{\mathbb{C}}\Psi_{1}^{\prime}$, we have that
$\Psi_{1}^{\prime}\mathrel{\rightarrow}\Psi_{2}^{\prime}\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{\ast}}}\Psi_{3}^{\prime}\mathrel{\rightarrow}\Psi_{4}^{\prime}$,
${\Psi_{4}^{\prime}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
$\Psi_{4}.pc=\Psi_{4}^{\prime}.pc$, and either  (1) $\Psi_{3}$is a gated call
to the application (${\Psi_{3}}\llparenthesis{\mathtt{gatecall}_{m}\
{e}}\rrparenthesis$ and
${\Psi_{3}^{\prime}}\llparenthesis{\mathtt{gatecall}_{m}\ {e}}\rrparenthesis$)
and $\Psi_{4}=_{\mathtt{call}\ m}\Psi_{4}^{\prime}$ or  (2) $\Psi_{3}$is a
gated return to the application
(${\Psi_{3}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$ and
${\Psi_{3}^{\prime}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$) and
$\Psi_{4}=_{\mathtt{ret}}\Psi_{4}^{\prime}$.

This definition captures that, for any sequence of executing within the
library then returning control to the application, varying confidential inputs
does not influence the public outputs and the library returns control to the
application in the same number of steps. Thus, an SFI system that satisfies
Disjoint Noninterference is guaranteed to not leak data while running within
the sandbox.

We formalize NaCl style heavyweight transitions in Appendix B and prove that
they meet the above secure transition properties. We discuss our proof that
zero-cost Wasm meets the above secure transition properties in Section 6.1.

##  4\. Zero-Cost Transition Conditions

$\mathit{Val}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{p}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}$
---|---|---|---|---
$\mathit{Frame}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\\{\mathit{base}\mathrel{\vcentcolon}\mathbb{N};\mathit{ret\mbox{-}addr\mbox{-}loc}\mathrel{\vcentcolon}\mathbb{N};\mathit{csr\mbox{-}vals}\mathrel{\vcentcolon}\wp({\mathit{Reg}\times\mathbb{N}})\\}$
$\mathit{Function}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | $\\{\mathit{instrs}\mathrel{\vcentcolon}\mathbb{N}\rightharpoonup\mathit{Command};\mathit{entry}\mathrel{\vcentcolon}\mathbb{N};\mathit{type}\mathrel{\vcentcolon}\mathbb{N}\\}$
$\mathit{oState}$ | $\ni$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}$ | $\mathrel{\vcentcolon\vcentcolon=}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}\mid\\{\Psi\mathrel{\vcentcolon}\mathit{State};\mathit{funcs}\mathrel{\vcentcolon}\mathbb{N}\rightharpoonup\mathit{Function};\mathit{stack}\mathrel{\vcentcolon}[\mathit{Frame}]\\}$
Figure 3. oSFIasm Extended Syntax

Having laid out the security properties required of an SFI transition system,
we turn to formally defining the set of zero-cost conditions on sandboxed code
such that they sufficiently capture when we may securely elide springboards or
trampolines. To this end we define our zero-cost conditions as a safety
monitor via the language oSFIasm overlaid on top of SFIasm. oSFIasm extends
SFIasm with additional structure and dynamic type checks that ensure the
invariants needed for zero-cost transitions are maintained upon returning from
library functions, providing both an inductive structure for proofs of
security for zero-cost implementations and providing a top-level guarantee
that our integrity and confidentiality properties are maintained. In Section
4.2 we outline the proofs of overlay soundness, showing that oSFIasm captures
when a system is zero-cost secure.

Syntax of oSFIasm. Figure 3 shows the extended syntax of oSFIasm. Values
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}$) are
extended with a security label $p$. Overlay state, written
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}$,
wraps the state of SFIasm, extending it with two extra pieces of data. First,
oSFIasm requires the sandboxed code be organized into functions
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}$).
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}$
maps each command in the sandboxed library to its parent function. Functions
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}$)
also store the code indices of their commands as the field
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{instrs}$,
store the entry point
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{entry}$),
and track the number of arguments the function expects
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{type}$).
This partitioning of sandboxed code into functions is static. Second, the
overlay state dynamically tracks a list of overlay stack frames
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$).
These stack frames
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}$)
are solely logical and inaccessible to instructions. They instead serve as
bookkeeping to implement the dynamic type checks of oSFIasm by tracking the
base address of each stack frame
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{base}$),
the stack location of the return address
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr}$),
and the values of the callee save registers upon entry to the function
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{csr\mbox{-}vals}$).
We are concerned with the behavior of the untrusted library, so the logical
stack does not finely track application stack frames, but keeps a single large
“stack frame” for all nested application stack frames.

When code fails the overlay’s dynamic checks it will result in the state
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$.
Our definition of monitor safety, which will ensure that zero-cost transitions
are secure, is then simply that a program does not step to an
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$.

###  4.1. Overlay monitor

oCall $\displaystyle\displaystyle{\hbox{\hskip
193.15804pt\vbox{\hbox{\hskip-145.83173pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp+1$}\hskip
18.00003pt\hbox{\hskip-97.86401pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc+1]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{stack}^{\prime}=[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}}}}}}}}\vbox{\hbox{\hskip-97.86401pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[sp^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc+1]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{stack}^{\prime}=[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}}}}\vbox{\hbox{\hskip-193.15804pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}=\operatorname{new-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{typechecks}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime},sp^{\prime})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[\mathit{stack}\mathbin{\vcentcolon=}\mathit{stack}^{\prime},pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}sp^{\prime},M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}\vbox{}}}}}\over\hbox{\hskip
33.7296pt\vbox{\vbox{}\hbox{\hskip-33.72958pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{call}_{{k}}\
{e}}\rrparenthesis_{\mathtt{lib}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}$}}}}}}$
oRet $\displaystyle\displaystyle{\hbox{\hskip
151.71925pt\vbox{\hbox{\hskip-151.71925pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{is-
ret-
addr}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp)$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp)$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
18.00003pt\hbox{\hskip-72.79312pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{csr-
restored}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}=\operatorname{pop-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}}}}}}}}\vbox{\hbox{\hskip-72.79312pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{csr-
restored}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}=\operatorname{pop-
frame}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}}}}\vbox{}}}}\over\hbox{\hskip
69.49919pt\vbox{\vbox{}\hbox{\hskip-69.49919pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{ret}_{{k}}}\rrparenthesis_{\mathtt{lib}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}[pc\mathbin{\vcentcolon=}n^{\prime},sp\mathbin{\vcentcolon=}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.sp-1]$}}}}}}$
oJmp $\displaystyle\displaystyle{\hbox{\hskip
85.83762pt\vbox{\hbox{\hskip-85.8376pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
18.00003pt\hbox{\hskip-47.75557pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc,n^{\prime})$}}}}}}\vbox{\hbox{\hskip-47.75557pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.pc,n^{\prime})$}}}\vbox{}}}}\over\hbox{\hskip
48.76714pt\vbox{\vbox{}\hbox{\hskip-48.76714pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{jmp}_{{k}}\
{e}}\rrparenthesis_{\mathtt{lib}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}[pc\mathbin{\vcentcolon=}n^{\prime}]$}}}}}}$
oStore $\displaystyle\displaystyle{\hbox{\hskip
164.63092pt\vbox{\hbox{\hskip-164.6309pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{n},{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\langle}}{\\_},{p_{e^{\prime}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\rangle}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{V}}}_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}({e^{\prime}})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
M^{\prime}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.M[n^{\prime}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{v}}]$}\hskip
18.00003pt\hbox{\hskip-99.11986pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e^{\prime}}=\mathtt{app}\Longrightarrow n^{\prime}\notin
H_{\mathtt{lib}}$}}}}}}}}}\vbox{\hbox{\hskip-99.11986pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n^{\prime})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle n^{\prime}=k(n)$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
p_{e^{\prime}}=\mathtt{app}\Longrightarrow n^{\prime}\notin
H_{\mathtt{lib}}$}}}}}\vbox{}}}}\over\hbox{\hskip
64.93793pt\vbox{\vbox{}\hbox{\hskip-64.93791pt\hbox{\hbox{$\displaystyle\displaystyle{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}\llparenthesis{\mathtt{store}_{k}\
{e}\mathbin{\vcentcolon=}{e^{\prime}}}\rrparenthesis_{\mathtt{lib}}\mathrel{\leadsto}{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}[M\mathbin{\vcentcolon=}M^{\prime}]$}}}}}}$
Figure 4. oSFIasm Operational Semantics Excerpt
$\displaystyle\displaystyle{\hbox{\hskip
155.6064pt\vbox{\hbox{\hskip-155.6064pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}(\mathit{target})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{entry}=\mathit{target}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle sp\in S_{p}$}\hskip
18.00003pt\hbox{\hskip-94.44234pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr}+{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{type}$}}}}}}}}\vbox{\hbox{\hskip-94.44234pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
sp\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr}+{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{type}$}}}}\vbox{}}}}\over\hbox{\hskip
47.161pt\vbox{\vbox{}\hbox{\hskip-47.16098pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{typechecks}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},\mathit{target},sp)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
66.83138pt\vbox{\hbox{\hskip-66.83138pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
18.00003pt\hbox{\hskip-42.23758pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{ret\mbox{-}addr}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr}$}}}}}\vbox{\hbox{\hskip-42.23758pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{ret\mbox{-}addr}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr}$}}}\vbox{}}}}\over\hbox{\hskip
44.57507pt\vbox{\vbox{}\hbox{\hskip-44.57507pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{is-
ret-
addr}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},\mathit{ret\mbox{-}addr})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
53.88203pt\vbox{\hbox{\hskip-53.88202pt\hbox{\hbox{$\displaystyle\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}\in\operatorname{cod}({{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{funcs}})$}\hskip
18.00003pt\hbox{\hskip-26.67638pt\hbox{\hbox{$\displaystyle\displaystyle
n,n^{\prime}\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{instrs}$}}}}}\vbox{\hbox{\hskip-26.67638pt\hbox{\hbox{$\displaystyle\displaystyle
n,n^{\prime}\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}.\mathit{instrs}$}}}\vbox{}}}}\over\hbox{\hskip
41.74516pt\vbox{\vbox{}\hbox{\hskip-41.74516pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{in-
same-
func}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n,n^{\prime})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
78.73216pt\vbox{\hbox{\hskip-78.73216pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
18.00003pt\hbox{\hskip-66.03917pt\hbox{\hbox{$\displaystyle\displaystyle\forall(r,n)\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{csr\mbox{-}vals}.\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r)=n$}}}}}\vbox{\hbox{\hskip-66.03917pt\hbox{\hbox{$\displaystyle\displaystyle\forall(r,n)\in{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{csr\mbox{-}vals}.\leavevmode\nobreak\
{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.R(r)=n$}}}\vbox{}}}}\over\hbox{\hskip
29.58754pt\vbox{\vbox{}\hbox{\hskip-29.58754pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{csr-
restored}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
82.62003pt\vbox{\hbox{\hskip-82.62003pt\hbox{\hbox{$\displaystyle\displaystyle[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}]\mathbin{{+}\mspace{-8.0mu}{+}}\\_={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\mathit{stack}$}\hskip
18.00003pt\hbox{\hskip-73.8149pt\hbox{\hbox{$\displaystyle\displaystyle n\in
S_{p}\Longrightarrow
n\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{base}\wedge
n\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr}$}}}}}\vbox{\hbox{\hskip-73.8149pt\hbox{\hbox{$\displaystyle\displaystyle
n\in S_{p}\Longrightarrow
n\geq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{base}\wedge
n\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathit{SF}}}.\mathit{ret\mbox{-}addr}$}}}\vbox{}}}}\over\hbox{\hskip
29.4636pt\vbox{\vbox{}\hbox{\hskip-29.4636pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{writeable}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}},n)$}}}}}}$
Figure 5. oSFIasm Semantics Auxiliary Predicates

oSFIasm enforces our zero-cost conditions by extending the operational
semantics of SFIasm with additional checks in the overlay’s small step
operational semantics, written
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}\mathrel{\leadsto}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}$.
Each of these steps is a refinement of the underlying SFIasm step, that is
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}.\Psi\mathrel{\rightarrow}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}.\Psi$
whenever
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}$
is not
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$.
Figure 4 (with auxiliary definitions shown in Figure 5) shows an excerpt of
the checks, which we describe below. Full definitions can be found in Appendix
C. The checks are similar in nature to the defensive semantics of Besson et
al. (2018) though they account for confidentiality and define a more flexible
notion of protecting stack frames.

Call. In the overlay, the reduction rule for library $\mathtt{call}$
instructions (oCall) checks type-safe execution with
$\operatorname{typechecks}$, a predicate over the state
(${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}$),
call target ($\mathit{target}$), and stack pointer ($sp$) that checks that
(1) the address we are jumping to is the entry instruction of one of the
functions,  (2) the stack pointer remains within the stack ($sp\in S_{p}$),
and  (3) the number of arguments expected by the callee have been pushed to
the stack.  On top of this, $\mathtt{call}$ also creates a new logical stack
frame recording the base of the new frame, location of the return address, and
the current callee-save register values, pushing the new frame onto the
overlay stack. To ensure IFC, we require that $i$ has the label $\mathtt{lib}$
to ensure that control flow is not influenced by confidential values; a
similar check is done when jumping within library code, obviating the need for
a program counter label. Further, because the overlay captures zero-cost
transitions, $\mathtt{gatecall}$ behaves in the exact same way except for an
additional IFC check that the arguments are not influenced by confidential
values.

Jmp. Our zero-cost conditions rely on preventing invariants internal to a
function from being interfered with by other functions. A key protection
enabling this is illustrated by the reduction for $\mathtt{jmp}$ (oJmp), which
enforces that the only inter-function control flow is via $\mathtt{call}$ and
$\mathtt{ret}$: the $\operatorname{in-same-func}$ predicate checks that the
current ($n$) and target ($n^{\prime}$) instructions are within the same
overlay function. The same check is added to the program counter increment
operation,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi}}}^{++}$.
These checks ensure that the logical call stack corresponds to the actual
control flow of the program, enabling the overlay stack’s use in maintaining
invariants at the level of function calls.

Store. The reduction rule for $\mathtt{store}$ (oStore) demonstrates the other
key protection enabling function local reasoning, with the check that the
address ($n$) is $\operatorname{writeable}$ given the current state of the
overlay stack. The predicate $\operatorname{writeable}$ guarantees that, if
the operation is writing to the stack, then that write must be within the
current frame and cannot be the location of the stored return address. This
allows reasoning to be localized to each function: they do not need to worry
about their callees tampering with their local variables. Protecting the
stored return address is crucial for ensuring well-bracketing, which
guarantees that each function returns to its caller.

To guarantee IFC, oStore first requires that the pointer have the label
$\mathtt{lib}$, ensuring that the location we write to is not based on
confidential data. Second, the check
$p_{i^{\prime}}=\mathtt{app}\Longrightarrow n^{\prime}\notin H_{\mathtt{lib}}$
enforces that confidential values cannot be written to the library heap.
Similar checks, based on standard IFC techniques, are implemented for all
other instructions.

Ret. With control flow checks and memory write checks in place, we guarantee
that, when we reach a $\mathtt{ret}$ instruction, the logical call frame will
correspond to the “actual” call frame. $\mathtt{ret}$ is then responsible for
guaranteeing well-bracketing and ensuring callee-save registers are restored.
This is handled by two extra conditions on $\mathtt{ret}$ instructions:
$\operatorname{is-ret-addr}$ and $\operatorname{csr-restored}$.
$\operatorname{csr-restored}$ checks that callee-save registers have been
properly restored by comparing against the values that were saved in the
logical stack frame by $\mathtt{call}$. $\operatorname{is-ret-addr}$ checks
that the value pointed to by the stack pointer ($\mathit{ret\mbox{-}addr}$)
corresponds to the location of the return address saved in the logical stack
frame. Memory writes were checked to enforce that the return address cannot be
overwritten, so this guarantees the function will return to the expected
program location.

###  4.2. Overlay Semantics Enforce Security

The goal of the overlay semantics and our zero-cost conditions is to capture
the essential behavior necessary to ensure that individual, well-behaved
library functions can be composed together into a sandboxed library call that
enforces SFI integrity and confidentiality properties. Thus, library code that
is well-behaved under the dynamic overlay type system will behave equivalently
to library code with springboard and trampoline wrappers, and therefore well-
behaved library code can safely elide those wrappers and their overhead. We
prove that the overlay semantics is sound with respect to each of our security
properties:

###### Theorem 1 (Overlay Integrity Soundness).

If
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\in\mathit{Program}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\mathrel{\mathrel{\leadsto}^{n}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}\mathrel{\mathrel{\leadsto}^{\ast}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}$
such that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi\mathrel{\xrightarrow{\\!\text{wb}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi$
with
$\pi={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}.\Psi\mathrel{\mathrel{\rightarrow}^{n}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi$,
then  (1)
$\mathcal{CSR}(\pi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi)$and
(2)
$\mathcal{RA}(\pi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi)$.

###### Theorem 2 (Overlay Confidentiality Soundness).

If
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\in\mathit{Program}$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{lib}}$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}.\Psi\mathrel{\mathrel{\rightarrow}^{\ast}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}.\Psi\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{n}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}.\Psi\mathrel{\rightarrow}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}.\Psi$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}\mathrel{\mathrel{\leadsto}^{n+1}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}$,
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}}}=_{\mathtt{lib}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}^{\prime}}}$,
then
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}^{\prime}}}.\Psi\mathrel{\xrightarrow{\mathtt{lib}}\mathrel{\vphantom{\to}{}^{n}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}^{\prime}}}.\Psi\mathrel{\rightarrow}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}.\Psi$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{1}^{\prime}}}\mathrel{\mathrel{\leadsto}^{n+1}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}$
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}}\llparenthesis{\\_}\rrparenthesis_{\mathtt{app}}$,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}.pc={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}.pc$,
and  (1)
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}}\llparenthesis{\mathtt{gatecall}_{n^{\prime}}\
{e}}\rrparenthesis$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}^{\prime}}}}\llparenthesis{\mathtt{gatecall}_{n^{\prime}}\
{e}}\rrparenthesis$, and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}=_{\mathtt{call}\
n^{\prime}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}$
or  (2)
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}}}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$,
${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{2}^{\prime}}}}\llparenthesis{\mathtt{gateret}}\rrparenthesis$,
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}}}=_{\mathtt{ret}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{3}^{\prime}}}$.

##  5\. Instantiating Zero-Cost

We describe two isolation systems that securely support zero-cost transitions:
they meet the overlay monitor zero-cost conditions. The first (§5.1) is an SFI
system using WebAssembly as an IR before compiling to native code using the
Lucet toolchain (Bytecode Alliance, 2020a). Here we rely on the language-level
invariants of Wasm to satisfy our zero-cost requirements. To ensure that these
invariants are maintained, in Section 6 we describe a verifier, VeriZero, that
checks that compiled binaries meet the zero-cost conditions. In Section 6.1 we
outline our proof that the verifier guarantees that compiled Wasm can safely
elide springboards and trampolines.

The second system, SegmentZero32, is our novel SFI system combining the x86
segmented memory model for memory isolation with several security-hardening
LLVM compiler passes to enforce our zero-cost conditions. While WebAssembly
meets the zero-cost conditions, it imposes additional restrictions that lead
to unrelated slowdowns. SegmentZero32 thus serves as a platform for evaluating
the potential cost of enforcing the zero-cost conditions directly as well as a
proof-of-concept SFI implementation designed using the zero-cost framework.

###  5.1. WebAssembly

WebAssembly (Wasm) is a low-level bytecode with a sound, static type system.
Wasm’s abstract state includes global variables and heap memory, which are
zero-initialized at start-up. All heap accesses are explicitly bounds checked,
meaning that compiled Wasm programs inherently implement heap isolation.
Beyond this, Wasm programs enjoy several language-level properties, which
ensure compiled binaries satisfying the zero-cost conditions. We describe
these below.

Control flow. There are no arbitrary jump instructions in Wasm, only
structured intra-function control flow. Functions may only be entered through
a call instruction, and may only be exited by executing a return instruction.
Functions also have an associated type; direct calls are type-checked at
compile time while indirect calls are subject to a runtime type check. This
ensures that compiled Wasm meets our type-directed forward-edge CFI condition.

Protecting the stack. A Wasm function’s type precisely describes the space
required to allocate the function’s stack frame (including spilled registers).
All accesses to local variables and arguments are performed through statically
known offsets from the current stack base. It is therefore impossible for a
Wasm operation to access other stack frames or alter the saved return address.
This ensures that compiled Wasm meets our local state encapsulation condition,
and, in combination with type-checking function calls, guarantees that Wasm’s
control-flow is well-bracketed. We therefore know that compiled Wasm functions
will always execute the register-saving preamble and, upon termination, will
execute the register-restoring epilogue. Further, the function body will not
alter the values of any registers saved to the stack, thereby ensuring
restoration of callee-save registers.

Confidentiality. Wasm code may store values into function-local variables or a
function-local “value stack” similar to that of the Java Virtual Machine (jvm,
2019). The Wasm spec requires that compilers initialize function-local
variables either with a function argument or with a default value. Further,
accesses to the Wasm value stack are governed by a coarse-grained data-flow
type system, with explicit annotations at control flow joins. These are used
to check at compile-time that an instruction cannot pop a value from the stack
unless a corresponding value was pushed earlier in the same function. This
guarantees that local variable and value stack accesses can be compiled to
register accesses or accesses to a statically-known offset in the stack frame.

When executing a compiled Wasm function without heavyweight transitions,
confidential values from prior computations may linger in these spilled
registers or parts of the stack. However, the above checks ensure that these
locations will only be read if they have been previously overwritten during
execution of the same function by a low-confidentiality Wasm library value.

###  5.2. SegmentZero32

To demonstrate that zero-cost conditions can be applied outside of highly
structured languages such as Wasm, we demonstrate their enforcement in our
novel SFI system for C code called SegmentZero32. As we mention in §2.3, our
zero-cost conditions amalgamate a number of individual conditions which
separately have well-studied enforcement mechanisms, and so we are able to
compose a series of off-the-shelf Clang/LLVM security-hardening passes to form
the core of SegmentZero32. The memory bounds checks are performed using the
x86 segmented memory model (Intel, 2020) (Similar to NaCl (Yee et al., 2009),
however we use an additional segment to separate the sandboxed heap and
stack).

Since SegmentZero32 directly enforces the structure required for zero-cost
transitions on C code (rather than relying on Wasm as an IR), it allows us to
investigate the intrinsic cost of enforcing zero-cost (See Section 7.3),
without suffering from irrelevant Wasm overheads. We additionally compare
SegmentZero32 against NaCl’s 32-bit SFI scheme for the x86 architecture, which
we believe is the fastest production-quality SFI toolchain currently
available. Below we discuss specific details SegmentZero32 zero-cost condition
enforcement.

Protecting the stack. We apply the SafeStack (Kuznetsov et al., 2014; The LLVM
Foundation, 2021b) compiler pass to further split the sandboxed stack into a
safe and unsafe stack. The safe stack contains only data that the compiler can
statically verify is always accessed safely, e.g., return addresses, spilled
registers, and allocations that are only accessed locally using verifiably
safe offsets within the function that allocates them.777We also use LLVM’s
stack-heap clash detection (-fstack-clash-protection) to prevent the stack
growing into the heap. All other stack values are moved to the heap segment.
This ensures that pointer manipulation of unsafe stack references cannot be
used to corrupt the return address and saved context of the current call. We
write a small LLVM pass to add additional support for tracking whether an
access must be made through the heap segment or the stack segment, ensuring
correct code generation.

These transformations ensure that malicious code cannot programmatically
access anything stored in the stack segment, except through offsets statically
determined to be safe by the SafeStack pass. This protects the stored callee-
save registers and return address, guaranteeing the restoration of callee-save
registers and well-bracketing _iff forward control flow is enforced_.

Control flow. Fortunately, enforcing forward-edge CFI has been widely studied
(Burow et al., 2017). We use a CFI pass as implemented in Clang/LLVM (The LLVM
Foundation, 2021a; Tice et al., 2014) including flags to dynamically protect
indirect function calls, ensuring forward control flow integrity. Further,
SegmentZero32 conservatively bans non-local control flow (e.g. setjmp/longjmp)
in the C source code. A more permissive approach is possible, but we leave
this for future work.

Confidentiality. To guarantee confidentiality we implement a small change in
Clang to zero initialize all stack variables.888We can’t use Clang’s existing
pass for variable initialization (The LLVM Foundation, 2018) as it zero
initializes data on the unsafe stack leading to poor performance This ensures
that scratch registers cannot leak secrets as all sandbox values are
semantically written before use. In practice, many of these writes are
statically known to be dead and therefore optimised away.

##  6\. Verifying compiled WebAssembly

Instead of trusting the Wasm compiler, we build a _zero-cost verifier_ ,
VeriZero, to check that the native, compiled output meets the zero-cost
conditions and is thus safe to run without springboards and trampolines.
VeriZero is a static x86 assembly analyzer that takes as input potentially
untrusted native programs and verifies a series of local properties via
abstract interpretation. Together these local properties guarantee that the
monitor checks defined in oSFIasm are met; we discuss the proof of soundness
in Section 6.1.

VeriZero extends the VeriWasm SFI verifier (Johnson et al., 2021). Both
operate over WebAssembly modules compiled by the Lucet Wasm compiler (Bytecode
Alliance, 2020a), first disassembling the native x86 code before computing a
control-flow graph (CFG) for each function in the binary. The disassembled
code is then lifted to a subset of SFIasm, which serves as the first abstract
domain in our analysis. Unfortunately, the properties checked by VeriWasm,
while sufficient to guarantee SFI security, are insufficient to guarantee
zero-cost security. Below we will describe how VeriZero extends VeriWasm to
guarantee the stronger zero-cost conditions are met.

⬇

1bad_func: [] $\rightarrow$ rax good_func: [rdi] $\rightarrow$ rax

2 push r12 mov rax $\leftarrow$ rdi

3 ; TRACK: stack[0] = initial r12 value ret

4 mov r12 $\leftarrow$ 1

5 ; TRACK: r12 initialized

6 mov r11 $\leftarrow$ r13 + r12

7 ; TRACK: r11 uninitialized

8 mov rdi $\leftarrow$ 2

9 ; TRACK: rdi initialized

10 ; ASSERT: good_func arguments initialized

11 call good_func

12 ; TRACK: good_func return value initialized

13 pop r12

14 ; TRACK: r12 = initial r12 value

15 ; ASSERT: callee-save registers restored

16 gateret

Figure 6. Disassembled and lifted WebAssembly functions

The VeriZero analyzers. VeriZero adds two new analyses to VeriWasm. The first
extends VeriWasm’s CFI analysis, which only captures coarse grained control-
flow (i.e., that all calls target valid sandboxed functions), to also extract
type information. Extracting type information from the binary code is possible
without any complex type inference because Lucet leaves the type signatures in
the compiled output (though we do not need to trust Lucet to get these type
signatures correct since VeriZero would catch any deviations at the binary
level). For direct calls, VeriZero simply extracts the WebAssembly type stored
in the binary. For indirect calls we extend the VeriWasm indirect call
analysis to track the type of each indirect call table entry, enabling us to
resolve each indirect call to a statically known type. These types correspond
to the input registers and stack slots, and the output registers (if any) used
by a function. For example, in Figure 6 bad_func takes no input and outputs to
rax and good_func takes rdi as input and outputs to rax.

The second analysis tracks dataflow in local variables, i.e., in registers and
stack slots. Continuing with bad_func as our example this analysis captures
that: in Line 2 stack slot 0 now holds the initial value of r12, in Line 4 r12
holds an initialized (and therefore public) value, in Line 6 r13 has not been
initialized and therefore potentially contains confidential data so r11 may
also contain confidential data, etc. This analysis is used to check
confidentiality, callee-save register restoration, local state encapsulation,
and is combined with the previous analysis to check type-directed CFI.

The dataflow abstract domain. To track local variable dataflow, VeriZero uses
an abstract domain with three elements: $\mathtt{Uninitialized}$ which
represents an uninitialized, potentially confidential value;
$\mathtt{Initialized}$ which represents an initialized, public value; and
$\mathtt{UninitializedCallee}({r})$ which represents a potentially
confidential value which corresponds to the original value of the callee-save
register $r$. The domain forms a meet-semilattice with
$\mathtt{Uninitialized}$ the least element and all other elements
incomparable.

From here, analysis is straightforward, with a function’s argument registers
and stack slots initialized to $\mathtt{Initialized}$, each callee-save
register $r$ initialized to $\mathtt{UninitializedCallee}({r})$, and
everything else $\mathtt{Uninitialized}$. Instructions are interpreted as
expected, e.g., $\mathtt{mov}$ simply copies the abstract value of its source
into the target, operations return the meet of their operands, and all
constants and reads from the heap are treated as initialized. Across calls we
assume that callee-save register conventions are followed (as we will be
checking this), preserving the value of all callee-save registers and clearing
all other registers’ values. We extract the type information from the extended
CFI analysis to determine the return register that is initialized after a
function call.

Checking the zero-cost conditions. The above two analyses, along with
additional information from VeriWasm’s existing analyses enable us to check
the zero-cost conditions.

  1. (1)

_Callee-save register restoration:_ The $\mathtt{UninitializedCallee}({r})$
value enables straightforward checking that callee-save registers have been
restored by checking that, at each $\mathtt{ret}$ instruction, each callee-
save register $r$ has the abstract value $\mathtt{UninitializedCallee}({r})$.

  2. (2)

_Well-bracketed control-flow:_ VeriWasm already implements a stack checker
that guarantees that all writes to the stack are to local variables, ensuring
that the saved return address on the stack cannot be tampered with. Further,
it checks that the stack pointer is restored to its original location at the
end of every function, ensuring the saved return address is used.

  3. (3)

_Type-directed forward-edge CFI:_ The dataflow analysis gives us the registers
that are initialized when we reach a $\mathtt{call}$ instruction, enabling us
to check that the input arguments of the target have been initialized. For
example, when we reach Line 11 we know that rdi has the value
$\mathtt{Initialized}$. The type-based CFI analysis tells us that good_func
expects rdi as an input, so this call is marked as safe.

  4. (4)

_Local state encapsulation:_ To ensure SFI security, VeriWasm checks that no
writes are below the current stack frame, ensuring that verified Wasm
functions cannot tamper with other frames.

  5. (5)

_Confidentiality:_ We check confidentiality using the information obtained in
our dataflow analysis, where the value $\mathtt{Initialized}$ ensures that a
value is initialized with a public, non-confidential value. This enables us to
check each of the confidentiality checks encoded in oSFIasm are met: for
instance the type-safe forward-edge CFI check described above already ensures
each argument is initialized. In Figure 6, the confidentiality checker will
flag Line 6 as unsafe because r13 still has the value
$\mathtt{UninitializedCallee}({\mathtt{r13}})$, which potentially contains
confidential information leaked from the application.

###  6.1. Proving Wasm secure

We prove that compiled and verified Wasm libraries can safely elide
springboards and trampolines while maintaining integrity and confidentiality,
by showing that the verified code would not violate the safety monitor.
Formally, this amounts to showing that Wasm code verified by VeriZero never
reaches an
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$
state. This allows us to apply Theorem 1 and Theorem 2. It is relatively
straightforward (with one exception) to prove that the abstract interpretation
as described guarantees the necessary safety conditions.

The crucial exception in the soundness proof is when a function calls to other
Wasm functions. We must inductively assume that the called function is safe,
i.e., doesn’t change any variables in our stack frame, restores callee-save
registers, etc. Unfortunately, a naive attempt does not lead to an inductively
well-founded argument. Instead, we use the overlay monitor’s notion of a well-
behaved function to define a step-indexed logical relation (detailed in
Appendix D.1) that captures a semantic notion of well-behaved functions (as a
relation $\mathcal{F}$), and then lift this to a relation over an entire Wasm
library (as a relation $\mathcal{L}$). This gives a basis for an inductively
well-founded argument where we can prove that, locally, the abstract
interpretation gives that each Wasm function is semantically well-behaved (is
in $\mathcal{F}$) and then use this to prove the standard fundamental theorem
of a logical relation for a whole Wasm library:

###### Theorem 1 (Fundamental Theorem for Wasm Libraries).

For any number of steps $n\in\mathbb{N}$ and compiled Wasm library $L$,
$(n,L)\in\mathcal{L}$.

This theorem states that every function in a compiled Wasm library, when
making calls to other Wasm functions or application callbacks, is well-behaved
with respect to the zero-cost conditions. The number of steps is a technical
detail related to step-indexing. Zero-cost security then follows by adequacy
of the logical relation, Theorem 1, and Theorem 2:

###### Theorem 2 (Adequacy of Wasm Logical Relation).

For any number of steps $n\in\mathbb{N}$, library $L$ such that
$(n,L)\in\mathcal{L}$, program
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\in\mathit{Program}$
using $L$, and $n^{\prime}\leq n$, if
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi_{0}}}\mathrel{\mathrel{\leadsto}^{n^{\prime}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}$
then
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\Phi^{\prime}}}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{oerror}}}$.

Details of the logical relation and proofs are in Appendix D.

##  7\. Evaluation

We evaluate our zero-cost model by asking four questions:

  * $\blacktriangleright$

Q1: What is the cost of a context switch? (§7.1)

  * $\blacktriangleright$

Q2: What is end-to-end performance gain of Wasm-based SFI due to zero-cost
transitions? (§7.2)

  * $\blacktriangleright$

Q3: What is the performance overhead of purpose-built zero-cost SFI
enforcement? (§7.3)

  * $\blacktriangleright$

Q4: Is the VeriZero verifier effective? (§7.4)

Since our zero-cost condition enforcement does incur some runtime overhead, Q2
and Q3 are heavily workload-dependent. The benefit a workload receives from
the zero-cost approach will be in direct proportion to the frequency with
which it performs domain transitions.

Systems. To investigate the first three questions, we consider two groups of
SFI systems. The first group compares a number of different transition models
for Wasm-based SFI for 64-bit binaries, built on top of the Lucet compiler
(Bytecode Alliance, 2020a). All of these will have identical runtime overhead,
meaning that the only variance between them will be due to transition
overhead. The WasmLucet build uses the original heavyweight springboards and
trampolines shipped with the Lucet runtime written in Rust. WasmHeavy adopts
techniques from NaCl and uses optimized assembly to save and restore
application context during transitions. WasmZero implements our zero-cost
transition system, meaning transitions are simple function calls. To
understand the overhead of register saving/restoring and stack switching, we
also evaluate a WasmReg build which saves/restores registers like WasmHeavy,
but shares the library and application stack like WasmZero.

The second group compares optimized SFI techniques for 32-bit binaries. Wasm-
based SFI imposes overheads far beyond what is strictly necessary to enforce
our zero-cost conditions, both because of the immaturity of the Lucet compiler
in comparison to more established compilers such as Clang, and because Wasm
inherently enforces additional restrictions on compiled code (e.g., structured
intra-function control flow). We design SegmentZero32 (§5.2) to enforce only
our zero-cost-conditions and nothing more, aiming to benchmark it against the
Native Client 32-bit isolation scheme (NaCl32) (Yee et al., 2009), arguably
the fastest production SFI system available, which requires heavyweight
transitions. Both systems make use of memory segmentation, a 32-bit x86-only
feature for fast memory isolation. Unfortunately, we cannot make a uniform
comparison between NaCl32, SegmentZero32, and WasmZero since Lucet only
supports a 64-bit target.

Each group additionally uses unsandboxed, insecure native execution (Vanilla)
as a baseline. To represent the best possible performance of schemes relying
on heavyweight transitions, we also benchmark IdealHeavy32 and IdealHeavy64,
ideal hardware isolation schemes, which incur no runtime overhead but require
heavyweight transitions. To simulate the performance of these ideal schemes,
we simply measure the performance of native code with heavyweight trampolines.

We integrate all of the above SFI schemes into Firefox using the RLBox
framework (Narayan et al., 2020). Since RLBox already provides plugins for the
WasmLucet and NaCl32 builds, we only implement the plugins for the remaining
system builds.

Benchmarks. We use a micro-benchmark to evaluate the cost of a single
transition for our different transition models, using unsandboxed native calls
as a baseline (Q1).

We answer questions Q2–Q3 by measuring the end-to-end performance of font and
image rendering in Firefox, using a sandboxed libgraphite and libjpeg,
respectively. We use these libraries because they have many cross-sandbox
transitions, which Narayan et al. (2020) previously observed to affect the
overall browser performance. To evaluate the performance of libgraphite, we
use Kew’s benchmark999Available at
https://jfkthame.github.io/test/udhr_urd.html, which reflows the text on a
page ten times, adjusting the size of the fonts each time to negate the
effects of font caches. When calling libgraphite, Firefox makes a number of
calls into the sandbox roughly proportional to the number of glyphs on the
page. We run this benchmark 100 times and report the median execution time
below (all values have standard deviations within 1%).

To evaluate the performance of libjpeg, we measure the overhead of rendering
images of varying complexity and size. Since the work done by the sandboxed
libjpeg, per call, is proportional to the width of the image— Firefox executes
the library in _streaming mode_ , one row at a time— we consider images of
different widths, keeping the image height fixed. This allows us to understand
the benefits and limitations of zero-cost transitions, since the proportion of
execution time spent context-switching decreases as the image width increases.
We do this for three images, of varying complexity: a simple image consisting
of a single color (SimpleImage), a stock image from the Image Compression
benchmark suite101010Online: https://imagecompression.info/test_images/.
Visited Dec 9, 2020. (StockImage), and an image of random pixels
(RandomImage). We render each image 500 times and report the median time
(standard deviations are all under 1%).

Finally, we use SPEC CPU® 2006 to partly evaluate the sandboxing overhead of
our purpose-built SegmentZero32 SFI system (Q3), and to measure VeriZero’s
verification speed (Q4).

Machine and software setup. We run all but the verification benchmarks on an
Intel® CoreTM i7-6700K machine with four 4GHz cores, 64GB RAM, running Ubuntu
20.04.1 LTS (kernel version 5.4.0-58). We run benchmarks with a shielded
isolated cpuset (Tsariounov, 2021) consisting of one core with hyperthreading
disabled and the clock frequency pinned to 2.2GHz. We generate Wasm sandboxed
code in two steps: First, we compile C/C++ to Wasm using Clang-11, and then
compile Wasm to native code using the fork of the Lucet used by RLBox
(snapshot from Dec 9, 2020). We generate NaCl sandboxed code using a modified
version of Clang-4. We compile all other C/C++ source code, including
SegmentZero32 sandboxed code and benchmarks using Clang-11. We implement our
Firefox benchmarks on top of Firefox Nightly (from August 22, 2020).

Summary of results. We find that the performance of Wasm-based isolation can
be significantly improved by adopting zero-cost transitions, but that Lucet-
compiled WebAssembly’s runtime overhead means that it does not outperform more
optimised isolation schemes in end-to-end tests. The low performance overhead
of SegmentZero32 demonstrates that these runtime overheads are not inherent to
the zero-cost approach, and that an optimised zero-cost SFI system can
significantly outperform more traditional schemes, especially for workloads
with a large number of transitions. Finally, we find that we can efficiently
check zero-cost conditions at the binary level, for Lucet compiled code, with
no false positives.

Build | Direct call | Indirect call | Callback | Syscall
---|---|---|---|---
Vanilla (in C) | 1ns | 56ns | 56ns | 24ns
WasmLucet | — | 1137ns | — | —
WasmHeavy | 120ns | 209ns | 172ns | 192ns
WasmReg | 120ns | 210ns | 172ns | 192ns
WasmZero | 7ns | 66ns | 67ns | 60ns
Vanilla (in C, 32-bit) | 1ns | 74ns | 74ns | 37ns
NaCl32 | — | 714ns | 373ns | 356ns
SegmentZero32 | 24ns | 108ns | 80ns | 88ns
Figure 7.  Costs of transitions in different isolation models. Zero-cost
transitions are shown in boldface. Vanilla is the performance of an
unsandboxed C function call, to serve as a baseline.

###  7.1. The cost of transitions

We measure the cost of different cross-domain transitions— direct and indirect
calls into the sandbox, callbacks from the sandbox, and syscall invocations
from the sandbox— for the different system builds described above. To expose
overheads fully, we choose extremely fast payloads—either a function that just
adds two numbers or the gettimeofday syscall, which relies on Linux’s vDSO to
avoid CPU ring changes. The results are shown in Figure 7. All numbers are
averages of one million repetitions, and repeated runs have negligible
standard deviation.111111 Lucet and NaCl don’t support direct sandbox calls;
Lucet further does not support custom callbacks or syscall invocations.

We make several observations. First, among Wasm-based SFI schemes, zero-cost
transitions (WasmZero) are significantly faster than even optimized
heavyweight transitions (WasmHeavy). Lucet’s existing indirect calls written
in Rust (WasmLucet) are significantly slower than both. Second, the cost of
stack switching (the difference of WasmHeavy and WasmReg) is surprisingly
negligible. Third, the performance of Vanilla and WasmZero should be identical
but is not. This is _not_ because our transitions have a hidden cost. Rather,
it’s because we are comparing code produced by two different compilers:
Vanilla is native code produced by Clang, while WasmZero is code produced by
Lucet, and Lucet’s code generation is not yet highly optimized (Hansen, 2019).
For example, in the benchmark that adds two numbers, Clang eliminates the
function prologue and epilogue that save and restore the frame pointer, while
Lucet does not. We observe similar trends for hardware-based isolation. For
example, we find that SegmentZero32 transitions are much faster than
IdealHeavy32 and NaCl32 transitions and only 23ns slower than Vanilla for
direct calls. Finally, we observe that SegmentZero32 is slower than WasmZero:
hardware isolation schemes like SegmentZero32 and NaCl32 execute instructions
to enable or disable the hardware based memory isolation in their transitions.

###  7.2. End-to-end performance improvements of zero-cost transitions for
Wasm

(a) SimpleImage

(b) StockImage

(c) RandomImage

Figure 8.  Performance of different Wasm transitions on rendering of (a) a
simple image with one color, (b) a stock image, and (c) a complex image with
random pixels, normalized to WasmZero. WasmZero transitions outperform other
transitions. The difference diminishes with width, but narrower images are
more common on the web.

We evaluate the end-to-end performance impact of the different transition
models on Wasm-sandboxed font and image rendering as used in Firefox (see §7).

Font rendering. We report the performance of libgraphite isolated with Wasm-
based schemes on Kew’s benchmark below:

|  WasmLucet |  WasmHeavy |  WasmReg |  WasmZero |  Vanilla |  IdealHeavy64
---|---|---|---|---|---|---
Font render |  8173ms |  2246ms |  2230ms |  2032ms |  1116ms |  1563ms

As expected, Wasm with zero-cost transitions (WasmZero) outperforms the other
Wasm-based SFI transition models. Compared to WasmZero, Lucet’s existing
transitions slow down rendering by over 4$\times$.121212 This overhead is
smaller than the 8$\times$ overhead reported by Narayan et al. (2020); we
attribute this difference to the different compilers— we use a more recent,
and faster, version of Lucet.  But, even the optimized heavyweight transitions
(WasmHeavy) impose a 10% performance tax. This overhead is due to register
saving/restoring; stack switching only accounts for 0.8% overhead.

While these results show that existing Wasm-based isolation schemes can
benefit from switching to zero-cost transitions— and indeed the speed-up due
to zero-cost transitions allowed Mozilla to ship the Wasm-sandboxed
libgraphite — they also show that Lucet-compiled Wasm is slow ($\sim$80$\%$
slower than Vanilla). This, unfortunately, means that the transition cost
savings alone are not enough to beat IdealHeavy64, even for a workload with
many transitions. To compete with this ideal SFI scheme with heavyweight
transitions, we would need to reduce the runtime overhead to $\sim$40$\%$.
Jangda et al. (2019) report the average runtime overhead of Mozilla
SpiderMonkey JIT-compiled WebAssembly compared to native as $\sim$45$\%$ in a
different set of benchmarks, while noting many correctable inefficiencies in
the generated assembly code, suggesting that there is a lot of room for Lucet
to be further optimised.

Image rendering. Figure 8 report the overhead of Wasm-based sandboxing on
image rendering, normalized to WasmZero to highlight the relative overheads of
different transitions as compared to our zero-cost transitions. We report
results of WasmLucet separately, in Appendix E (Figure 28) because the
rendering times are up to 9.2$\times$ longer than the other builds. Here, we
instead focus on evaluating the overheads of optimized heavy transitions.

As expected, WasmZero significantly outperforms other transitions when images
are narrower and simpler. On SimpleImage, WasmHeavy and WasmLucet can take as
much as 29.7% and 9.2$\times$ longer to render the image as with WasmZero
transitions. However, this performance gap diminishes as image width increases
(and the relative cost of context switching decreases). For StockImage and
RandomImage, the WasmHeavy trends are similar, but the rendering time
differences start at about 4.5%. Lucet’s existing transitions (WasmLucet) are
still significantly slower than zero-cost transitions (WasmZero) even on wide
images.

Figure 9.  Cumulative distribution of image widths on the landing pages of the
Alexa top 500 websites. Over 80% of the images have widths under 480 pixels.
Narrower images have a higher transition rate, and thus higher relative
overheads when using expensive transitions.

Though the differences between the transitions are smaller as the image width
increases, many images on the Web are narrow. Figure 9 shows the distribution
of images on the landing pages of the Alexa top 500 websites. Of the 10.6K
images, 8.6K (over 80%) have widths between 1 and 480 pixels, a range in which
zero-cost transitions noticeably outperform the other kinds of transitions.

Like font rendering, we measure the target runtime overhead Lucet should
achieve to beat IdealHeavy64 end-to-end for rendering images. We report our
results in Figure 29 in Appendix E. For the small simple image, we observe
this to be 94%— this is approximately the overhead of Lucet that we see
already today. For the small stock image, we observe this to be 15%— this is
much smaller than the overhead of Lucet today, but lower overheads have been
demonstrated on some benchmarks by the prototype Wasm compiler of Gadepalli et
al. (2020).

###  7.3. Performance overhead of purpose-built zero-cost SFI enforcement

(a) SimpleImage

(b) StockImage

(c) RandomImage

Figure 10.  Performance of image rendering with libjpeg sandboxed with
SegmentZero32 and NaCl32 and IdealHeavy32. Times are relative to unsandboxed
code. NaCl32 and IdealHeavy32 relative overheads are as high as 312% and 208%
respectively, while SegmentZero32 relative overheads do not exceed 24%.

In this section, we measure the performance overhead of SegmentZero32 with
zero-cost transitions. We compare SegmentZero32 with NaCl (NaCl32) and
IdealHeavy32— a hypothetical SFI scheme with no isolation enforcement
overhead, both of which rely on heavyweight transitions. We measure the
overhead of these systems on the standard SPEC CPU® 2006 benchmark suite, and
the libgraphite and libjpeg font and image rendering benchmarks. Since both
SegmentZero32 and NaCl32 use segmentation which is supported only in 32-bit
mode, we implement these three isolation builds in 32-bit mode and compare it
to native 32-bit unsandboxed code. We describe these benchmarks next.

SPEC. We report the impact of sandboxing on SPEC CPU® 2006 in Figure 11.
Several benchmarks are not compatible with NaCl32; augmenting NaCl32 runtime
and libraries to fix such compatibility issues (e.g., as done in (Yee et al.,
2009) for SPEC2000) is beyond the scope of this paper. The gcc benchmark, on
the other hand, is not compatible with SegmentZero32— gcc fails (at runtime)
because the CFI used by SegmentZero32 — Clang’s CFI— incorrectly computes a
target CFI label. Clang’s CFI implementation is more precise than necessary
for our zero-cost conditions; as with NaCl32, we leave the implementation of a
coarse-grain and more permissive CFI to future work. On the overlapping
benchmarks, SegmentZero32’s overhead is comparable to NaCl32’s.

System 400.perlbench 401.bzip2 403.gcc 429.mcf 445.gobmk 456.hmmer 458.sjeng
462.libquantum 464.h264ref 471.omnetpp 473.astar 483.xalancbmk NaCl32 — —
1.10$\times$ — 1.27$\times$ 0.97$\times$ 1.20$\times$ 1.06$\times$
1.34$\times$ 1.06$\times$ 1.31$\times$ — SegmentZero32 1.20$\times$
1.08$\times$ — 1.04$\times$ 1.25$\times$ 0.82$\times$ 1.16$\times$
1.02$\times$ 1.01$\times$ 1.01$\times$ 1.10$\times$ 1.05$\times$

Figure 11. Overheads compared to native code on SPEC CPU® 2006 (nc), for
NaCl32 and SegmentZero32.

Font rendering. The impact of these isolation schemes on font rendering is
shown below:

| Vanilla (32-bit) | IdealHeavy32 | NaCl32 | SegmentZero32
---|---|---|---|---
Font render | 1441ms | 2399ms | 2769ms | 1765ms

We observe that NaCl32 and IdealHeavy32 impose an overhead of 92% and 66%
respectively. In contrast, SegmentZero32 has a smaller overhead (22.5%) as it
does not have to save and restore registers or switch stacks. We attribute the
overhead of SegmentZero32 (over Vanilla) to three factors: (1) changing
segments to enable/disable isolation during function calls, (2) using indirect
function calls for cross-domain calls (a choice that simplifies engineering
but is not fundamental), and (3) the structure imposed by our zero-cost
condition enforcement.

Image rendering. We report the impact of sandboxing on image rendering in
Figure 10. For narrow images (10 pixel width), SegmentZero32 overheads
relative to the native unsandboxed code are 24%, 1%, and 6.5% for SimpleImage,
StockImage and RandomImage, respectively. These overheads are lower than the
corresponding overheads for NaCl32 (312%, 29%, and 66%) as well as
IdealHeavy32 (208%, 28% and 45%). As in the Wasm measurements, these overheads
shrink as image width increases and the complexity of the image increases
(e.g., the overheads for images wider than 480 pixels are negligible).

###  7.4. Effectiveness of the VeriZero verifier

We evaluate VeriZero’s effectiveness by using it to (1) verify 13 binaries—
five third-party libraries shipping (or about to ship) with Firefox compiled
across 3 binaries, and 10 binaries from the SPEC CPU® 2006 benchmarks— and (2)
find nine manually introduced bugs, inspired by real calling convention bugs
in previous SFI toolchains (Rydgard, 2020; Nacl Issue 775, 2010; Nacl Issue
2919, 2012). We measure VeriZero’s performance verifying the aforementioned 13
binaries. Finally, we stress test VeriZero by running it on random binaries
generated by Csmith (Yang et al., 2011).

Experimental setup. We run all VeriZero experiments on a 2.1GHz Intel® Xeon®
Platinum 8160 machine with 96 cores and 1 TB of RAM running Arch Linux
5.11.12. All experiments run on a single core and use no more than 2GB of RAM.
We compile the SPEC binaries used using the Lucet toolkit used in Section 7.2.
We verify three of the Firefox libraries from Firefox Nightly; we compile the
other two from the patches that are in the process of being integrated into
Firefox.

Effectiveness and performance results. VeriZero successfully verifies the 13
Firefox and SPEC CPU® 2006 binaries. These binaries vary in size from 150
functions (the lbm benchmark from SPEC CPU® 2006) to 4094 functions (the
binary consisting of the Firefox Nightly libraries libogg, libgraphite, and
hunspell). It took VeriZero between 1.77 seconds and 19.28 seconds to verify
these binaries, with an average of 9.2 seconds and median of 5.93 seconds.
VeriZero’s performance is on par with the original VeriWasm’s performance: on
the 10 SPEC CPU® 2006 benchmarks evaluated in the VeriWasm paper (Johnson et
al., 2021) VeriZero is slightly (15%) faster, despite checking zero-cost
conditions in addition to all of VeriWasm’s original checks. This is due to
various engineering improvements that were made to VeriWasm in the course of
developing VeriZero.

VeriZero also successfully found bugs injected into nine binaries. These bugs
tested all the zero-cost properties that VeriZero was designed to check, and
when possible they were based on real bugs (like those in Cranelift (Rydgard,
2020)). VeriZero successfully detected all nine of these bugs, giving us
confidence that VeriZero is capable of finding violations of the zero-cost
conditions.

Fuzzing results. We fuzzed VeriZero to both search for potential bugs in
Lucet, as well as to ensure VeriZero does not incorrectly declare safe
programs unsafe. The fuzzing pipeline works in four stages: first, we use
Csmith (Yang et al., 2011) to generate random C and C++ programs, next we use
Clang to compile the generated C/C++ program to WebAssembly, followed by
compiling the Wasm file to native code using Lucet, and finally we verify the
generated binary with VeriZero. As these programs were compiled by Lucet, we
expect them to adhere to the zero-cost conditions, and any binaries flagged by
VeriZero are either bugs in Lucet or are spurious errors in VeriZero.

While we did not find bugs in Lucet, fuzzing did find cases where VeriZero
triggered spurious errors. After fixing these errors, we verified 100,000
randomly generated programs with no false positives.

##  8\. Limitations

Our Wasm SFI scheme is capable of sandboxing any C/C++-like language (with
arbitrary intra-function control flow, arbitrary type casting, arbitrary
pointer aliasing, arithmetic etc.) that can compile to Wasm, so long as it
does not use features which Wasm must emulate through JavaScript131313See
https://emscripten.org/— most prominently C++-style exceptions,
setjmp/longjmp, and multithreading. These limitations are not inherent to our
zero-cost conditions, and Wasm is in the process of being extended with
support for all of the above features (Watt et al., 2019; WebAssembly
Community Group, 2021).

Our SegmentZero32 scheme is built as a proof-of-concept, using mostly existing
LLVM passes to sandbox C programs compiled to 32-bit x86, as an approach to
understanding the overhead of zero-cost conditions on native code. As such,
our SegmentZero32 implementation does not support, for instance,
setjmp/longjmp or multithreading (similar to Wasm). In addition it does not
support user-defined variadic function arguments or position independent code.
However, these are engineering limitations and not fundamental. For example,
user-defined variadic function arguments could be supported by extending the
SafeStack LLVM pass to move the variadic argument buffer into the unsafe
stack, and position independent code could be supported through minor
generalisations of existing compiler primitives.

Both Wasm and SegmentZero32 rely on a type-directed forward-edge CFI which
requires us to statically infer a limited amount of information about
arguments to functions.141414We do not need to infer any information about the
heap or unsafe stack. Variadic functions, for example, can pass a dynamic
number of arguments on the unsafe stack. This information includes the number
of arguments, their width, and the calling convention. In practice, this
information is readily available as part of compilation and does not require
any complex control flow inference (unlike more precise fine grain CFI
schemes), so this is only a limitation when analyzing certain binary programs.
Like most SFI schemes, both Wasm and our SegmentZero32 do not currently
support JIT code compilation within the isolated component; adding this would
require engineering work, but can be done following the approaches of (Ansel
et al., 2011; Vahldiek-Oberwagner et al., 2019). Finally, side channels are
out of scope for this paper.

##  9\. Related work

A considerable amount of research has gone into efficient implementations of
memory isolation and CFI techniques to provide SFI across many platforms (Sehr
et al., 2010; McCamant and Morrisett, 2006; Goonasekera et al., 2015; Bytecode
Alliance, 2020a; Lucco et al., 1995; Adl-Tabatabai et al., 1996; Seltzer et
al., 1996; Herder et al., 2009; Niu and Tan, 2014; Siefers et al., 2010; Ford
and Cox, 2008; Tan et al., 2017; Payer and Gross, 2011; Bittau et al., 2008;
Litton et al., 2016; Chen et al., 2016; Castro et al., 2009). However, these
systems either implement or require the user to implement heavyweight
springboards and trampolines to guarantee security.

SFI systems. Wahbe et al. (1993) suggest two ways to optimize transitions: (1)
partitioning the registers used by the application and the sandboxed component
and (2) performing link time optimizations (LTO) that conservatively
eliminates register saves that are never used in the entire sandboxed
component (not just the callee). Register partitioning would cause slowdowns
due to increased spilling. Native Client (Yee et al., 2009) optimized
transitions by clearing and saving contexts using machine specific mechanisms
to, e.g., clear floating point state and SIMD registers in bulk. However, we
show (§7) that, even with those optimizations, the software model imposes
significant transition overheads. While CPU makers continue to add optimized
context switching instructions, such instructions do not yet eliminate all
overhead.

Zeng et al. (2011) combine an SFI scheme with a rich CFI scheme enforcing
structure on executing code. While a similar approach, their goal is to safely
perform optimizations to elide SFI and CFI bounds checks, and they do not
impose sufficient structure to enforce well-bracketing, a necessary property
for zero-cost transitions. XFI (Erlingsson et al., 2006) also combines an SFI
scheme with a rich CFI scheme and adopts a safe stack model. While meeting
many of the zero-cost conditions, it does not prevent reading uninitialized
scratch registers and therefore cannot ensure confidentiality without
heavyweight springboards that clear scratch registers. They also do not
specify the CFG granularity, so it is not clear if is strong enough to satisfy
the zero-cost type-safe CFI requirement.

WebAssembly based isolation. WasmBoxC (Zakai, 2020) sandboxes C code by
compiling to Wasm followed by (de)compiling back to C, ensuring that the
sandboxed code will inherit isolation properties from Wasm. The sandboxed
library code can be safely linked with C applications, enabling a form of
zero-cost transition. The zero-cost Wasm SFI system described by this paper
was designed and released prior to and independently of WasmBoxC, as the
creators of WasmBoxC acknowledge (citation elided for DBR). Moreover, we
believe that the theory developed in this paper provides a foundation for
analyzing and proving the security of WasmBoxC though such analysis would need
to account for possible undefined behavior introduced in compiling to C.

Sledge (Gadepalli et al., 2020) describes a Wasm runtime for edge computing,
that relies on Wasm properties to enable efficient isolation of serverless
components. However, Sledge focuses on function scheduling including
preempting running Wasm programs, so its needs for context saving differ from
library sandboxing as contexts must be saved even in the middle of function
calls.

SFI Verification. Previous work on SFI (e.g., (McCamant and Morrisett, 2006;
Yee et al., 2009; Erlingsson et al., 2006; Johnson et al., 2021)) uses a
_verifier_ or a theorem prover (Zhao et al., 2011; Kroll et al., 2014) to
validate the relevant SFI properties of compiled sandbox code. However, unlike
VeriZero, none of these verifiers establish sufficient properties for zero-
cost transitions.

Hardware based isolation. Hardware features such as memory protection keys
(Vahldiek-Oberwagner et al., 2019; Hedayati et al., 2019), extended page
tables (Qiang et al., 2017), virtualization instructions (Qiang et al., 2017;
Belay et al., 2012), or even dedicated hardware designs (Schrammel et al.,
2020) can be used to speed up memory isolation. These works focus on the
efficiency of memory isolation as well as switching between protected memory
domains; however these approaches also use a single memory region that contain
both the stack and heap making them incompatible with zero-cost conditions,
i.e. they require heavyweight transitions. IdealHeavy32 and IdealHeavy64 in
Section 7 studies an idealized version of such a scheme.

Capabilities. Karger (1989) and Skorstengaard et al. (2019) look at protecting
interacting components on systems that provide hardware-enforced capabilities.
Karger (1989) specifically looks at how register saving and restoration can be
optimized based on different levels of trust between components, however their
analysis does not offer formal security guarantees. Skorstengaard et al.
(2019) investigate a calling-convention based on capabilities (à la CHERI
(Watson et al., 2015)) that allow safe sharing of a stack between distrusting
components. Their definition of well-bracketed control flow and local state
encapsulation via an overlay inspired our work, and our logical relation is
also based on their work. However, their technique does not yet ensure an
equivalent notion to our confidentiality property, and further is tied to
machine support for hardware capabilities.

Type safety for isolation. There has also been work on using strongly-typed
languages to provide similar security benefits. SingularityOS (Aiken et al.,
2006; Hunt and Larus, 2007; Fähndrich et al., 2006), explored using Sing# to
build an OS with cheap transitions between mutually untrusting processes.
Unlike the work on SFI techniques that zero-cost transitions extend, tools
like SingularityOS require engineering effort to rewrite unsafe components in
new safe languages.

At a lower level, Typed Assembly Language (TAL) (Morrisett et al., 1999b,
2002; Morrisett et al., 1999a) is a type-safe compilation target for high-
level type-safe languages. Its type system enables proofs that assembly
programs follow calling conventions, and enables an elegant definition of
stack safety through polymorphism. Unfortunately, SFI is designed with unsafe
code in mind, so cannot generally be compiled to meet TAL’s static checks. To
handle this our zero-cost and security conditions instead capture the
_behavior_ that TAL’s type system is designed to ensure.

###### Acknowledgements.

We thank the reviewers for their suggestions and insightful comments. Many
thanks to Bobby Holley, Mike Hommey, Chris Fallin, Tom Ritter, Till
Schneidereit, Andy Wortman, and Alon Zakai for fruitful discussions. We thank
Chris Fallin, Pat Hickey, and Andy Wortman for working with us to integrate
VeriZero into the Lucet compiler. This work was supported in part by gifts
from Cisco, Fastly, Google, and Intel; by the NSF under Grant Number
CNS-1514435, CNS-2120642, CCF-1918573, CAREER CNS-2048262; and, by the CONIX
Research Center, one of six centers in JUMP, a Semiconductor Research
Corporation (SRC) program sponsored by DARPA. Conrad Watt was supported by the
EPSRC grant REMS: Rigorous Engineering for Mainstream Systems (EP/K008528/1),
a Google PhD Fellowship in Programming Technology and Software Engineering,
and a Research Fellowship from Peterhouse, University of Cambridge.

## References

  * (1)
  * jvm (2019) 2019\.  _Java Platform, Standard Edition: Java Virtual Machine Guide_.  Technical Report.  https://docs.oracle.com/en/java/javase/13/vm/java-virtual-machine-guide.pdf
  * Adl-Tabatabai et al. (1996) Ali-Reza Adl-Tabatabai, Geoff Langdale, Steven Lucco, and Robert Wahbe. 1996.  Efficient and language-independent mobile programs. In _Proceedings of the ACM SIGPLAN’96 Conference on Programming Language Design and Implementation (PLDI), Philadephia, Pennsylvania, USA, May 21-24, 1996_. ACM.  https://doi.org/10.1145/231379.231402
  * Aiken et al. (2006) Mark Aiken, Manuel Fähndrich, Chris Hawblitzel, Galen Hunt, and James Larus. 2006.  Deconstructing process isolation. In _Proceedings of the 2006 workshop on Memory System Performance and Correctness, San Jose, California, USA, October 11, 2006_. ACM.  https://doi.org/10.1145/1178597.1178599
  * Alder et al. (2020) Fritz Alder, Jo Van Bulck, David Oswald, and Frank Piessens. 2020.  Faulty Point Unit: ABI Poisoning Attacks on Intel SGX. In _ACSAC ’20: Annual Computer Security Applications Conference, Virtual Event / Austin, TX, USA, 7-11 December, 2020_. ACM.  https://doi.org/10.1145/3427228.3427270