11institutetext:  Carnegie Mellon University 22institutetext: Inria
Paris33institutetext: University of Pennsylvania

# The Meaning of Memory Safety

Arthur Azevedo de Amorim 11 Cătălin Hritcu 22 Benjamin C. Pierce 33

###### Abstract

We give a rigorous characterization of what it means for a programming
language to be memory safe, capturing the intuition that memory safety
supports local reasoning about state. We formalize this principle in two ways.
First, we show how a small memory-safe language validates a noninterference
property: a program can neither affect nor be affected by unreachable parts of
the state. Second, we extend separation logic, a proof system for heap-
manipulating programs, with a “memory-safe variant” of its frame rule. The new
rule is stronger because it applies even when parts of the program are buggy
or malicious, but also weaker because it demands a stricter form of separation
between parts of the program state. We also consider a number of pragmatically
motivated variations on memory safety and the reasoning principles they
support. As an application of our characterization, we evaluate the security
of a previously proposed dynamic monitor for memory safety of heap-allocated
data.

##  1 Introduction

Memory safety, and the vulnerabilities that follow from its absence [43], are
common concerns. So what is it, exactly? Intuitions abound, but translating
them into satisfying formal definitions is surprisingly difficult [20].

In large part, this difficulty stems from the prominent role that informal,
everyday intuition assigns, in discussions of memory safety, to a range of
errors related to memory misuse—buffer overruns, double frees, etc.
Characterizing memory safety in terms of the absence of these errors is
tempting, but this falls short for two reasons. First, there is often
disagreement on which behaviors qualify as errors. For example, many real-
world C programs intentionally rely on unrestricted pointer arithmetic [28],
though it may yield undefined behavior according to the language standard [21,
§6.5.6]. Second, from the perspective of security, the critical issue is not
the errors themselves, but rather the fact that, when they occur in unsafe
languages like C, the program’s ensuing behavior is determined by obscure,
low-level factors such as the compiler’s choice of run-time memory layout,
often leading to exploitable vulnerabilities. By contrast, in memory-safe
languages like Java, programs can attempt to access arrays out of bounds, but
such mistakes lead to sensible, predictable outcomes.

Rather than attempting a definition in terms of bad things that cannot happen,
we aim to formalize memory safety in terms of reasoning principles that
programmers can soundly apply in its presence (or conversely, principles that
programmers should not naively apply in unsafe settings, because doing so can
lead to serious bugs and vulnerabilities). Specifically, to give an account of
memory safety, as opposed to more inclusive terms such as “type safety,” we
focus on reasoning principles that are common to a wide range of stateful
abstractions, such as records, tagged or untagged unions, local variables,
closures, arrays, call stacks, objects, compartments, and address spaces.

What sort of reasoning principles? Our inspiration comes from separation logic
[36], a variant of Hoare logic designed to verify complex heap-manipulating
programs. The power of separation logic stems from _local reasoning_ about
state: to prove the correctness of a program component, we must argue that its
memory accesses are confined to a _footprint_ , a precise region demarcated by
the specification. This discipline allows proofs to ignore regions outside of
the footprint, while ensuring that arbitrary invariants for these regions are
preserved during execution.

The locality of separation logic is deeply linked to memory safety. Consider a
hypothetical jpeg decoding procedure that manipulates image buffers. We might
expect its execution not to interfere with the integrity of an unrelated
window object in the program. We can formalize this requirement in separation
logic by proving a specification that includes only the image buffers, but not
the window, in the decoder’s footprint. Showing that the footprint is
respected would amount to checking the bounds of individual buffer accesses,
thus enforcing memory safety; conversely, if the decoder is not memory safe, a
simple buffer overflow might suffice to tamper with the window object, thus
violating locality and potentially paving the way to an attack.

Our aim is to extend this line of reasoning beyond conventional separation
logic, seeking to encompass settings such as ML, Java, or Lisp that enforce
memory safety automatically without requiring complete correctness
proofs—which can be prohibitively expensive for large code bases, especially
in the presence of third-party libraries or plugins over which we have little
control. The key observation is that memory safety forces code to respect a
natural footprint: the set of its reachable memory locations (reachable with
respect to the variables it mentions). Suppose that the jpeg decoder above is
written in Java. Though we may not know much about its input-output behavior,
we can still assert that it cannot have any effect on the window object simply
by replacing the detailed reasoning demanded by separation logic by a simple
inaccessibility check.

Our _first contribution_ is to formalize local reasoning principles supported
by an ideal notion of memory safety, using a simple language (Section 2) to
ground our discussion. We show three results (Theorems 3.1, 3.3 and 3.4) that
explain how the execution of a piece of code is affected by extending its
initial heap. These results lead to a _noninterference_ property (Corollary
1), ensuring that code cannot affect or be affected by unreachable memory. In
Section 3.3, we show how these results yield a variant of the frame rule of
separation logic (Theorem 3.6), which embodies its local reasoning
capabilities. The two variants have complementary strengths and weaknesses:
while the original rule applies to unsafe settings like C, but requires
comprehensively verifying individual memory accesses, our variant does not
require proving that every access is correct, but demands a stronger notion of
separation between memory regions. These results have been verified with the
Coq proof assistant.111The proofs are available at:
https://github.com/arthuraa/memory-safe-language.

Our _second contribution_ (Section 4) is to evaluate pragmatically motivated
relaxations of the ideal notion above, exploring various trade-offs between
safety, performance, flexibility, and backwards compatibility. These variants
can be broadly classified into two groups according to reasoning principles
they support. The stronger group gives up on some secrecy guarantees, but
still ensures that pieces of code cannot modify the contents of unreachable
parts of the heap. The weaker group, on the other hand, leaves gaps that
completely invalidate reachability-based reasoning.

Our _third contribution_ (Section 5) is to demonstrate how our
characterization applies to more realistic settings, by analyzing a heap-
safety monitor for machine code [15, 5]. We prove that the abstract machine
that it implements also satisfies a noninterference property, which can be
transferred to the monitor via refinement, modulo memory exhaustion issues
discussed in Section 4. These proofs are also done in Coq.222 Available at
https://github.com/micro-policies/micro-policies-
coq/tree/master/memory_safety.

We discuss related work on memory safety and stronger reasoning principles in
Section 6, and conclude in Section 7. While memory safety has seen prior
formal investigation (e.g. [31, 41]), our characterization is the first
phrased in terms of reasoning principles that are valid when memory safety is
enforced automatically. We hope that these principles can serve as good
criteria for formally evaluating such enforcement mechanisms in practice.
Moreover, our definition is self-contained and does not rely on additional
features such as full-blown capabilities, objects, module systems, etc. Since
these features tend to depend on some form of memory safety anyway, we could
see our characterization as a common core of reasoning principles that
underpin all of them.

##  2 An Idealized Memory-Safe Language

Our discussion begins with a concrete case study: a simple imperative language
with manual memory management. It features several mechanisms for controlling
the effects of memory misuse, ranging from the most conventional, such as
bounds checking for spatial safety, to more uncommon ones, such as assigning
unique identifiers to every allocated block for ensuring temporal safety.

Choosing a language with manual memory management may seem odd, since safety
is often associated with garbage collection. We made this choice for two
reasons. First, most discussions on memory safety are motivated by its absence
from languages like C that also rely on manual memory management. There is a
vast body of research that tries to make such languages safer, and we would
like our account to apply to it. Second, we wanted to stress that our
characterization does not depend fundamentally on the mechanisms used to
enforce memory safety, especially because they might have complementary
advantages and shortcomings. For example, manual memory management can lead to
more memory leaks; garbage collectors can degrade performance; and specialized
type systems for managing memory [41, 37] are more complex. After a brief
overview of the language, we explore its reasoning principles in Section 3.

Command | Description
---|---
$x\leftarrow e$ | Local assignment
$x\leftarrow[e]$ | Read from heap
$[e_{1}]\leftarrow e_{2}$ | Heap assignment
$x\leftarrow\mathsf{alloc}(e_{size})$ | Allocation
$\mathsf{free}(e)$ | Deallocation
$\mathsf{skip}$ | Do nothing
$\mathsf{if}\;e\;\mathsf{then}\;c_{1}\;\mathsf{else}\;c_{2}$ | Conditional
$\mathsf{while}\;e\;\mathsf{do}\;c\;\mathsf{end}$ | Loop
$c_{1};c_{2}$ | Sequencing

$\displaystyle s\in\mathcal{S}$
$\displaystyle\triangleq\mathcal{L}\times\mathcal{M}$ (states) $\displaystyle
l\in\mathcal{L}$
$\displaystyle\triangleq\mathsf{var}\rightharpoonup_{\mathrm{fin}}\mathcal{V}$
(local stores) $\displaystyle m\in\mathcal{M}$
$\displaystyle\triangleq\mathbb{I}\times\mathbb{Z}\rightharpoonup_{\mathrm{fin}}\mathcal{V}$
(heaps) $\displaystyle v\in\mathcal{V}$
$\displaystyle\triangleq\mathbb{Z}\uplus\mathbb{B}\uplus\\{\mathsf{nil}\\}\uplus\mathbb{I}\times\mathbb{Z}$
(values) $\displaystyle\mathcal{O}$
$\displaystyle\triangleq\mathcal{S}\uplus\\{\mathsf{error}\\}$ (outcomes)
$\displaystyle\mathbb{I}$ $\displaystyle\triangleq\text{a countably infinite
set}$ $\displaystyle X\rightharpoonup_{\mathrm{fin}}Y$
$\displaystyle\triangleq\text{finite partial functions $X\rightharpoonup Y$}$

Figure 1: Syntax, states and values

Figure 1 summarizes the language syntax and other basic definitions.
Expressions $e$ include variables $x\in\mathsf{var}$, numbers
$n\in\mathbb{Z}$, booleans $b\in\mathbb{B}$, an invalid pointer
$\mathsf{nil}$, and various operations, both binary (arithmetic, logic, etc.)
and unary (extracting the offset of a pointer). We write $[e]$ for
dereferencing the pointer denoted by $e$.

Programs operate on states consisting of two components: a _local store_ ,
which maps variables to values, and a _heap_ , which maps pointers to values.
Pointers are not bare integers, but rather pairs $(i,n)$ of a _block
identifier_ $i\in\mathbb{I}$ and an offset $n\in\mathbb{Z}$. The offset is
relative to the corresponding block, and the identifier $i$ need not bear any
direct relation to the physical address that might be used in a concrete
implementation on a conventional machine. (That is, we can equivalently think
of the heap as mapping each identifier to a separate array of heap cells.)
Similar structured memory models are widely used in the literature, as in the
CompCert verified C compiler [26] and other models of the C language [23], for
instance.

We write $\llbracket c\rrbracket(s)$ to denote the outcome of running a
program $c$ in an initial state $s$, which can be either a successful final
state $s^{\prime}$ or a fatal run-time error. Note that $\llbracket
c\rrbracket$ is partial, to account for non-termination. Similarly,
$\llbracket e\rrbracket(s)$ denotes the result of evaluating the expression
$e$ on the state $s$ (expression evaluation is total and has no side effects).
The formal definition of these functions is left to the Appendix; we just
single out a few aspects that have a crucial effect on the security properties
discussed later.

#### Illegal Memory Accesses Lead to Errors

The language controls the effect of memory misuse by raising errors that stop
execution immediately. This contrasts with typical C implementations, where
such errors lead to unpredictable _undefined behavior_. The main errors are
caused by reads, writes, and frees to the current memory $m$ using _invalid
pointers_ —that is, pointers $p$ such that $m(p)$ is undefined. Such pointers
typically arise by offsetting an existing pointer out of bounds or by freeing
a structure on the heap (which turns all other pointers to that block in the
program state into dangling ones). In common parlance, this discipline ensures
both _spatial_ and _temporal_ memory safety.

#### Block Identifiers are Capabilities

Pointers can only be used to access memory corresponding to their identifiers,
which effectively act as capabilities. Identifiers are set at allocation time,
where they are chosen to be fresh with respect to the entire current state
(i.e., the new identifier is not associated with any pointers defined in the
current memory, stored in local variables, or stored on the heap). Once
assigned, identifiers are immutable, making it impossible to fabricate a
pointer to an allocated block out of thin air. This can be seen, for instance,
in the semantics of addition, which allows pointer arithmetic but does not
affect identifiers:

$\displaystyle\llbracket e_{1}+e_{2}\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}n_{1}+n_{2}&\text{if $\llbracket
e_{i}\rrbracket(s)=n_{i}$}\\\ (i,n_{1}+n_{2})&\text{if $\llbracket
e_{1}\rrbracket(s)=(i,n_{1})$ and $\llbracket e_{2}\rrbracket(s)=n_{2}$}\\\
\mathsf{nil}&\text{otherwise}\end{cases}$

For simplicity, nonsensical combinations such as adding two pointers simply
result in the $\mathsf{nil}$ value. A real implementation might represent
identifiers with hardware tags and use an increasing counter to generate
identifiers for new blocks (as done by Dhawan et al. [15]; see section 5.1);
if enough tags are available, every identifier will be fresh.

#### Block Identifiers Cannot be Observed

Because of the freshness condition above, identifiers can reveal information
about the entire program state. For example, if they are chosen according to
an increasing counter, knowing what identifier was assigned to a new block
tells us how many allocations have been performed. A concrete implementation
would face similar issues related to the choice of physical addresses for new
allocations. (Such issues are commonplace in systems that combine dynamic
allocation and information-flow control [12].) For this reason, our language
keeps identifiers opaque and inaccessible to programs; they can only be used
to reference values in memory, and nothing else. We discuss a more permissive
approach in Section 4.2.

Note that hiding identifiers doesn’t mean we have to hide _everything_
associated with a pointer: besides using pointers to access memory, programs
can also safely extract their offsets and test if two pointers are equal
(which means equality for both offsets and identifiers). Our Coq development
also shows that it is sound to compute the size of a memory block via a valid
pointer.

#### New Memory is Always Initialized

Whenever a memory block is allocated, all of its contents are initialized to
$0$. (The exact value does not matter, as long it is some constant that is not
a previously allocated pointer.) This is important for ensuring that
allocation does not leak secrets present in previously freed blocks; we return
to this point in Section 4.3.

##  3 Reasoning with Memory Safety

Having presented our language, we now turn to the reasoning principles that it
supports. Intuitively, these principles allow us to analyze the effect of a
piece of code by restricting our attention to a smaller portion of the program
state. A first set of _frame theorems_ (3.1, 3.3, and 3.4) describes how the
execution of a piece of code is affected by extending the initial state on
which it runs. These in turn imply a noninterference property, Corollary 1,
guaranteeing that program execution is independent of inaccessible memory
regions—that is, those that correspond to block identifiers that a piece of
code does not possess. Finally, in Section 3.3, we discuss how the frame
theorems can be recast in the language of separation logic, leading to a new
variant of its frame rule (Theorem 3.6).

###  3.1 Basic Properties of Memory Safety

$\displaystyle(l_{1},m_{1})\cup(l_{2},m_{2})$
$\displaystyle\triangleq(l_{1}\cup l_{2},m_{1}\cup m_{2})$ (state union)
$\displaystyle(f\cup g)(x)$ $\displaystyle\triangleq\begin{cases}f(x)&\text{if
$x\in\mathsf{dom}(f)$}\\\ g(x)&\text{otherwise}\end{cases}$ (partial function
union) $\displaystyle\mathsf{blocks}(l,m)$
$\displaystyle\triangleq\\{i\in\mathbb{I}\mid\exists
n,(i,n)\in\mathsf{dom}(m)\\}$ (identifiers of live blocks)
$\displaystyle\mathsf{ids}(l,m)$ $\displaystyle\triangleq\mathsf{blocks}(l,m)$
(all identifiers in state) $\displaystyle\cup\\{i\mid\exists
x,n,l(x)=(i,n)\\}$ $\displaystyle\cup\\{i\mid\exists p,n,m(p)=(i,n)\\}$
$\displaystyle\mathsf{vars}(l,m)$ $\displaystyle\triangleq\mathsf{dom}(l)$
(defined local variables) $\displaystyle\mathsf{vars}(c)$
$\displaystyle\triangleq\text{local variables of program $c$}$ $\displaystyle
X\mathrel{\\#}Y$ $\displaystyle\triangleq(X\cap Y=\emptyset)$ (disjoint sets)
$\displaystyle\pi\cdot s$ $\displaystyle\triangleq\text{rename identifiers
with permutation $\pi$}$ Figure 2: Basic notation

Figure 2 summarizes basic notation used in our results. By _permutation_ , we
mean a function $\pi:\mathbb{I}\to\mathbb{I}$ that has a two-sided inverse
$\pi^{-1}$; that is,
$\pi\circ\pi^{-1}=\pi^{-1}\circ\pi=\mathsf{id}_{\mathbb{I}}$. Some of these
operations are standard and omitted for brevity.333The renaming operation
$\pi\cdot s$, in particular, can be derived formally by viewing $\mathcal{S}$
as a nominal set over $\mathbb{I}$ [34] obtained by combining products,
disjoint unions, and partial functions.

The first frame theorem states that, if a program terminates successfully,
then we can extend its initial state almost without affecting execution.

######  Theorem 3.1 (Frame OK)

Let $c$ be a command, and $s_{1}$, $s_{1}^{\prime}$, and $s_{2}$ be states.
Suppose that $\llbracket c\rrbracket(s_{1})=s_{1}^{\prime}$,
$\mathsf{vars}(c)\subseteq\mathsf{vars}(s_{1})$, and
$\mathsf{blocks}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{2})$. Then there exists
a permutation $\pi$ such that $\llbracket c\rrbracket(s_{1}\cup
s_{2})=\pi\cdot s_{1}^{\prime}\cup s_{2}$ and $\mathsf{blocks}(\pi\cdot
s_{1}^{\prime})\mathrel{\\#}\mathsf{blocks}(s_{2})$.

The second premise, $\mathsf{vars}(c)\subseteq\mathsf{vars}(s_{1})$,
guarantees that all the variables needed to run $c$ are already defined in
$s_{1}$, implying that their values do not change once we extend that initial
state with $s_{2}$. The third premise,
$\mathsf{blocks}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{2})$, means that the
memories of $s_{1}$ and $s_{2}$ store disjoint regions. Finally, the
conclusion of the theorem states that (1) the execution of $c$ does not affect
the extra state $s_{2}$ and (2) the rest of the result is almost the same as
$s_{1}^{\prime}$, except for a permutation of block identifiers.

Permutations are needed to avoid clashes between identifiers in $s_{2}$ and
those assigned to regions allocated by $c$ when running on $s_{1}$. For
instance, suppose that the execution of $c$ on $s_{1}$ allocated a new block,
and that this block was assigned some identifier $i\in\mathbb{I}$. If the
memory of $s_{2}$ already had a block corresponding to $i$, $c$ would have to
choose a different identifier $i^{\prime}$ for allocating that block when
running on $s_{1}\cup s_{2}$. This change requires replacing all occurrences
of $i$ by $i^{\prime}$ in the result of the first execution, which can be
achieved with a permutation that swaps these two identifiers.

The proof of Theorem 3.1 relies crucially on the facts that programs cannot
inspect identifiers, that memory can grow indefinitely (a common assumption in
formal models of memory), and that memory operations fail on invalid pointers.
Because of the permutations, we also need to show that permuting the initial
state $s$ of a command $c$ with any permutation $\pi$ yields the same outcome,
up to some additional permutation $\pi^{\prime}$ that again accounts for
different choices of fresh identifiers.

######  Theorem 3.2 (Renaming states)

Let $s$ be a state, $c$ a command, and $\pi$ a permutation. There exists
$\pi^{\prime}$ such that:

$\displaystyle\llbracket c\rrbracket(\pi\cdot
s)=\begin{cases}\mathsf{error}&\text{if $\llbracket
c\rrbracket(s)=\mathsf{error}$}\\\ \bot&\text{if $\llbracket
c\rrbracket(s)=\bot$}\\\ \pi^{\prime}\cdot\pi\cdot s^{\prime}&\text{if
$\llbracket c\rrbracket(s)=s^{\prime}$}\end{cases}$

A similar line of reasoning yields a second frame theorem, which says that we
cannot make a program terminate just by extending its initial state.

######  Theorem 3.3 (Frame Loop)

Let $c$ be a command, and $s_{1}$ and $s_{2}$ be states. If $\llbracket
c\rrbracket(s_{1})=\bot$, $\mathsf{vars}(c)\subseteq\mathsf{vars}(s_{1})$, and
$\mathsf{blocks}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{2})$, then $\llbracket
c\rrbracket(s_{1}\cup s_{2})=\bot$.

The third frame theorem shows that extending the initial state also preserves
erroneous executions. Its statement is similar to the previous ones, but with
a subtle twist. In general, by extending the state of a program with a block,
we might turn an erroneous execution into a successful one—if the error was
caused by accessing a pointer whose identifier matches that new block. To
avoid this, we need a different premise
($\mathsf{ids}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{2})$) preventing any
pointers in the original state $s_{1}$ from referencing the new blocks in
$s_{2}$—which is only useful because our language prevents programs from
forging pointers to existing regions. Since
$\mathsf{blocks}(s)\subseteq\mathsf{ids}(s)$, this premise is stronger than
the analogous ones in the preceding results.

######  Theorem 3.4 (Frame Error)

Let $c$ be a command, and $s_{1}$ and $s_{2}$ be states. If $\llbracket
c\rrbracket(s_{1})=\mathsf{error}$,
$\mathsf{vars}(c)\subseteq\mathsf{vars}(s_{1})$, and
$\mathsf{ids}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{2})$, then $\llbracket
c\rrbracket(s_{1}\cup s_{2})=\mathsf{error}$.

###  3.2 Memory Safety and Noninterference

The consequences of memory safety analyzed so far are intimately tied to the
notion of _noninterference_ [19]. In its most widely understood sense,
noninterference is a _secrecy_ guarantee: varying secret inputs has no effect
on public outputs. Sometimes, however, it is also used to describe _integrity_
guarantees: low-integrity inputs have no effect on high-integrity outputs. In
fact, both guarantees apply to unreachable memory in our language, since they
do not affect code execution; that is, execution (1) cannot modify these
inaccessible regions (preserving their integrity), and (2) cannot learn
anything meaningful about them, not even their presence (preserving their
secrecy).

######  Corollary 1 (Noninterference)

Let $s_{1}$, $s_{21}$, and $s_{22}$ be states and $c$ be a command. Suppose
that $\mathsf{vars}(c)\subseteq\mathsf{vars}(s_{1})$, that
$\mathsf{ids}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{21})$ and that
$\mathsf{ids}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{22})$. When running $c$ on
the extended states $s_{1}\cup s_{21}$ and $s_{1}\cup s_{22}$, only one of the
following three possibilities holds: (1) both executions loop ($\llbracket
c\rrbracket(s_{1}\cup s_{21})=\llbracket c\rrbracket(s_{1}\cup s_{22})=\bot$);
(2) both executions terminate with an error ($\llbracket c\rrbracket(s_{1}\cup
s_{21})=\llbracket c\rrbracket(s_{1}\cup s_{22})=\mathsf{error}$); or (3) both
executions successfully terminate without interfering with the inaccessible
portions $s_{21}$ and $s_{22}$ (formally, there exists a state
$s_{1}^{\prime}$ and permutations $\pi_{1}$ and $\pi_{2}$ such that
$\llbracket c\rrbracket(s_{1}\cup s_{2i})=\pi_{i}\cdot s_{1}^{\prime}\cup
s_{2i}$ and $\mathsf{ids}(\pi_{i}\cdot
s_{1}^{\prime})\mathrel{\\#}\mathsf{blocks}(s_{2i})$, for $i=1,2$).

Noninterference is often formulated using an _indistinguishability relation_
on states, which expresses that one state can be obtained from the other by
varying its secrets. We could have equivalently phrased the above result in a
similar way. Recall that the hypothesis
$\mathsf{ids}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{2})$ means that memory
regions stored in $s_{2}$ are unreachable via $s_{1}$. Then, we could call two
states “indistinguishable” if the reachable portions are the same (except for
a possible permutation). In Section 4, the connection with noninterference
will provide a good benchmark for comparing different flavors of memory
safety.

###  3.3 Memory Safety and Separation Logic

We now explore the relation between the principles identified above,
especially regarding integrity, and the local reasoning facilities of
separation logic. Separation logic targets specifications of the form
$\\{p\\}\;c\;\\{q\\}$, where $p$ and $q$ are predicates over program states
(subsets of $\mathcal{S}$). For our language, this could roughly mean

$\displaystyle\forall s\in p,$
$\displaystyle\,\mathsf{vars}(c)\subseteq\mathsf{vars}(s)\Rightarrow\llbracket
c\rrbracket(s)\in q\cup\\{\bot\\}.$

That is, if we run $c$ in a state satisfying $p$, it will either diverge or
terminate in a state that satisfies $q$, but it will not trigger an error.
Part of the motivation for precluding errors is that in unsafe settings like C
they yield undefined behavior, destroying all hope of verification.

Local reasoning in separation logic is embodied by the _frame rule_ , a
consequence of Theorems 3.1 and 3.3. Roughly, it says that a verified program
can only affect a well-defined portion of the state, with all other memory
regions left untouched.444Technically, the frame rule requires a slightly
stronger notion of specification, accounting for permutations of allocated
identifiers; our Coq development has a more precise statement.

###### Theorem 3.5

Let $p$, $q$, and $r$ be predicates over states and $c$ be a command. The rule

$\displaystyle\displaystyle{\hbox{\hskip
88.35777pt\vbox{\hbox{\hskip-88.35777pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{independent}(r,\mathsf{modvars}(c))$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\\{p\\}\;c\;\\{q\\}$}}}}\vbox{}}}\over\hbox{\hskip
32.99124pt\vbox{\vbox{}\hbox{\hskip-32.99123pt\hbox{\hbox{$\displaystyle\displaystyle\\{p*r\\}\;c\;\\{q*r\\}$}}}}}}$
Frame

is sound, where $\mathsf{modvars}(c)$ is the set of local variables modified
by $c$, $\mathsf{independent}(r,V)$ means that the assertion $r$ does not
depend on the set of local variables $V$

$\forall l_{1}\,l_{2}\,m,(\forall x\notin
V,\;l_{1}(x)=l_{2}(x))\Rightarrow(l_{1},m)\in r\Rightarrow(l_{2},m)\in r,$

and $p*r$ denotes the _separating conjunction_ of $p$ and $r$:

$\\{(l,m_{1}\cup m_{2})\mid(l,m_{1})\in p,(l,m_{2})\in
r,\mathsf{blocks}(l,m_{1})\mathrel{\\#}\mathsf{blocks}(l,m_{2})\\}.$

As useful as it is, precluding errors during execution makes it difficult to
use separation logic for _partial verification_ : proving any property, no
matter how simple, of a nontrivial program requires detailed reasoning about
its internals. Even the following vacuous rule is unsound in separation logic:

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
26.35994pt\vbox{\vbox{}\hbox{\hskip-26.35994pt\hbox{\hbox{$\displaystyle\displaystyle\\{p\\}\;c\;\\{\mathsf{true}\\}$}}}}}}$
Taut

For a counterexample, take $p$ to be $\mathsf{true}$ and $c$ to be some
arbitrary memory read $x\leftarrow[y]$. If we run $c$ on an empty heap, which
trivially satisfies the precondition, we obtain an error, contradicting the
specification.

Fortunately, our memory-safe language—in which errors have a sensible,
predictable semantics, as opposed to wild undefined behavior—supports a
variant of separation logic that allows looser specifications of the form
$\\{p\\}\;c\;\\{q\\}_{e}$, defined as

$\displaystyle\forall s\in p,$
$\displaystyle\,\mathsf{vars}(c)\subseteq\mathsf{vars}(s)\Rightarrow\llbracket
c\rrbracket(s)\in q\cup\\{\bot,\mathsf{error}\\}.$

These specifications are weaker than their conventional counterparts, leading
to a subsumption rule:

$\displaystyle\displaystyle{\hbox{\hskip
19.8686pt\vbox{\hbox{\hskip-19.86859pt\hbox{\hbox{$\displaystyle\displaystyle\\{p\\}\;c\;\\{q\\}$}}}\vbox{}}}\over\hbox{\hskip
21.17236pt\vbox{\vbox{}\hbox{\hskip-21.17235pt\hbox{\hbox{$\displaystyle\displaystyle\\{p\\}\;c\;\\{q\\}_{e}$}}}}}}$

Because errors are no longer prevented, the Taut rule
$\\{p\\}\;c\;\\{\mathsf{true}\\}_{e}$ becomes sound, since the
$\mathsf{true}{}$ postcondition now means that any outcome whatsoever is
acceptable. Unfortunately, there is a price to pay for allowing errors: they
compromise the soundness of the frame rule. The reason, as hinted in the
introduction, is that preventing run-time errors has an additional purpose in
separation logic: it forces programs to act locally—that is, to access only
the memory delimited their pre- and postconditions. To see why, consider the
same program $c$ as above, $x\leftarrow[y]$. This program clearly yields an
error when run on an empty heap, implying that the triple
$\\{\mathsf{emp}\\}\;c\;\\{x=0\\}_{e}$ is valid, where the predicate
$\mathsf{emp}$ holds of any state with an empty heap and $x=0$ holds of states
whose local store maps $x$ to $0$. Now consider what happens if we try to
apply an analog of the frame rule to this triple using the frame predicate
$y\mapsto 1$, which holds in states where $y$ contains a pointer to the unique
defined location on the heap, which stores the value $1$. After some
simplification, we arrive at the specification $\\{y\mapsto
1\\}\;c\;\\{x=0\wedge y\mapsto 1\\}_{e}$, which clearly does not hold, since
executing $c$ on a state satisfying the precondition leads to a successful
final state mapping $x$ to $1$.

For the frame rule to be recovered, it needs to take errors into account. The
solution lies on the reachability properties of memory safety: instead of
enforcing locality by preventing errors, we can use the fact that memory
operations in a safe language are automatically local—in particular, local to
the identifiers that the program possesses.

###### Theorem 3.6

Under the same assumptions as Theorem 3.5, the following rule is sound

$\displaystyle\displaystyle{\hbox{\hskip
89.66153pt\vbox{\hbox{\hskip-89.66153pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{independent}(r,\mathsf{modvars}(c))\qquad\\{p\\}\;c\;\\{q\\}_{e}$}}}\vbox{}}}\over\hbox{\hskip
35.40608pt\vbox{\vbox{}\hbox{\hskip-35.40607pt\hbox{\hbox{$\displaystyle\displaystyle\\{p\triangleright
r\\}\;c\;\\{q\triangleright r\\}_{e}$}}}}}}$ SafeFrame

where $p\mathrel{\triangleright}r$ denotes the _isolating conjunction_ of $p$
and $r$, defined as

$\\{(l,m_{1}\cup m_{2})\mid(l,m_{1})\in p,(l,m_{2})\in
r,\mathsf{ids}(l,m_{1})\mathrel{\\#}\mathsf{blocks}(l,m_{2})\\}.$

The proof is similar to the one for the original rule, but it relies
additionally on Theorem 3.4. This explains why the isolating conjunction is
needed, since it ensures that the fragment satisfying $r$ is unreachable from
the rest of the state.

###  3.4 Discussion

As hinted by their connection with the frame rule, the theorems of Section 3.1
are a form of local reasoning: to reason about a command, it suffices to
consider its reachable state; _how_ this state is used bears no effect on the
unreachable portions. In a more realistic language, reachability might be
inferred from additional information such as typing. But even here it can
probably be accomplished by a simple check of the program text.

For example, consider the hypothetical jpeg decoder from Section 1. We would
like to guarantee that the decoder cannot tamper with an unreachable object—a
window object, a whitelist of trusted websites, etc. The frame theorems give
us a means to do so, provided that we are able to show that the object is
indeed unreachable; additionally, they imply that the jpeg decoder cannot
directly extract any information from this unreachable object, such as
passwords or private keys.

Many real-world attacks involve direct violations of these reasoning
principles. For example, consider the infamous Heartbleed attack on OpenSSL,
which used out-of-bounds reads from a buffer to leak data from completely
unrelated parts of the program state and to steal sensitive information [16].
Given that the code fragment that enabled that attack was just manipulating an
innocuous array, a programmer could easily be fooled into believing (as
probably many have) that that snippet could not possibly access sensitive
information, allowing that vulnerability to remain unnoticed for years.

Finally, our new frame rule only captures the fact that a command cannot
influence the heap locations that it cannot reach, while our noninterference
result (Corollary 1) captures not just this integrity aspect of memory safety,
but also a secrecy aspect. We hope that future research will explore the
connection between the secrecy aspect of memory safety and (relational)
program logics.

##  4 Relaxing Memory Safety

So much for formalism. What about reality? Strictly speaking, the security
properties we have identified do not hold of any real system. This is partly
due to fundamental physical limitations—real systems run with finite memory,
and interact with users in various ways that transcend inputs and outputs,
notably through time and other side channels.555Though the attacker model
considered in this paper does not try to address such side-channel attacks,
one should be able to use the previous research on the subject to protect
against them or limit the damage they can cause [39, 6, 49, 40]. A more
interesting reason is that real systems typically do not impose all the
restrictions required for the proofs of these properties. Languages that aim
for safety generally offer relatively benign glimpses of their implementation
details (such accessing the contents of uninitialized memory, extract physical
addresses from pointers or compare them for ordering) in return for
significant flexibility or performance gains. In other systems, the
concessions are more fundamental, to the extent that it is harder to clearly
delimit what part of a program is unsafe: the SoftBound transformation [31],
for example, adds bounds checks for C programs, but does not protect against
memory-management bugs; a related transformation, CETS [32], is required for
temporal safety.

In this section, we enumerate common relaxed models of memory safety and
evaluate how they affect the reasoning principles and security guarantees of
Section 3. Some relaxations, such as allowing pointers to be forged out of
thin air, completely give up on reachability-based reasoning. Others, however,
retain strong guarantees for integrity while giving up on some secrecy,
allowing aspects of the global state of a program to be observed. For example,
a system with finite memory (Section 4.5) may leak some information about its
memory consumption, and a system that allows pointer-to-integer casts (Section
4.2) may leak information about its memory layout. Naturally, the distinction
between integrity and secrecy should be taken with a grain of salt, since the
former often depends on the latter; for example, if a system grants privileges
to access some component when given with the right password, a secrecy
violation can escalate to an integrity violation!

###  4.1 Forging Pointers

Many real-world C programs use integers as pointers. If this idiom is allowed
without restrictions, then local reasoning is compromised, as every memory
region may be reached from anywhere in the program. It is not surprising that
languages that strive for safety either forbid this kind of pointer forging or
confine it to clear unsafe fragments.

More insidiously, and perhaps surprisingly, similar dangers lurk in the
stateful abstractions of some systems that are widely regarded as “memory
safe.” JavaScript, for example, allows code to access _arbitrary_ global
variables by indexing an associative array with a string, a feature that
enables many serious attacks [1, 18, 44, 29]. One might argue that global
variables in JavaScript are “memory unsafe” because they fail to validate
local reasoning: even if part of a JavaScript program does not explicitly
mention a given global variable, it might still change this variable or the
objects it points to. Re-enabling local reasoning requires strong restrictions
on the programming style [9, 1, 18].

###  4.2 Observing Pointers

The language of Section 2 maintains a complete separation between pointers and
other values. In reality, this separation is often only enforced in one
direction. For example, some tools for enforcing memory safety in C [31, 13]
allow pointer-to-integer casts [23] (a feature required by many low-level
idioms [10, 28]); and the default implementation of `hashCode()` in Java leaks
address information. To model such features, we can extend the syntax of
expressions with a form $\mathsf{cast}(e)$, the semantics of which are defined
with some function
$\llbracket\mathsf{cast}\rrbracket:\mathbb{I}\times\mathbb{Z}\to\mathbb{Z}$
for converting a pointer to an integer:

$\displaystyle\llbracket\mathsf{cast}(e)\rrbracket(s)$
$\displaystyle=\llbracket\mathsf{cast}\rrbracket(\llbracket
e\rrbracket(s))\qquad\text{ if $\llbracket
e\rrbracket(s)\in\mathbb{I}\times\mathbb{Z}$}$

Note that the original language included an operator for extracting the offset
of a pointer. Their definitions are similar, but have crucially different
consequences: while offsets do not depend on the identifier, allocation order,
or other low-level details of the language implementation (such as the choice
of physical addresses when allocating a block), all of these could be relevant
when defining the semantics of $\mathsf{cast}$. The three frame theorems (3.1,
3.3, and 3.4) are thus lost, because the state of unreachable parts of the
heap may influence integers observed by the program. An important consequence
is that secrecy is weakened in this language: an attacker could exploit
pointers as a side-channel to learn secrets about data it shouldn’t access.

Nevertheless, _integrity_ is not affected: if a block is unreachable, its
contents will not change at the end of the execution. (This result was also
proved in Coq.)

######  Theorem 4.1 (Integrity-only Noninterference)

Let $s_{1}$, $s_{2}$, and $s^{\prime}$ be states and $c$ a command such that
$\mathsf{vars}(c)\subseteq\mathsf{vars}(s_{1})$,
$\mathsf{ids}(s_{1})\mathrel{\\#}\mathsf{blocks}(s_{2})$, and $\llbracket
c\rrbracket(s_{1}\cup s_{2})=s^{\prime}$. Then we can find
$s_{1}^{\prime}\in\mathcal{S}$ such that $s^{\prime}=s_{1}^{\prime}\cup s_{2}$
and $\mathsf{ids}(s_{1}^{\prime})\mathrel{\\#}\mathsf{blocks}(s_{2})$.

The stronger noninterference result of Corollary 1 showed that, if pointer-to-
integer casts are prohibited, changing the contents of the unreachable portion
$s_{2}$ has no effect on the reachable portion, $s_{1}^{\prime}$. In contrast,
Theorem 4.1 allows changes in $s_{2}$ to influence $s_{1}^{\prime}$ in
arbitrary ways in the presence of these casts: not only can the contents of
this final state change, but the execution can also loop forever or terminate
in an error.

To see why, suppose that the jpeg decoder of Section 1 is part of a web
browser, but that it does not have the required pointers to learn the address
that the user is currently visiting. Suppose that there is some relation
between the memory consumption of the program and that website, and that there
is some correlation between the memory consumption and the identifier assigned
to a new block. Then, by allocating a block and converting its pointer to a
integer, the decoder might be able to infer useful information about the
visited website [22]. Thus, if $s_{2}$ denoted the part of the state where
that location is stored, changing its contents would have a nontrivial effect
on $s_{1}^{\prime}$, the part of the state that the decoder does have access
to. We could speculate that, in a reasonable system, this channel can only
reveal information about the layout of unreachable regions, and not their
contents. Indeed, we conjecture this for the language of this subsection.

Finally, it is worth noting that simply excluding casts might not suffice to
prevent this sort of vulnerability. Recall that our language takes both
offsets and identifiers into account for equality tests. For performance
reasons, we could have chosen a different design that only compares physical
addresses, completely discarding identifiers. If attackers know the address of
a pointer in the program—which could happen, for instance, if they have access
to the code of the program and of the allocator—they can use pointer
arithmetic (which is generally harmless and allowed in our language) to find
the address of other pointers. If $x$ holds the pointer they control, they can
run, for instance,

$y\leftarrow\mathsf{alloc}(1);\mathsf{if}\;x+1729=y\;\mathsf{then}\;\ldots\;\mathsf{else}\;\ldots,$

to learn the location assigned to $y$ and draw conclusions about the global
state.

###  4.3 Uninitialized Memory

Safe languages typically initialize new variables and objects. But this can
degrade performance, leading to cases where this feature is dropped—including
standard C implementations, safer alternatives [31, 13], OCaml’s Bytes.create
primitive, or Node.js’s Buffer.allocUnsafe, for example.

The problem with this concession is that the entire memory becomes relevant to
execution, and local reasoning becomes much harder. By inspecting old values
living in uninitialized memory, an attacker can learn about parts of the state
they shouldn’t access and violate secrecy. This issue would become even more
severe in a system that allowed old pointers or other capabilities to occur in
re-allocated memory in a way that the program can use, since they could yield
access to restricted resources directly, leading to potential integrity
violations as well. (The two examples given above—OCaml and Node.js—do not
suffer from this issue, because any preexisting pointers in re-allocated
memory are treated as bare bytes that cannot be used to access memory.)

###  4.4 Dangling Pointers and Freshness

Another crucial issue is the treatment of dangling pointers—references to
previously freed objects. Dangling pointers are problematic because there is
an inherent tension between giving them a sensible semantics (for instance,
one that validates the properties of Section 3) and obtaining good performance
and predictability. Languages with garbage collection avoid the issue by
forbidding dangling pointers altogether—heap storage is freed only when it is
unreachable. In the language of section 2, besides giving a well-defined
behavior to the use of dangling pointers (signaling an error), we imposed
strong freshness requirements on allocation, mandating not only that the new
identifier not correspond to any existing block, but also that it not be
present anywhere else in the state.

To see how the results of Section 3 are affected by weakening freshness,
suppose we run the program $x\leftarrow\mathsf{alloc}(1);z\leftarrow(y=x)$ on
a state where $y$ holds a dangling pointer. Depending on the allocator and the
state of the memory, the pointer assigned to $x$ could be equal to $y$. Since
this outcome depends on the entire state of the system, not just the reachable
memory, Theorems 3.1, 3.3 and 3.4 now fail. Furthermore, an attacker with
detailed knowledge of the allocator could launder secret information by
testing pointers for equality. Weakening freshness can also have integrity
implications, since it becomes harder to ensure that blocks are properly
isolated. For instance, a newly allocated block might be reachable through a
dangling pointer controlled by an attacker, allowing them to access that block
even if they were not supposed to.

Some practical solutions for memory safety use mechanisms similar to our
language’s, where each memory location is tagged with an identifier describing
the region it belongs to [11, 15]. Pointers are tagged similarly, and when a
pointer is used to access memory, a violation is detected if its identifier
does not match the location’s. However, for performance reasons, the number of
possible identifiers might be limited to a relatively small number, such as 2
or 4 [11] or 16 [46]. In addition to the problems above, since multiple live
regions can share the same identifier in such schemes, it might be possible
for buffer overflows to lead to violations of secrecy and integrity as well.

Although we framed our discussion in terms of identifiers, the issue of
freshness can manifest itself in other ways. For example, many systems for
spatial safety work by adding base and bounds information to pointers. In some
of these [13, 31], dangling pointers are treated as an orthogonal issue, and
it is possible for the allocator to return a new memory region that overlaps
with the range of a dangling pointer, in which case the new region will not be
properly isolated from the rest of the state.

Finally, dangling pointers can have disastrous consequences for overall system
security, independently of the freshness issues just described: freeing a
pointer more than once can break allocator invariants, enabling attacks [43].

###  4.5 Infinite Memory

Our idealized language allows memory to grow indefinitely. But real languages
run on finite memory, and allocation fails when programs run out of space.
Besides enabling denial-of-service attacks, finite memory has consequences for
secrecy. Corollary 1 does not hold in a real programming language as is,
because an increase in memory consumption can cause a previously successful
allocation to fail. By noticing this difference, a piece of code might learn
something about the _entire_ state of the program. How problematic this is in
practice will depend on the particular system under consideration.

A potential solution is to force programs that run out of memory to terminate
immediately. Though this choice might be bad from an availability standpoint,
it is probably the most benign in terms of secrecy. We should be able to prove
an _error-insensitive_ variant of Corollary 1, where the only significant
effect that unreachable memory can have is to turn a successful execution or
infinite loop into an error. Similar issues arise for IFC mechanisms that
often cannot prevent secrets from influencing program termination, leading to
_termination-insensitive_ notions of noninterference.

Unfortunately, even an error-insensitive result might be too strong for real
systems, which often make it possible for attackers to extract multiple bits
of information about the global state of the program—as previously noted in
the IFC literature [4]. Java, for example, does not force termination when
memory runs out, but triggers an exception that can be caught and handled by
user code, which is then free to record the event and probe the allocator with
a different test. And most languages do not operate in batch mode like ours
does, merely producing a single answer at the end of execution; rather, their
programs continuously interact with their environment through inputs and
outputs, allowing them to communicate the exact amount of memory that caused
an error.

This discussion suggests that, if size vulnerabilities are a real concern,
they need to be treated with special care. One approach would be to limit the
amount of memory an untrusted component can allocate [47], so that exhausting
the memory allotted to that component doesn’t reveal information about the
state of the rest of the system (and so that also global denial-of-service
attacks are prevented). A more speculative idea is to develop _quantitative_
versions [39, 6] of the noninterference results discussed here that apply only
if the total memory used by the program is below a certain limit.

##  5 Case Study: A Memory-safety Monitor

To demonstrate the applicability of our characterization, we use it to analyze
a tag-based monitor proposed by Dhawan et al. to enforce heap safety for low-
level code [15]. In prior work [5], we and others showed that an idealized
model of the monitor correctly implements a higher-level abstract machine with
built-in memory safety—a bit more formally, every behavior of the monitor is
also a behavior of the abstract machine. Building upon this work, we prove
that this abstract machine satisfies a noninterference property similar to
Corollary 1. We were also able to prove that a similar result holds for a
lower-level machine that runs a so-called “symbolic” representation of the
monitor—although we had to slightly weaken the result to account for memory
exhaustion (cf. Section 4.5), since the machine that runs the monitor has
finite memory, while the abstract machine has infinite memory. If we had a
verified machine-code implementation of this monitor, it would be possible to
prove a similar result for it as well.

###  5.1 Tag-based Monitor

We content ourselves with a brief overview of Dhawan et al.’s monitor [15, 5],
since the formal statement of the reasoning principles it supports are more
complex than the one for the abstract machine from section 5.2, on which we
will focus. Following a proposal by Clause _et al._ [11], Dhawan et al.’s
monitor enforces memory safety for heap-allocated data by checking and
propagating _metadata tags_. Every memory location receives a tag that
uniquely identifies the allocated region to which that location belongs (akin
to the identifiers in Section 2), and pointers receive the tag of the region
they are allowed to reference. The monitor assigns these tags to new regions
by storing a monotonic counter in protected memory that is bumped on every
call to `malloc`; with a large number of possible tags, it is possible to
avoid the freshness pitfalls discussed in Section 4.4. When a memory access
occurs, the monitor checks whether the tag on the pointer matches the tag on
the location. If they do, the operation is allowed; otherwise, execution
halts. The monitor instruments the allocator to make set up tags correctly.
Its implementation achieves good performance using the _PUMP_ , a hardware
extension accelerating such micro-policies for metadata tagging [15].

###  5.2 Abstract Machine

The memory-safe abstract machine [5] operates on two kinds of values: machine
words $w$, or pointers $(i,w)$, which are pairs of an identifier
$i\in\mathbb{I}$ and an offset $w$. We use $\mathcal{W}$ to denote the set of
machine words, and $\mathcal{V}$ to denote the set of values. Machine states
are triples $(m,\mathit{rs},\mathit{pc})$, where (1)
$m\in\mathbb{I}\rightharpoonup_{\mathrm{fin}}\mathcal{V}^{*}$ is a _memory_
mapping identifiers to lists of values; (2)
$\mathit{rs}\in\mathcal{R}\rightharpoonup_{\mathrm{fin}}\mathcal{V}$ is a
_register bank_ , mapping register names to values; and (3)
$\mathit{pc}\in\mathcal{V}$ is the _program counter_.

The execution of an instruction is specified by a step relation $s\to
s^{\prime}$. If there is no $s^{\prime}$ such that $s\to s^{\prime}$, we say
that $s$ is stuck, which means that a fatal error occurred during execution.
On each instruction, the machine checks if the current program counter is a
pointer and, if so, tries to fetch the corresponding value in memory. The
machine then ensures that this value is a word that correctly encodes an
instruction and, if so, acts accordingly. The instructions of the machine,
representative of typical RISC architectures, allow programs to perform binary
and logical operations, move values to and from memory, and branch. The
machine is in fact fairly similar to the language of Section 2. Some
operations are overloaded to manipulate pointers; for example, adding a
pointer to a word is allowed, and the result is obtained by adjusting the
pointer’s offset accordingly. Accessing memory causes the machine to halt when
the corresponding position is undefined.

In addition to these basic instructions, the machine possesses a set of
special _monitor services_ that can be invoked as regular functions, using
registers to pass in arguments and return values. There are two services
$\mathsf{alloc}$ and $\mathsf{free}$ for managing memory, and one service
$\mathsf{eq}$ for testing whether two values are equal. The reason for using
separate monitor services instead of special instructions is to keep its
semantics closer to the more concrete machine that implements it. While
instructions include an equality test, it cannot replace the $\mathsf{eq}$
service, since it only takes physical addresses into account. As argued in
Section 4.2, such comparisons can be turned into a side channel. To prevent
this, testing two pointers for equality directly using the corresponding
machine instruction results in an error if the pointers have different block
identifiers.

###  5.3 Verifying Memory Safety

The proof of memory safety for this abstract machine mimics the one carried
for the language in Section 3. We use similar notations as before: $\pi\cdot
s$ means renaming every identifier that appears in $s$ according to the
permutation $\pi$, and $\mathsf{ids}(s)$ is the finite set of all identifiers
that appear in the state $s$. A simple case analysis on the possible
instructions yields analogs of Theorems 3.2, 3.1 and 3.4 (we don’t include an
analog of Theorem 3.3 because we consider individual execution steps, where
loops cannot occur).

###### Theorem 5.1

Let $\pi$ be a permutation, and $s$ and $s^{\prime}$ be two machine states
such that $s\to s^{\prime}$. There exists another permutation $\pi^{\prime}$
such that $\pi\cdot s\to\pi^{\prime}\cdot s^{\prime}$.

###### Theorem 5.2

Let $(m_{1},\mathit{rs},\mathit{pc})$ be a state of the abstract machine, and
$m_{2}$ a memory. Suppose that
$\mathsf{ids}(m_{1},\mathit{rs},\mathit{pc})\mathrel{\\#}\mathsf{dom}(m_{2})$,
and that
$(m_{1},\mathit{rs},\mathit{pc})\to(m^{\prime},\mathit{rs}^{\prime},\mathit{pc}^{\prime})$.
Then, there exists a permutation $\pi$ such that $\mathsf{ids}(\pi\cdot
m^{\prime},\pi\cdot\mathit{rs},\pi\cdot\mathit{pc})\mathrel{\\#}\mathsf{dom}(m_{2})$
and $(m_{2}\cup m_{1},\mathit{rs},\mathit{pc})\to(m_{2}\cup\pi\cdot
m^{\prime},\pi\cdot\mathit{rs}^{\prime},\pi\cdot\mathit{pc}^{\prime})$.

###### Theorem 5.3

Let $(m_{1},\mathit{rs},\mathit{pc})$ be a machine state, and $m_{2}$ a
memory. If
$\mathsf{ids}(m_{1},\mathit{rs},\mathit{pc})\mathrel{\\#}\mathsf{dom}(m_{2})$,
and $(m_{1},\mathit{rs},\mathit{pc})$ is stuck, then $(m_{2}\cup
m_{1},\mathit{rs},\mathit{pc})$ is also stuck.

Once again, we can combine these properties to obtain a proof of
noninterference. Our Coq development includes a complete statement.

###  5.4 Discussion

The reasoning principles supported by the memory-safety monitor have an
important difference compared to the ones of Section 3. In the memory-safe
language, reachability is relative to a program’s local variables. If we want
to argue that part of the state is isolated from some code fragment, we just
have to consider that fragment’s local variables—other parts of the program
are still allowed to access the region. The memory-safety monitor, on the
other hand, does not have an analogous notion: an unreachable memory region is
useless, since it remains unreachable by all components forever.

It seems that, from the standpoint of noninterference, heap memory safety
_taken in isolation_ is much weaker than the guarantees it provides in the
presence of other language features, such as local variables. Nevertheless,
the properties studied above suggest several avenues for strengthening the
mechanism and making its guarantees more useful. The most obvious one would be
to use the mechanism as the target of a compiler for a programming language
that provides other (safe) stateful abstractions, such as variables and a
stack for procedure calls. A more modest approach would be to add other state
abstractions to the mechanism itself. Besides variables and call stacks, if
the mechanism made code immutable and separate from data, a simple check would
suffice to tell whether a code segment stored in memory references a given
privileged register. If the register is the only means of reaching a memory
region, we should be able to soundly infer that that code segment is
independent of that region.

On a last note, although the abstract machine we verified is fairly close to
our original language, the dynamic monitor that implements it using tags is
quite different (section 5.1). In particular, the monitor works on a machine
that has a flat memory model, and keeps track of free and allocated memory
using a protected data structure that stores block metadata. It was claimed
that reasoning about this base and bounds information was the most challenging
part of the proof that the monitor implements the abstract machine [5]. For
this reason, we believe that this proof can be adapted to other enforcement
mechanisms that rely solely on base and bounds information—for example, fat
pointers [25, 13] or SoftBound [31]—while keeping a similar abstract machine
as their specification, and thus satisfying a similar noninterference
property. This gives us confidence that our memory safety characterization
generalizes to other settings.

##  6 Related Work

The present work lies at the intersection of two areas of previous research:
one on formal characterizations of memory safety, the other on reasoning
principles for programs. We review the most closely related work in these
areas.

#### Characterizing Memory Safety

Many formal characterizations of memory safety originated in attempts to
reconcile its benefits with low-level code. Generally, these works claim that
a mechanism is safe by showing that it prevents or catches typical temporal
and spatial violations. Examples in the literature include: Cyclone [41], a
language with a type system for safe manual memory management; CCured [33], a
program transformation that adds temporal safety to C by refining its pointer
type with various degrees of safety; Ivory [17] an embedding of a similar
“safe-C variant” into Haskell; SoftBound [31], an instrumentation technique
for C programs for spatial safety, including the detection of bounds
violations within an object; CETS [32], a compiler pass for preventing
temporal safety violations in C programs, including accessing dangling
pointers into freed heap regions and stale stack frames; the memory-safety
monitor for the PUMP [15, 5], which formed the basis of our case study in
Section 5; and languages like Mezzo [35] and Rust [45], whose guarantees
extend to preventing data races [7]. Similar models appear in formalizations
of C [26, 24], which need to rigorously characterize its sources of undefined
behavior—in particular, instances of memory misuse.

Either explicitly or implicitly, these works define memory errors as attempts
to use a pointer to access a location that it was not meant to access—for
example, an out-of-bounds or free one. This was noted by Hicks [20], who,
inspired by SoftBound, proposed to define memory safety as an execution model
that tracks what part of memory each pointer can access. Our characterization
is complementary to these accounts, in that it is _extensional_ : its data
isolation properties allow us to reason directly about the observable behavior
of the program. Furthermore, as demonstrated by our application to the monitor
of Section 5 and the discussions on Section 4, it can be adapted to various
enforcement mechanisms and variations of memory safety.

#### Reasoning Principles

Separation logic [36, 48] has been an important source of inspiration for our
work. The logic’s frame rule enables its local reasoning capabilities and
imposes restrictions that are similar to those mandated by memory-safe
programming guidelines. As discussed in Section 3.3, our reasoning principles
are reminiscent of the frame rule, but use reachability to guarantee locality
in settings where memory safety is enforced automatically. In separation
logic, by contrast, locality needs to be guaranteed for each program
individually by comprehensive proofs.

Several works have investigated similar reasoning principles for a variety of
program analyses, including static, dynamic, manual, or a mixture of those.
Some of these are formulated as expressive logical relations, guaranteeing
that programs are compatible with the framing of state invariants;
representative works include: L${}^{\mbox{\small 3}}$ [3], a linear calculus
featuring strong updates and aliasing control; the work of Benton and Tabereau
[8] on a compiler for a higher-order language; and the work of Devriese _et
al._ [14] on object capabilities for a JavaScript-like language. Other
developments are based on proof systems reminiscent of separation logic; these
include Yarra [38], an extension of C that allows programmers to protect the
integrity of data structures marked as _critical_ ; the work of Agten _et al._
[2], which allows mixing unverified and verified components by instrumenting
the program to check that required assertions hold at interfaces; and the
logic of Swasey _et al._ [42] for reasoning about object capabilities.

Unlike our work, these developments do not propose reachability-based
isolation as a general _definition_ of memory safety, nor do they attempt to
analyze how their reasoning principles are affected by common variants of
memory safety. Furthermore, many of these other works—especially the logical
relations—rely on encapsulation mechanisms such as closures, objects, or
modules that go beyond plain memory safety. Memory safety alone can only
provide complete isolation, while encapsulation provides finer control,
allowing some interaction between components, while guaranteeing the
preservation of certain state invariants. In this sense, one can see memory-
safety reasoning as a special case of encapsulation reasoning. Nevertheless,
it is a practically relevant special case that is interesting on its own,
since when reasoning about an encapsulated component, one must argue
explicitly that the invariants of interest are preserved by the private
operations of that component; memory safety, on the other hand, guarantees
that _any_ invariant on unreachable parts of the memory is automatically
preserved.

Perhaps closer to our work, Maffeis _et al._ [27] show that their notion of
“authority safety” guarantees isolation, in the sense that a component’s
actions cannot influence the actions of another component with disjoint
authority. Their notion of authority behaves similarly to the set of block
identifiers accessible by a program in our language; however, they do not
attempt to connect their notion of isolation to the frame rule,
noninterference, or traditional notions of memory safety.

Morrisett _et al._ [30] state a correctness criterion for garbage collection
based on program equivalence. Some of the properties they study are similar to
the frame rule, describing the behavior of code running in an extended heap.
However, they use this analysis to justify the validity of deallocating
objects, rather than studying the possible interactions between the extra
state and the program in terms of integrity and secrecy.

##  7 Conclusions and Future Work

We have explored the consequences of memory safety for reasoning about
programs, formalizing intuitive principles that, we argue, capture the
essential distinction between memory-safe systems and memory-unsafe ones. We
showed how the reasoning principles we identified apply to a recent dynamic
monitor for heap memory safety.

The systems studied in this paper have a simple storage model: the language of
Section 2 has just global variables and flat, heap-allocated arrays, while the
monitor of Section 5 doesn’t even have variables or immutable code. Realistic
programming platforms, of course, offer much richer stateful abstractions,
including, for example, procedures with stack-allocated local variables as
well as structured objects with contiguously allocated sub-objects. In terms
of memory safety, these systems have a richer vocabulary for describing
resources that programs can access, and programmers could benefit from
isolation-based local reasoning involving these resources.

For example, in typical safe languages with procedures, the behavior of a
procedure should depend only on its arguments, the global variables it uses,
and the portions of the state that are reachable from these values; if the
caller of that procedure has a private object that is not passed as an
argument, it should not affect or be affected by the call. Additionally,
languages such as C allow for objects consisting of contiguously allocated
sub-objects for improved performance. Some systems for spatial safety [31, 13]
allow _capability downgrading_ —that is, narrowing the range of a pointer so
that it can’t access outside of a sub-object’s bounds. It would be interesting
to refine our model to take these features into account. In the case of the
monitor of Section 5, such considerations could lead to improved designs or to
the integration of the monitor inside a secure compiler. Conversely, it would
be interesting to derive finer security properties for relaxations like the
ones discussed in Section 4. Some inspiration could come from the IFC
literature, where quantitative noninterference results provide bounds on the
probability that some secret is leaked, the rate at which it is leaked, how
many bits are leaked, etc. [6, 39].

The main goal of this work was to understand, formally, the benefits of memory
safety for informal and partial reasoning, and to evaluate a variety of
weakened forms of memory safety in terms of which reasoning principles they
preserve. However, our approach may also suggest ways to improve program
verification. One promising idea is to leverage the guarantees of memory
safety to obtain proofs of program correctness modulo unverified code that
could have errors, in contexts where complete verification is too expensive or
not possible (e.g., for programs with a plugin mechanism).

#### Acknowledgments

We are grateful to Antal Spector-Zabusky, Greg Morrisett, Justin Hsu, Michael
Hicks, Nick Benton, Yannis Juglaret, William Mansky, and Andrew Tolmach for
useful suggestions on earlier drafts. This work is supported by NSF grants
Micro-Policies (1513854) and DeepSpec (1521523), DARPA SSITH/HOPE, and ERC
Starting Grant SECOMP (715753).

## Appendix

$\begin{array}[]{rclr}\oplus&::=&{+}\mid{\times}\mid{-}\mid{=}\mid{\leq}\mid{\mathbin{\mathsf{and}}}\mid{\mathbin{\mathsf{or}}}&\text{(operators)}\\\
e&::=&x\in\mathsf{var}\mid b\in\mathbb{B}\mid
n\in\mathbb{Z}&\text{(expressions)}\\\ &\mid&e_{1}\oplus
e_{2}\mid\mathsf{not}\,e\mid\mathsf{offset}\,e\mid\mathsf{nil}&\\\
c&::=&\mathsf{skip}\mid c_{1};c_{2}&\text{(commands)}\\\
&\mid&\mathsf{if}\;e\;\mathsf{then}\;c_{1}\;\mathsf{else}\;c_{2}&\\\
&\mid&\mathsf{while}\;e\;\mathsf{do}\;c\;\mathsf{end}&\\\ &\mid&x\leftarrow
e\mid x\leftarrow[e]\mid[e_{1}]\leftarrow e_{2}&\\\
&\mid&x\leftarrow\mathsf{alloc}(e)\mid\mathsf{free}(e)\end{array}$

$\displaystyle s\in\mathcal{S}$
$\displaystyle\triangleq\mathcal{L}\times\mathcal{M}$ (states) $\displaystyle
l\in\mathcal{L}$
$\displaystyle\triangleq\mathsf{var}\rightharpoonup_{\mathrm{fin}}\mathcal{V}$
(local stores) $\displaystyle m\in\mathcal{M}$
$\displaystyle\triangleq\mathbb{I}\times\mathbb{Z}\rightharpoonup_{\mathrm{fin}}\mathcal{V}$
(heaps) $\displaystyle v\in\mathcal{V}$
$\displaystyle\triangleq\mathbb{Z}\uplus\mathbb{B}\uplus\\{\mathsf{nil}\\}\uplus\mathbb{I}\times\mathbb{Z}$
(values) $\displaystyle\mathcal{O}$
$\displaystyle\triangleq\mathcal{S}\uplus\\{\mathsf{error}\\}$ (outcomes)

$\displaystyle\mathbb{I}$ $\displaystyle\triangleq\text{some countably
infinite set}$ $\displaystyle X\rightharpoonup_{\mathrm{fin}}Y$
$\displaystyle\triangleq\text{partial functions $X\rightharpoonup Y$ with
finite domain}$

Figure 3: Syntax and program states $\displaystyle\llbracket x\rrbracket(l,m)$
$\displaystyle\triangleq\begin{cases}l(x)&\text{if $x\in\mathsf{dom}(l)$}\\\
\mathsf{nil}&\text{otherwise}\\\ \end{cases}$ $\displaystyle\llbracket
b\rrbracket(s)$ $\displaystyle\triangleq b$ $\displaystyle\llbracket
n\rrbracket(s)$ $\displaystyle\triangleq n$
$\displaystyle\llbracket\mathsf{nil}\rrbracket(s)$
$\displaystyle\triangleq\mathsf{nil}$ $\displaystyle\llbracket
e_{1}+e_{2}\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}n_{1}+n_{2}&\text{if $\llbracket
e_{1}\rrbracket(s)=n_{1}$ and $\llbracket e_{2}\rrbracket(s)=n_{2}$}\\\
(i,n_{1}+n_{2})&\text{if $\llbracket e_{1}\rrbracket(s)=(i,n_{1})$ and
$\llbracket e_{2}\rrbracket(s)=n_{2}$}\\\ &\text{or $\llbracket
e_{1}\rrbracket(s)=n_{1}$ and $\llbracket e_{2}\rrbracket(s)=(i,n_{2})$}\\\
\mathsf{nil}&\text{otherwise}\end{cases}$ $\displaystyle\llbracket
e_{1}-e_{2}\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}n_{1}-n_{2}&\text{if $\llbracket
e_{1}\rrbracket(s)=n_{1}$ and $\llbracket e_{2}\rrbracket(s)=n_{2}$}\\\
(i,n_{1}-n_{2})&\text{if $\llbracket e_{1}\rrbracket(s)=(i,n_{1})$ and
$\llbracket e_{2}\rrbracket(s)=n_{2}$}\\\
\mathsf{nil}&\text{otherwise}\end{cases}$ $\displaystyle\llbracket e_{1}\times
e_{2}\rrbracket(s)$ $\displaystyle\triangleq\begin{cases}n_{1}\times
n_{2}&\text{if $\llbracket e_{1}\rrbracket(s)=n_{1}$ and $\llbracket
e_{2}\rrbracket(s)=n_{2}$}\\\ \mathsf{nil}&\text{otherwise}\end{cases}$
$\displaystyle\llbracket e_{1}=e_{2}\rrbracket(s)$
$\displaystyle\triangleq(\llbracket e_{1}\rrbracket(s)=\llbracket
e_{2}\rrbracket(s))$ $\displaystyle\llbracket e_{1}\leq e_{2}\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}n_{1}\leq n_{2}&\text{if $\llbracket
e_{1}\rrbracket(s)=n_{1}$ and $\llbracket e_{2}\rrbracket(s)=n_{2}$}\\\
\mathsf{nil}&\text{otherwise}\end{cases}$ $\displaystyle\llbracket
e_{1}\mathbin{\mathsf{and}}e_{2}\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}b_{1}\wedge b_{2}&\text{if $\llbracket
e_{1}\rrbracket(s)=b_{1}$ and $\llbracket e_{2}\rrbracket(s)=b_{2}$}\\\
\mathsf{nil}&\text{otherwise}\end{cases}$ $\displaystyle\llbracket
e_{1}\mathbin{\mathsf{or}}e_{2}\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}b_{1}\vee b_{2}&\text{if $\llbracket
e_{1}\rrbracket(s)=b_{1}$ and $\llbracket e_{2}\rrbracket(s)=b_{2}$}\\\
\mathsf{nil}&\text{otherwise}\end{cases}$
$\displaystyle\llbracket\mathsf{not}\;e\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}\neg b&\text{if $\llbracket
e\rrbracket(s)=b$}\\\ \mathsf{nil}&\text{otherwise}\end{cases}$
$\displaystyle\llbracket\mathsf{offset}\;e\rrbracket(s)$
$\displaystyle\triangleq\begin{cases}n&\text{if $\llbracket
e\rrbracket(s)=(i,n)$}\\\ \mathsf{nil}&\text{otherwise}\end{cases}$ Figure 4:
Expression evaluation $\displaystyle\mathsf{bind}(f,\bot)$
$\displaystyle\triangleq\bot$ $\displaystyle\mathsf{bind}(f,\mathsf{error})$
$\displaystyle\triangleq\mathsf{error}$
$\displaystyle\mathsf{bind}(f,(I,l,m))$
$\displaystyle\triangleq\begin{cases}(I\cup
I^{\prime},l^{\prime},m^{\prime})&\text{if
$f(l,m)=(I^{\prime},l^{\prime},m^{\prime})$}\\\ \mathsf{error}&\text{if
$f(l,m)=\mathsf{error}$}\\\ \bot&\text{otherwise}\end{cases}$
$\displaystyle\mathsf{if}(b,x,y)$
$\displaystyle\triangleq\begin{cases}x&\text{if $b=\mathsf{true}$}\\\
y&\text{if $b=\mathsf{false}$}\\\ \mathsf{error}&\text{otherwise}\end{cases}$
Figure 5: Auxiliary operators $\mathsf{bind}$ and $\mathsf{if}$
$\displaystyle\llbracket\mathsf{skip}\rrbracket_{+}(l,m)\triangleq(\emptyset,l,m)\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\llbracket
c_{1};c_{2}\rrbracket_{+}(l,m)\triangleq\mathsf{bind}(\llbracket
c_{2}\rrbracket_{+},\llbracket c_{1}\rrbracket_{+}(l,m))\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\llbracket\mathsf{if}\;e\;\mathsf{then}\;c_{1}\;\mathsf{else}\;c_{2}\rrbracket_{+}(l,m)\triangleq\mathsf{if}(\llbracket
e\rrbracket(l,m),\llbracket c_{1}\rrbracket_{+}(l,m),\llbracket
c_{2}\rrbracket_{+}(l,m))\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\llbracket\mathsf{while}\;e\;\mathsf{do}\;c\;\mathsf{end}\rrbracket_{+}\triangleq\mathsf{fix}(\lambda\,f\,(l,m).\;\mathsf{if}(\llbracket
e\rrbracket(l,m),\mathsf{bind}(\llbracket
c\rrbracket_{+},f(l,m)),(\emptyset,l,m)))\penalty 50\hskip 20.00003pt plus
0.5fil minus 5.0pt\llbracket x\leftarrow
e\rrbracket_{+}(l,m)\triangleq(\emptyset,l[x\mapsto\llbracket
e\rrbracket(l,m)],m)\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\llbracket
x\leftarrow[e]\rrbracket_{+}(s)\triangleq\begin{cases}(\emptyset,l[x\mapsto
v],m)&\text{if $\llbracket e\rrbracket(s)=(i,n)$ and $m(i,n)=v$}\\\
\mathsf{error}&\text{otherwise}\end{cases}\penalty 50\hskip 20.00003pt plus
0.5fil minus 5.0pt\llbracket[e_{1}]\leftarrow
e_{2}\rrbracket_{+}(s)\triangleq\begin{cases}(\emptyset,l,m[(i,n)\mapsto\llbracket
e_{2}\rrbracket(l,m)])&\text{if $\llbracket e_{1}\rrbracket(s)=(i,n)$ and
$m(i,n)\neq\bot$}\\\ \mathsf{error}&\text{otherwise}\end{cases}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt\llbracket
x\leftarrow\mathsf{alloc}(e)\rrbracket_{+}(l,m)\triangleq\begin{cases}(\\{i\\},l[x\mapsto(i,0)],m[(i,k)\mapsto
0\mid 0\leq k<n])&\text{if $\llbracket e\rrbracket(l,m)=n$ and
$i=\mathsf{fresh}(\mathsf{ids}(l,m))$}\\\
\mathsf{error}&\text{otherwise}\end{cases}\penalty 50\hskip 20.00003pt plus
0.5fil minus
5.0pt\llbracket\mathsf{free}(e)\rrbracket_{+}(l,m)\triangleq\begin{cases}(\emptyset,l,m[(i,k)\mapsto\bot\mid
k\in\mathbb{Z}])&\text{if $\llbracket e\rrbracket(l,m)=(i,0)$ and
$m(i,n)\neq\bot$ for some $n$}\\\ \mathsf{error}&\text{otherwise}\end{cases}$
Figure 6: Command evaluation with explicit allocation sets

This appendix defines the language of Section 2 more formally. Figure 3
summarizes the syntax of programs and repeats the definition of program
states. The syntax is standard for a simple imperative language with pointers.

Figure 4 defines expression evaluation, $\llbracket
e\rrbracket:\mathcal{S}\to\mathcal{V}$. Variables are looked up in the local-
variable part of the state (for simplicity, heap cells cannot be dereferenced
in expressions; the command $x\leftarrow[e]$ puts the value of a heap cell in
a local variable). Constants (booleans, numbers, and the special value
$\mathsf{nil}$ used to simplify error propagation) evaluate to themselves.
Addition and subtraction can be applied both to numbers and to combinations of
numbers and pointers (for pointer arithmetic); multiplication only works on
numbers. Equality is allowed both on pointers and on numbers. Pointer equality
compares both the block identifier and its offset, and while this is harder to
implement in practice than just comparing physical addresses, this is needed
for not leaking information about pointers (see Section 4.2). The special
expression $\mathsf{offset}$ extracts the offset component of a pointer; we
introduce it to illustrate that for satisfying our memory characterization
pointer offsets do not need to be hidden (as opposed to block identifiers).
The less-than-or-equal operator only applies to numbers—in particular,
pointers cannot be compared. However, since we can extract pointer offsets, we
can compare those instead.

The definition of command evaluation employs an auxiliary partial function
that computes the result of evaluating a program along with the set of block
identifiers that were allocated during evaluation. Formally, $\llbracket
c\rrbracket_{+}:\mathcal{S}\rightharpoonup\mathcal{O}_{+}$, where
$\mathcal{O}_{+}$ is an extended set of outcomes defined as
$\mathcal{P}_{\mathrm{fin}}(\mathbb{I})\times\mathcal{S}\uplus\\{\mathsf{error}\\}$.
We then set

$\displaystyle\llbracket c\rrbracket(l,m)$
$\displaystyle=\begin{cases}(l^{\prime},m^{\prime})&\text{if $\llbracket
c\rrbracket_{+}(l,m)=(I,l^{\prime},m^{\prime})$}\\\ \mathsf{error}&\text{if
$\llbracket c\rrbracket_{+}(l,m)=\mathsf{error}$}\\\ \bot&\text{if $\llbracket
c\rrbracket_{+}(l,m)=\bot$}\end{cases}$ $\displaystyle\mathsf{finalids}(l,m)$
$\displaystyle=\begin{cases}\mathsf{ids}(l,m)\setminus I&\text{if $\llbracket
c\rrbracket_{+}(l,m)=(I,l^{\prime},m^{\prime})$}\\\
\emptyset&\text{otherwise}\end{cases}$

To define $\llbracket c\rrbracket_{+}$, we first endow the set
$\mathcal{S}\rightharpoonup\mathcal{O}_{+}$ with the partial order of program
approximation:

$f\sqsubseteq g\ \ \triangleq\ \ \forall s,f(s)\neq\bot\Rightarrow f(x)=g(x)$

This allows us to define the semantics of iteration (the rule for
$\mathsf{while}\;e\;\mathsf{do}\;c\;\mathsf{end}$) in a standard way using the
Kleene fixed point operator $\mathsf{fix}$.

The definition of $\llbracket c\rrbracket_{+}$ appears in Figure 6, where
several of the rules use a $\mathsf{bind}$ operator (Figure 5) to manage the
“plumbing” of the sets of allocated block ids between the evaluation of one
subcommand and the next. The rules for $\mathsf{if}$ and $\mathsf{while}$ also
use an auxiliary operator $\mathsf{if}$ (also defined in Figure 5) that turns
non-boolean guards into errors.

The evaluation rules for $\mathsf{skip}$, sequencing, conditionals,
$\mathsf{while}$, and assignment are standard. The rule for heap lookup,
$x\leftarrow[e]$, evaluates $e$ to a pointer and then looks it up in the heap,
yielding an error if $e$ does not evaluate to a pointer or if it evaluates to
a pointer that is invalid, either because its block id is not allocated or
because its offset is out of bounds. Similarly, the heap mutation command,
$[e_{1}]\leftarrow e_{2}$, requires that $e_{1}$ evaluate to a pointer that is
valid in the current memory $m$ (i.e., such that looking it up in $m$ yields
something other than $\bot$). The allocation command
$x\leftarrow\mathsf{alloc}(e)$ first evaluates $e$ to an integer $n$, then
calculates the next free block id for the current machine state
($\mathsf{fresh}(\mathsf{ids}(l,m))$); it yields a new machine state where $x$
points to the first cell in the new block and where a new block of $n$ cells
is added the heap, all initialized to $0$. Finally, $\mathsf{free}(e)$
evaluates $e$ to a pointer and yields a new heap where every cell sharing the
same block id as this pointer is undefined.

## References

  * [1] Caja. Attack vectors for privilege escalation, 2012.
  * [2] P. Agten, B. Jacobs, and F. Piessens.  Sound modular verification of C code executing in an unverified context.  POPL. 2015.
  * [3] A. Ahmed, M. Fluet, and G. Morrisett.  L${}^{\mbox{3}}$: A linear language with locations.  Fundam. Inform., 77(4):397–449, 2007.
  * [4] A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands.  Termination-insensitive noninterference leaks more than just a bit.  ESORICS. 2008.
  * [5] A. Azevedo de Amorim, M. Dénès, N. Giannarakis, C. Hriţcu, B. C. Pierce, A. Spector-Zabusky, and A. Tolmach.  Micro-policies: Formally verified, tag-based security monitors.  Oakland S&P. 2015.
  * [6] M. Backes, B. Köpf, and A. Rybalchenko.  Automatic discovery and quantification of information leaks.  Oakland S&P, 2009.
  * [7] T. Balabonski, F. Pottier, and J. Protzenko.  Type soundness and race freedom for Mezzo.  FLOPS. 2014.
  * [8] N. Benton and N. Tabareau.  Compiling functional types to relational specifications for low level imperative code. In A. Kennedy and A. Ahmed, editors, TLDI. 2009.
  * [9] K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis.  Defensive JavaScript - building and verifying secure web components.  FOSAD. 2013.
  * [10] D. Chisnall, C. Rothwell, R. N. M. Watson, J. Woodruff, M. Vadera, S. W. Moore, M. Roe, B. Davis, and P. G. Neumann.  Beyond the PDP-11: Architectural support for a memory-safe C abstract machine.  ASPLOS. 2015.
  * [11] J. A. Clause, I. Doudalis, A. Orso, and M. Prvulovic.  Effective memory protection using dynamic tainting.  ASE. 2007.
  * [12] A. A. de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu, D. Pichardie, B. C. Pierce, R. Pollack, and A. Tolmach.  A verified information-flow architecture.  Journal of Computer Security, 24(6):689–734, 2016.
  * [13] J. Devietti, C. Blundell, M. M. K. Martin, and S. Zdancewic.  HardBound: Architectural support for spatial safety of the C programming language.  ASPLOS, 2008.
  * [14] D. Devriese, F. Piessens, and L. Birkedal.  Reasoning about object capabilities with logical relations and effect parametricity.  EuroS&P, 2016.
  * [15] U. Dhawan, C. Hriţcu, R. Rubin, N. Vasilakis, S. Chiricescu, J. M. Smith, T. F. Knight, Jr., B. C. Pierce, and A. DeHon.  Architectural support for software-defined metadata processing.  ASPLOS, 2015.
  * [16] Z. Durumeric, J. Kasten, D. Adrian, J. A. Halderman, M. Bailey, F. Li, N. Weaver, J. Amann, J. Beekman, M. Payer, and V. Paxson.  The matter of Heartbleed.  IMC. 2014.
  * [17] T. Elliott, L. Pike, S. Winwood, P. C. Hickey, J. Bielman, J. Sharp, E. L. Seidel, and J. Launchbury.  Guilt free Ivory.  Haskell. 2015.
  * [18] C. Fournet, N. Swamy, J. Chen, P.-É. Dagand, P.-Y. Strub, and B. Livshits.  Fully abstract compilation to JavaScript.  POPL. 2013.
  * [19] J. A. Goguen and J. Meseguer.  Security policies and security models.  S&P, 1982.
  * [20] M. Hicks.  What is memory safety?  http://www.pl-enthusiast.net/2014/07/21/memory-safety/, 2014.
  * [21] ISO.  ISO C standard 1999.  Technical report, ISO, 1999.  ISO/IEC 9899:1999 draft.
  * [22] S. Jana and V. Shmatikov.  Memento: Learning secrets from process footprints.  Oakland S&P. 2012.
  * [23] J. Kang, C. Hur, W. Mansky, D. Garbuzov, S. Zdancewic, and V. Vafeiadis.  A formal C memory model supporting integer-pointer casts.  PLDI. 2015\.
  * [24] R. Krebbers.  The C standard formalized in Coq.  PhD thesis, Radboud University Nijmegen, 2015.
  * [25] A. Kwon, U. Dhawan, J. M. Smith, T. F. Knight, Jr., and A. DeHon.  Low-fat pointers: compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security.  CCS. 2013.
  * [26] X. Leroy and S. Blazy.  Formal verification of a C-like memory model and its uses for verifying program transformations.  JAR, 41(1):1–31, 2008.
  * [27] S. Maffeis, J. C. Mitchell, and A. Taly.  Object capabilities and isolation of untrusted web applications.  Oakland S&P, 2010.
  * [28] K. Memarian, J. Matthiesen, J. Lingard, K. Nienhuis, D. Chisnall, R. N. M. Watson, and P. Sewell.  Into the depths of C: elaborating the de facto standards.  PLDI, 2016.
  * [29] L. A. Meyerovich and V. B. Livshits.  Conscript: Specifying and enforcing fine-grained security policies for javascript in the browser.  Oakland S&P, 2010.
  * [30] G. Morrisett, M. Felleisen, and R. Harper.  Abstract models of memory management.  FPCA. 1995.
  * [31] S. Nagarakatte, J. Zhao, M. M. K. Martin, and S. Zdancewic.  SoftBound: highly compatible and complete spatial memory safety for C.  PLDI. 2009.
  * [32] S. Nagarakatte, J. Zhao, M. M. K. Martin, and S. Zdancewic.  CETS: compiler enforced temporal safety for C.  ISMM. 2010.
  * [33] G. C. Necula, J. Condit, M. Harren, S. McPeak, and W. Weimer.  CCured: type-safe retrofitting of legacy software.  TOPLAS, 27(3):477–526, 2005.
  * [34] A. M. Pitts.  Nominal Sets: Names and Symmetry in Computer Science.  Cambridge University Press, New York, NY, USA, 2013.
  * [35] F. Pottier and J. Protzenko.  Programming with permissions in Mezzo.  ICFP, 2013.
  * [36] J. C. Reynolds.  Separation logic: A logic for shared mutable data structures.  LICS. 2002.
  * [37] The Rust programming language.  http://www.rust-lang.org, 2017.
  * [38] C. Schlesinger, K. Pattabiraman, N. Swamy, D. Walker, and B. G. Zorn.  Modular protections against non-control data attacks.  JCS, 22(5):699–742, 2014.
  * [39] G. Smith.  On the foundations of quantitative information flow.  FoSSaCS. 2009.
  * [40] D. Stefan, P. Buiras, E. Z. Yang, A. Levy, D. Terei, A. Russo, and D. Mazières.  Eliminating cache-based timing attacks with instruction-based scheduling.  ESORICS. 2013.
  * [41] N. Swamy, M. W. Hicks, G. Morrisett, D. Grossman, and T. Jim.  Safe manual memory management in Cyclone.  SCP, 62(2):122–144, 2006.
  * [42] D. Swasey, D. Garg, and D. Dreyer.  Robust and compositional verification of object capability patterns.  To appear at OOPSLA, 2017.
  * [43] L. Szekeres, M. Payer, T. Wei, and D. Song.  SoK: Eternal war in memory.  IEEE S&P. 2013.
  * [44] A. Taly, Ú. Erlingsson, J. C. Mitchell, M. S. Miller, and J. Nagra.  Automated analysis of security-critical javascript apis.  Oakland S&P. 2011.
  * [45] A. Turon.  Rust: from POPL to practice (keynote).  POPL. 2017\.
  * [46] C. Williams.  Oracle’s Larry Ellison claims his Sparc M7 chip is hacker-proof – errr… The Register, 2015.
  * [47] E. Z. Yang and D. Mazières.  Dynamic space limits for Haskell.  PLDI. 2014.
  * [48] H. Yang and P. W. O’Hearn.  A semantic basis for local reasoning.  FoSSaCS. 2002.
  * [49] D. Zhang, A. Askarov, and A. C. Myers.  Language-based control and mitigation of timing channels.  PLDI. 2012\.