# An Information Flow Monitor-Inlining Compiler for Securing a Core of JavaScript

José Fragoso Santos, Tamara Rezk

► To cite this version:

José Fragoso Santos, Tamara Rezk. An Information Flow Monitor-Inlining Compiler for Securing a Core of JavaScript. 29th IFIP International Information Security Conference (SEC), Jun 2014, Marrakesh, Morocco. pp.278-292, 10.1007/978-3-642-55415-5_23. hal-01087374

HAL Id: hal-01087374

https://inria.hal.science/hal-01087374

Submitted on 25 Nov 2014

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# An Information Flow Monitor-Inlining Compiler for Securing a Core of JavaScript

José Fragoso Santos and Tamara Rezk

INRIA

firstname.lastname@inria.fr

**Abstract.** Web application designers and users alike are interested in isolation properties for trusted JavaScript code in order to prevent confidential resources from being leaked to untrusted parties. Noninterference provides the mathematical foundation for reasoning precisely about the information flows that take place during the execution of a program. Due to the dynamicity of the language, research on mechanisms for enforcing noninterference in JavaScript has mostly focused on dynamic approaches. We present the first information flow monitor inlining compiler for a realistic core of JavaScript. We prove that the proposed compiler enforces termination-insensitive noninterference and we provide an implementation that illustrates its applicability.

## 1 Introduction

Client-side JavaScript programs often include untrusted code dynamically loaded from third-party code providers, such as online advertisers. This issue raises the need for enforcement mechanisms that isolate trusted code from code that comes from untrusted sources. Such mechanisms must prevent trusted programs from leaking confidential resources. Noninterference [13] is an expressive and elegant property that formally defines secure information flow, thus being commonly used as a soundness criteria for dynamic and static analyses that aim at enforcing secure information flow.

Due to the dynamic nature of JavaScript, research on mechanisms to check the compliance of JavaScript programs with noninterference has mostly focused on dynamic approaches. In practice, there are two main approaches for implementing a JavaScript information flow monitor: either one modifies a JavaScript engine so that it additionally implements the security monitor (as in [9]), or one inlines the monitor in the original program (as in [7, 11]). The second approach, which we follow, has the advantage of being *browser-independent*. We present the first compiler that inlines an information flow monitor for a subset of JavaScript that we call Core JavaScript. Core JavaScript includes the main standard features of the language, such as objects with prototypical inheritance and closures, as well as non-standard features, such as several unusual ways for interacting with the *global object* – a special object that binds global variables.

The proposed compiler is proven sound with respect to a standard definition of input-output termination insensitive noninterference for monitors. Hence, in
the considered setting, attackers are assumed no to be able to observe the contents of intermediate memory states or to use divergent executions as a means of disclosing confidential resources. Informally, we prove that the execution of a compiled program only goes through if it is noninterferent; otherwise, the constraints inlined in the program by the compiler cause it to diverge. The paper is divided in two main sections. Section 2 presents an information flow monitored semantics for Core JavaScript that is proven sound, that is, it is proven to enforce termination-insensitive noninterference. The proposed monitored semantics differs from a previous monitor for enforcing secure information flow in a realistic core of JavaScript [9] in that it was specifically designed to guide the implementation of an inlining compiler. Section 3 presents an inlining compiler that rewrites Core JavaScript programs in order to simulate their execution in the monitor. The compiler is proven correct, meaning that the execution of a program goes through in the monitor if and only if the execution of its instrumentation by the inlining compiler goes through in the original semantics. We have implemented a prototype of the proposed compiler, which supports a subset of JavaScript semantics larger than the one modeled in Core JavaScript and that is available online at [1] together with a broad set of examples and a full version of this paper that includes the proofs of the main theorems.

## 1.1 Core JavaScript Syntax and Semantics

The syntax of Core JavaScript is given in Figure 1. Some expressions are annotated with one or two unique indexes for use by the compiler, which are omitted when not needed. In the examples, we use *o.p* as an abbreviation for *o*[“p”]. Objects are the fundamental data type in JavaScript. Informally, an object can be seen as a collection of named values. At the semantic level, we model objects as partial functions from strings, taken from a set *Str*, to values. JavaScript values comprise: (1) primitive values (taken from a set *Prim*), (2) object references (taken from a set *Ref*), and (3) parsed function literals (for which we use the lambda notation: `λx.var y₁, ..., yₙ; e`). *Prim* includes strings, numbers, and booleans, as well as two special values *null* and *undefined*. The strings in the domain of an object are called its *properties*. Some properties are internal and therefore can neither be changed nor read by programs. For clarity, these properties are prefixed with an “@”. Every expression that creates an object in memory yields a free non-deterministically chosen reference that points to it. Hence, references can be viewed as pointers to objects. Given an object *o*, we use `#o` to denote the reference that points to it. Finally, a *memory* µ is a partial mapping from references to objects.

*Notation.* We use the notation: (1) [*p*₀ ↦ *v*₀, ..., *p*ₙ ↦ *v*ₙ] for the partial function that maps *p*₀ to *v*₀, ..., and *p*ₙ to *v*ₙ resp., (2) *f* [*p*₀ ↦ *v*₀, ..., *p*ₙ ↦ *v*ₙ] for the function that coincides with *f* everywhere except in *p*₀, ..., *p*ₙ, which are otherwise mapped to *v*₀, ..., *v*ₙ resp., (3) *f*|*P* for the restriction of *f* to *P* (provided it is included in its domain), and (4) *f*(*r*)(*p*) for (*f*(*r*))(*p*), that is, the application of the image of *r* by *f* (which is assumed to be a function) to *p*. Furthermore, we use *iff* as an abbreviation for *if and only if*.
<table><thead><tr><th>e</th><th>::=</th><th>v<sup>i</sup></th><th>value</th><th>function<sup>i</sup>(x){var y<sub>1</sub>,...,y<sub>n</sub>; e}</th><th>function literal</th></tr></thead><tbody><tr><td></td><td>|</td><td><b>this</b><sup>i</sup></td><td>this keyword</td><td>{}<sup>i</sup></td><td>object literal</td></tr><tr><td></td><td>|</td><td>e<sub>0</sub> op<sup>i</sup></td><td>binary operation</td><td>e<sub>0</sub>(e<sub>1</sub>)<sup>i</sup></td><td>function call</td></tr><tr><td></td><td>|</td><td>x<sup>i</sup></td><td>variable</td><td>e<sub>0</sub>[e<sub>1</sub>](e<sub>2</sub>)<sup>i</sup></td><td>method call</td></tr><tr><td></td><td>|</td><td>x=e</td><td>variable assignment</td><td>e<sub>0</sub>, e<sub>1</sub></td><td>sequence</td></tr><tr><td></td><td>|</td><td>e<sub>0</sub>[e<sub>1</sub>]<sup>i</sup></td><td>property look-up</td><td>e<sub>0</sub>?<sup>i,j</sup> (e<sub>1</sub>) : (e<sub>2</sub>)</td><td>conditional</td></tr><tr><td></td><td>|</td><td>e<sub>0</sub>[e<sub>1</sub>]=e<sub>2</sub></td><td>property assignment</td><td></td><td></td></tr></tbody></table>

Where *e*, *e*<sub>0</sub>, *e*<sub>1</sub> and *e*<sub>2</sub> range over the set of expressions, *i* and *j* range over the set of program indexes, *x*, *y*<sub>1</sub>, ..., *y*<sub>n</sub> range over the set of variable names, and *op* ranges over the set of binary operators.

<caption>**Fig. 1.** Syntax of Core JavaScript</caption>

**Function Calls and Variables.** As in JavaScript, we model scope *via scope objects* [2, 10]. Every function call triggers the creation of a scope object which maps its formal parameter as well as the variables declared in its body to their corresponding values. A scope object is said to be *active* if it is associated with the function that is currently executing. Furthermore, every scope object defines a property `@scope` that points to the scope object that was active when the corresponding function literal was evaluated. The sequence of scope objects that can be accessed from a given scope object through the respective `@scope` properties is called a *scope-chain*. The *global object*, which is assumed to be pointed by a fixed reference `#glob`, is the object that is at the end of every scope-chain and therefore it is the object that binds *global variables*. In order to determine the value associated with a given variable, one has to inspect all objects in the scope-chain that starts in the *active* scope object. This behavior is modeled by the semantic relation $\mathcal{R}_{Scope}$, given in Definition 1. If $\langle\mu, r_0, x\rangle \mathcal{R}_{Scope} r_1$, then $r_1$ is the reference that points to the scope object that is closest to the one pointed by $r_0$ in the corresponding scope-chain (whose objects are in the range of $\mu$) and which defines a binding for variable $x$.

**Definition 1 (Scope Inspection Procedure $\mathcal{R}_{Scope}$).** The relation $\mathcal{R}_{Scope}$ is recursively defined as follows:

$$ \begin{array}{l} \text{NULL} \\ \langle\mu, \text{null}, x\rangle \mathcal{R}_{Scope} \text{ null} \\ \text{BASE} \\ \quad \frac{x \in \text{dom}(\mu(r))}{\langle\mu, r, x\rangle \mathcal{R}_{Scope} r} \\ \text{LOOK-UP} \\ \quad \frac{x \notin \text{dom}(\mu(r))}{\langle\mu, \mu(r, @scope), x\rangle \mathcal{R}_{Scope} r'} \\ \quad \frac{\langle\mu, r, x\rangle \mathcal{R}_{Scope} r'}{\langle\mu, r, x\rangle \mathcal{R}_{Scope} r'} \end{array} $$

**Function Literals and Variable Assignments.** The evaluation of a function literal yields a reference to an object, called a *function object*, that stores its parsed counterpart. More specifically, since every function is executed in the environment in which the corresponding function literal was evaluated, every function object defines the following two properties: (1) `@code` that stores the parsed function literal and (2) `@fscope` that stores the reference that points to the scope object that was active when the corresponding function literal was evaluated. Assuming that the global object defines a variable *out* originally set to `null`, the evaluation of the program presented below on the left yields the
value 0 and creates in memory the list of objects displayed below on the right:

$$
\begin{align*}
(\mathbf{function}(x)\{ & o_s^0 = [@scope \mapsto \#glob, x \mapsto 0, g \mapsto o_g, h \mapsto o_h] \\
& \mathbf{var} g, h; \\
& o_s^g = [@scope \mapsto \#o_s^0, x \mapsto 1] \\
& g = \mathbf{function}(x)\{h(2)\}, \\
& o_s^h = [@scope \mapsto \#o_s^0, y \mapsto 2] \\
h = \mathbf{function}(y)\{out = x\}, & o_0 = [@code \mapsto \lambda x.\mathbf{var} g, h; \hat{e}, @fscope \mapsto \#glob] \\
& g(1) \\
& o_g = [@code \mapsto \lambda x.h(2), @fscope \mapsto \#o_g^0] \\
\}) (0); & o_h = [@code \mapsto \lambda y.out = x, @fscope \mapsto \#o_h^0]
\end{align*}
$$

where (1) $o_s^0$, $o_s^g$, and $o_s^h$ correspond to the scope objects associated with the invocation of the anonymous function, of function $g$, and of function $h$, respectively, (2) objects $o_0$, $o_g$, and $o_h$ correspond to their respective function objects, and (3) $\hat{e}$ corresponds to the body of the anonymous function. After the execution of this program, the global object maps `out` to 0 and not to 1, because the scope object that is closest to $o_s^h$ and which defines a binding for $x$ is $o_s^0$ and not $o_s^g$ (which does not belong to the scope-chain of $o_s^h$).

### Object Literals and Property Look-ups.
Core JavaScript features prototypical inheritance. This means that every object (except scope objects and function objects) defines a property `_prot_` that stores a reference to its prototype. When trying to look-up the value of a property `p` of an object `o`, the semantics first checks whether `p` ∈ `dom(o)`. If `p` ∈ `dom(o)`, the property look-up yields `o(p)`, otherwise the semantics checks whether the prototype of `o` defines a property named `p`, and so forth. The sequence of objects that can be accessed from a given object through the respective `_prot_` properties is called a *prototype-chain*. The prototype-chain inspection procedure is emulated by the semantic relation $R_{Proto}$, given in Definition 2. If $\langle\mu, r, m, \Gamma, \Sigma\rangle R_{Proto} \langle r', \sigma\rangle$, then $r'$ is the closest reference to `r` in its corresponding prototype-chain (whose objects are in the range of $\mu$) that defines a binding for `m` (we ignore, by now, the remaining elements of the relation, since they are used by the monitored semantics and not by the original semantics). The evaluation of an object literal yields a free non-deterministically chosen reference that points to a new object that only defines a property `_prot_` originally set to `null`. Hence, the evaluation of $o_0 = \{\}$, $o_0.p = 0$, $o_1 = \{\}$, $o_1._prot_ = o_0$, $o_1.p$ yields 0, because, although $o_1$ does not define property `p`, its prototype does. When looking-up the value of a property `p` in an object `o`, if `p` is not defined in the whole prototype-chain of `o`, instead of yielding an error, the semantics yields `undefined`. Therefore, the expression $o = \{\}$, `o.p` evaluates to `undefined`.

**Definition 2 ($R_{Proto}$).** The relation $R_{Proto}$ is recursively defined as follows:

$$
\begin{array}{ll}
\texttt{NULL} & \texttt{BASE} \\
\langle\mu, \texttt{null}, m, \Gamma, \Sigma\rangle R_{Proto} \langle\texttt{null}, \perp\rangle & \displaystyle\frac{m \in \text{dom}(\mu(r))}{\langle\mu, r, m, \Gamma, \Sigma\rangle R_{Proto} \langle r, \perp\rangle}
\end{array}
$$

$$
\begin{array}{l}
\textsc{look-up} \\
m \notin \text{dom}(\mu(r)) \qquad r' = \mu(r)(\text{\textit{-prot-}}) \\
\langle\mu, \mu(r)(\text{\textit{-prot-}}), m, \Gamma, \Sigma\rangle R_{Proto} \langle r'', \sigma\rangle \\
\sigma' = \Gamma(r)(\text{\textit{-prot-}}) \sqcup \Sigma(r) \sqcup \sigma \\
\hline
\langle\mu, r, m, \Gamma, \Sigma\rangle R_{Proto} \langle r', \sigma'\rangle
\end{array}
$$
*Method Calls and the this keyword.* Functions whose references are assigned to properties of an object are called its *methods*. A function can be either invoked as a normal function or as a method. When calling a function as a method, the *this* keyword is bound to the corresponding object, otherwise it is bound to the global object. Therefore, every scope object defines a property *@this* (that was omitted in the first example) that holds the value of the *this* keyword in that scope. We further remark that given an object *o*, every method *m* accessible from *o* through its prototype-chain can be called as a method of *o*. Hence, suppose that in a memory *μ*, the global object defines two variables *o*₀ and *o*₁ that hold references to `[-prot_ ↦ null, f ↦ #of]` and `[-prot_ ↦ #o₀]` respectively, where `#of` is the reference of a given function object. In the evaluation of expression *o*₁.f(0), the semantics starts by creating a scope object in which property *@this* is set to `#o₁` and then proceeds with the evaluation of the body of *f*.

The remaining program constructs have the usual semantics, which can be understood from the formal definition. We make use of a big-step semantics for Core JavaScript with the following shape: $r \vdash \langle\langle\mu, e\rangle\rangle \Downarrow \langle\langle\mu', v\rangle\rangle$, where *r* is the reference of the active scope object, *μ* and *μ'* are the initial and final memories respectively, *e* the expression to be evaluated, and *v* the value to which it evaluates. Due to space constraints we choose not to give its formal definition here. Instead, we only present its monitored version, $\Downarrow_{IF}$ (Figure 2). In order to obtain $\Downarrow$ from $\Downarrow_{IF}$, one simply has to remove from $\Downarrow_{IF}$ the monitor constraints. Thus, the following correspondence between the two semantics can be straightforwardly proven:

**Lemma 1 (Semantics Correspondence).** If $r_s, \sigma_{pc} \vdash \langle\mu, s, \Gamma\rangle \Downarrow_{IF} \langle\mu', v, \Gamma', \sigma\rangle$ then $r_s \vdash \langle\langle\mu, s\rangle\rangle \Downarrow \langle\langle\mu', v\rangle\rangle$.

## 2 Monitoring Secure Information Flow

*Specifying Security Policies.* The specification of security policies usually relies on two key elements: a lattice of security levels and a labeling that maps resources to security levels. In the examples, we use $\mathcal{L} = \{H, L\}$ with $L \le H$, meaning that resources labeled with level *L* (low) are less confidential than resources labeled with *H* (high). Hence, after the execution of a program, resources labeled with *H* are allowed to depend on resources originally labeled with *L*, but not the opposite, since that would entail an information leak. In the following, we always assume that $\le$ and $\sqcup$ correspond to the order relation and the least upper bound on security levels respectively. A security labeling is a pair $\langle\Gamma, \Sigma\rangle$ where $\Gamma: \mathcal{R}ef \to Str \to \mathcal{L}$ maps each property in every object to a security level and $\Sigma: \mathcal{R}ef \to \mathcal{L}$ maps every reference to the structure security level [9] of the corresponding object. Hence, given an object *o* pointed by a reference $r_o, \Gamma(r_o)(p)$ is the security level associated with *o*'s property *p* and $\Sigma(r_o)$ is the structure security level of *o*. Notice that, since every variable is modeled as a property of a given scope object, $\Gamma$ also maps variables to the corresponding security levels. Hence, variables and properties are treated uniformly. In the
examples, we assume that variables *h* and *l* are respectively labeled with levels *H* and *L*. The structure security level of an object can be understood as the security level associated with its domain. The need to associate a security level with the domain of every object arises because it is possible for a program to leak information *via* the domain of an object. For instance, after the evaluation of *o* = {}, *h* ? (*o*.*p* = 0) : (null), *l* = *o*.*p*<sub>*</sub>, the final value of the low variable *l* depends on the initial value of the high variable *h*. Precisely, when *h* ∈ {false, 0, null, *undefined*}, property *p* is not added to the domain of *o* and *l* is set to *undefined*, whereas in all other cases, both property *p* and variable *l* are set to 0. Finally, we observe that initial memories are assumed to include a global object for the binding of global variables. Accordingly, initial labelings apply both to the global object as well as the objects that are initially accessible through the global object. We say that a memory *μ* is *well-labeled* by ⟨Γ, Σ⟩ if and only if dom(Γ) = dom(Σ) ⊆ dom(μ) and for every reference *r* ∈ dom(Γ), dom(Γ(r)) ⊆ dom(μ(r)).

**Low-Equality.** We introduce a notion of indistinguishability between memories that models the “power” of an attacker that can only observe resources up to a given security level $\sigma$, called low-equality, denoted by $\approx_{\beta,\sigma}$. Informally, two labeled memories are low-equal at level $\sigma$ if they coincide in the resources labeled with levels $\le \sigma$. Since references are non-deterministically chosen we need to be able to relate observable references in two different memories. To this end, we parameterize the low-equality relation with a partial injective function $\beta : \mathcal{R}ef \to \mathcal{R}ef$ [5] that relates observable references. The low-equality definition relies on a binary relation on values, named $\beta$-equality and denoted by $\sim_{\beta}$, given in Definition $\ref{def:beta-equality}$: two objects are $\beta$-equal if they have the same domain and all their properties are $\beta$-equal, primitive values and parsed functions are $\beta$-equal if they are equal, and two references $r_0$ and $r_1$ are $\beta$-equal if $\beta(r_0) = r_1$.

In the following, given a property labeling $\Gamma$, a reference $r$, and security level $\sigma$, we denote by $\Gamma(r)|_{\sigma}$, the set of observable properties in $\Gamma(r)$ at level $\sigma$: $\Gamma(r)|_{\sigma} = \{p | \Gamma(r)(p) \le \sigma\}$.

**Definition 3 (Low-Equality $\approx_{\beta,\sigma}$).** Two memories $\mu_0$ and $\mu_1$ are said to be low equal with respect to $\langle\Gamma_0, \Sigma_0\rangle$ and $\langle\Gamma_1, \Sigma_1\rangle$, security level $\sigma$, and function $\beta$, written $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta,\sigma} \mu_1, \Gamma_1, \Sigma_1$, iff for all references $r_0, r_1 \in \text{dom}(\beta)$ such that $r_1 = \beta(r_0)$, the following holds: (1) The observable domains coincide: $\Gamma_0(r_0)|_{\sigma} = \Gamma_1(r_1)|_{\sigma} = P$. (2) The objects coincide in their observable domains: $\mu_0(r_0)|_P \sim_{\beta} \mu_1(r_1)|_P$. (3) Either the domains of both objects are not observable, or they are both observable and completely coincide: $(\Sigma_0(r_0) \le \sigma \lor \Sigma_1(r_1) \le \sigma) \Rightarrow \Sigma_0(r_0) \sqcup \Sigma_1(r_1) \le \sigma \land \text{dom}(\mu_0(r_0)) = \text{dom}(\mu_1(r_1)).$

**Monitored semantics.** The rules of the monitored semantic relation, $\Downarrow_{IF}$, defined in Figure 2, have the form $r, \sigma_{pc} \vdash \langle\mu, e, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu', v, \Gamma', \Sigma', \sigma\rangle$, where $\sigma_{pc}$ is the security level of the execution context, $\langle\Gamma, \Sigma\rangle$ and $\langle\Gamma', \Sigma'\rangle$ are the initial and final labelings, and $\sigma$ is the *reading effect* of $e$ [13]. The remaining elements keep their original meaning in $\Downarrow$. The *reading effect* of an expression is defined as the least upper bound on (1) the levels of the resources on
which the value to which it evaluates depends and (2) the level of the current context, $\sigma_{pc}$. The monitored execution of an expression e can be interpreted as an extension of the unmonitored execution of e that additionally performs the abstract execution of e on the abstract memory given by $\Gamma$. Hence, the computation of $\Gamma'$ and $\sigma$ precisely mirrors the computation of $\mu'$ and $v$. The monitored semantics makes use of a relation $\mathcal{R}_{NewScope}$ given in Definition 4, which models the storing of a new scope object in memory. Hence, if $\langle\mu, \Gamma, \Sigma, r_f, v_{arg}, r_{this}, \sigma_{pc}, \sigma_{arg}\rangle \mathcal{R}_{NewScope} \langle\mu', e, \Gamma', \Sigma', r', \sigma'_{pc}\rangle$, then: (1) $\mu'$ and $\langle\Gamma', \Sigma'\rangle$ are the memory and labeling obtained from $\mu$ and $\langle\Gamma, \Sigma\rangle$ by the allocation of the new scope object in the free reference $r'$; (2) $r_f$ is the reference to the function that is going to be executed, e its body, $v_{arg}$ the argument to be used, $\sigma_{pc}$ the level of the context in which the function was invoked, $\sigma_{arg}$ the reading effect of the actual argument, and $r_{this}$ the reference to the object to be used as this; and (3) $\sigma'_{pc}$ is the security level at which the execution of e takes place.

**Definition 4** ($\mathcal{R}_{NewScope}$). For any two memories $\mu$ and $\mu'$, two labelings $\langle\Gamma, \Sigma\rangle$ and $\langle\Gamma', \Sigma'\rangle$, three references $r_f$, $r_{this}$, and $r'$, a value $v_{arg}$, an expression e, and three security levels $\sigma_{pc}$, $\sigma_{arg}$, and $\sigma'_{pc}$:

$$ \langle\mu, \Gamma, \Sigma, r_f, v_{arg}, r_{this}, \sigma_{pc}, \sigma_{arg}\rangle \mathcal{R}_{NewScope} \langle\mu', e, \Gamma', \Sigma', r', \sigma'_{pc}\rangle $$

holds if and only if:

1. $\lambda x. \{\text{var } y_1, \dots, y_n; e\} = \mu(r_f)(@code)$,

2. $r = \mu(r_f)(@fscope)$,

3. $r' \notin \text{dom}(\mu)$,

4. $\sigma'_{pc} = \sigma_{pc} \sqcup \Gamma(r_f)(@fscope)$,

5. $\mu' = \mu \left[ r' \mapsto \left[ \begin{array}{l} @scope \mapsto r, x \mapsto v_{arg}, @this \mapsto r_{this}, \\ y_1 \mapsto \text{undefined}, \dots, y_n \mapsto \text{undefined} \end{array} \right] \right]$,

6. $\Sigma' = \Sigma[r' \mapsto \sigma'_{pc}]$,

7. $\Gamma' = \Gamma[r' \mapsto \left[ \begin{array}{l} @scope \mapsto \sigma'_{pc}, x \mapsto \sigma'_{pc} \sqcup \sigma_{arg}, @this \mapsto \sigma'_{pc}, \\ y_1 \mapsto \sigma'_{pc}, \dots, y_n \mapsto \sigma'_{pc} \end{array} \right]$,

for some variables $x, y_1, \dots, y_n$.

Among the possible techniques to design a purely dynamic sound information flow monitor, we choose to follow the no-sensitive-upgrade discipline [3]. Essentially, the monitor blocks executions that try to upgrade the value of low resources within high contexts. To illustrate the idea of this strategy, consider the following program: $h ? (l = 0) : (null)$. Suppose that the monitor allows the execution of this program to go through in an initial memory that maps $h$ to 1 just raising the level of $l$ to $H$ (which constitutes a sensitive upgrade). If this same program is executed in a memory that maps $h$ to 0; in the final memory, $l$ is labeled with $L$ and therefore it is visible. Hence, after executing this program starting from two indistinguishable memories, we obtain two memories that are distinguishable by an attacker at level $L$, meaning that the attacker has learned something about the confidential resources of the program. Concretely, by allowing the sensitive upgrade in this example, we let an attacker know whether $h$ belongs or not to $\{null, \text{undefined}, 0, false\}$.
*Function/Method Calls, Conditional Expressions, and Function Literals.* The only non-trivial part concerning the monitoring of these four types of expressions has to do with how the first three update the level of the execution context in which their subexpressions are evaluated. Observe that $\sigma_{pc}$ must always be higher than or equal to the security levels of the resources that were used to decide: (1) which branch to take in a conditional expression whose code is still executing and (2) which function/method to execute in a function/method call expression whose execution is still being performed. For instance, consider the following expression:

$$f_1 = \text{function}(x)\{l = 0\}, f_2 = \text{function}(x)\{l = 1\}, h ? (f = f_1) : (f = f_2), f() \quad (1)$$

Since the final value of the low variable $l$ depends on the original value of the high variable $h$, this program does not abide by the security policy and is therefore considered *illegal*. Hence, independently of the branch taken in the execution of the conditional, in the evaluation of the corresponding expression, the monitor must be aware that the decision to take that branch depends on the value of a high variable. Analogously, when executing the body of the function assigned to $f$, the monitor must be aware that the fact that it is executing that function and not another does also depend on the value of a high variable. Hence, $\sigma_{pc}$ must be upgraded to high both during the execution of the taken branch of the conditional and during the execution of the body of the function bound to $f$. Additionally, $\sigma_{pc}$ must also take into account the level of the context in which the function literal corresponding to the function that is currently evaluating was itself evaluated. Consider the expression:

$$f = h ? (\text{function}(x)\{l = 0\}) : (\text{function}(x)\{l = 1\}), f() \quad (2)$$

This program is illegal because after its execution, depending on the value of the high variable $h$, the low variable $l$ can be either 0 or 1. To account for this type of leak, when a function literal is evaluated the level of the current context is stored in $\Gamma(r_f)(@fscope)$. Hence, every time the corresponding function is called, it is executed in a context whose level is set to be $\geq \Gamma(r_f)(@fscope)$.

*Variable Assignments and Property Updates.* In accordance with the no-sensitive-upgrade discipline, the monitor only allows a variable $x$ (or a property $p$ of an object $o$) to be upgraded in a context whose level is lower than or equal to its current level: $\sigma_{pc} \leq \Gamma(r_{pc})(x)$ (or $\sigma_{pc} \leq \Gamma(\#o)(p)$). Therefore, considering the expression given in Code Snippet (1), if $f$ is a high variable, the assignments inside the branches of the conditional are allowed to go through. However, the assignment inside the body of the function bound to $f$ is not, because the value of the execution context is high, whereas the level of the variable that is being updated is low. Notice, however, that, in the Rule [PROPERTY ASSIGNMENT] (for the case in which the property to be assigned is defined), the constraint is not $\sigma_{pc} \leq \Gamma(\#o)(p)$, but instead $\sigma_0 \sqcup \sigma_1 \leq \Gamma(\#o)(p)$. Observe that, since the monitor ensures that $\sigma_{pc} \leq \sigma_0$ and $\sigma_{pc} \leq \sigma_1$, the latter constraint subsumes the former. The need for this stricter constraint arises from the fact that in a property assignment, the assignment that actually takes place depends on the reading effects of (1) the expression that evaluates to the reference of the object of the property to be assigned and (2) the expression that evaluates to the actual property whose value is to be updated. Suppose, for instance, that variable
o holds an object only containing low properties. Then, even if $\sigma_{pc}$ is low, the expression $o[h] = 0$ is illegal, because depending on the value of $h$, it updates the value of a different low property. One cannot simply upgrade the level of the property to which $h$ evaluates to $H$ because that would constitute a sensitive upgrade, since for different values of $h$, an attacker at level $L$ would see different properties disappearing from the observable domain of $o$.

**Property Look-ups, Property Creation Expressions, and Object Literals.** When a program looks up the value of a property $p$ in an object $o$, if $p \notin \text{dom}(o)$, the security level associated with the property look-up expression must be equal to or higher than the structure security level of $o$, because this property look-up leaks information about its domain. In fact, since every property look-up searches the prototype-chain of the corresponding object, the security monitor has to take into account the structure security level as well as the level of property `-prot-` of every object traversed during the prototype-chain inspection procedure (which corresponds to $\sigma$ in $\langle\mu, r, m, \Gamma, \Sigma\rangle \mathcal{R}_{Proto} \langle r', \sigma'\rangle$). For example, given a memory:

$$ \mu = [\#o_0 \mapsto [p \mapsto 1, -prot_- \mapsto null], \#o_1 \mapsto [-prot_- \mapsto \#o_0], \#glob \mapsto [o_1 \mapsto \#o_1]] \quad (3) $$

and a labeling $\langle\Gamma, \Sigma\rangle$, such that $\Gamma$ maps all properties in every object in the range of $\mu$ to $L$ and $\Sigma = [\#o_0 \mapsto L, \#o_1 \mapsto H, \#glob \mapsto L]$, the reading effect of the expression $o_1.p$ must be $H$, because it leaks information about the domain of $o_1$ whose level is $H$. Naturally, when an object literal is evaluated, its structure security level is set to the level of the execution context, because the creation of the object is visible at that level. Finally, when creating a new property in an object $o$, the monitor checks whether the structure security level of $o$ ($\Sigma(\#o)$) is at least as high as the reading effects of: (1) the expression that evaluates to $\#o$ ($\sigma_0$) and (2) the expression that evaluates to the name of the property to create ($\sigma_1$). Recall that both $\sigma_0$ and $\sigma_1$ are at least as high as the level of the execution context. Hence, the monitor does also implicitly require that $\sigma_{pc} \le \Sigma(\#o)$. To illustrate the need for these constraints, consider the expression $o_0 = \{\}, o_1 = \{\}, h? (h = o_0) : (h = o_1), h.p = 0, l = o_1.p$. Naturally, this program is illegal because the final value of the low variable $l$ depends on the original value of the high variable $h$. In fact, since the level of $h$ is not lower than or equal to the structure security level of any of the two objects, the monitor blocks the property creation.

**Noninterferent Monitor.** We say that a security monitor is noninterferent iff it preserves the low-equality relation. Informally, an information flow monitor is noninterferent iff, for any program $e$, whenever an attacker cannot distinguish two labeled memories before executing $e$, then the attacker is also unable to distinguish the final memories.

**Theorem 1 (Non-Interferent Monitor).** For any expression $e$, memories $\mu$ and $\mu'$, respectively labeled by $\langle\Gamma, \Sigma\rangle$ and $\langle\Gamma', \Sigma'\rangle$, reference $r$, security levels $\sigma_{pc}$ and $\sigma$, and function $\beta$ s.t. $\mu, \Gamma, \Sigma \approx_{\beta,\sigma} \mu', \Gamma', \Sigma', r, \sigma_{pc} \vdash \langle\mu, e, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f\rangle$, and $\beta(r), \sigma_{pc} \vdash \langle\mu', e, \Gamma', \Sigma'\rangle \Downarrow_{IF} \langle\mu'_f, v'_f, \Gamma'_f, \Sigma'_f, \sigma'_f\rangle$; then, there exists a function $\beta'$ extending $\beta$ s.t.: $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta',\sigma} \mu'_f, \Gamma'_f, \Sigma'_f$. Moreover, if either $\sigma_f \le \sigma$ or $\sigma'_f \le \sigma$, then $v_f \sim_{\beta'} v'_f$.
VALUE

$r, \sigma_{pc} \vdash \langle \mu, v, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu, v, \Gamma, \Sigma, \sigma_{pc} \rangle$

THIS

$$
\frac{r_{this} = \mu(r)(@this) \quad \sigma_{this} = \Gamma(r)(@this) \sqcup \sigma_{pc}}{r, \sigma_{pc} \vdash \langle \mu, this, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu, r_{this}, \Gamma, \Sigma, \sigma_{this} \rangle}
$$

BINARY OPERATION

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, v_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle}{r, \sigma_{pc} \vdash \langle \mu, e_0 \ \mathbf{op} \ e_1, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_1, v_0 \ \mathbf{op} \ v_1, \Gamma_1, \Sigma_1, \sigma_0 \sqcup \sigma_1 \rangle}
$$

VARIABLE

$$
\frac{\langle \mu, r, x \rangle \mathcal{R}_{Scope} r_x \quad r_x \neq null}{v = \mu(r_x)(x) \quad \sigma = \Gamma(r_x)(x) \sqcup \sigma_{pc}} \\
\frac{r, \sigma_{pc} \vdash \langle \mu, x, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu, v, \Gamma, \Sigma, \sigma \rangle}{\quad}
$$

VARIABLE ASSIGNMENT

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad \langle \mu_0, r, x \rangle \mathcal{R}_{Scope} r_x}{r_x \neq null \quad \sigma_{pc} \leq \Gamma_0(r_x)(x)} \\
\frac{\Gamma' = \Gamma_0 [r_x \mapsto \Gamma_0(r_x)] [x \mapsto \sigma_0]] \quad \mu' = \mu_0 [r_x \mapsto \mu_0(r_x)] [x \mapsto v_0]}{r, \sigma_{pc} \vdash \langle \mu, x = e, \Gamma \rangle \Downarrow_{IF} \langle \mu', v_0, \Gamma', \Sigma_0, \sigma_0 \rangle}
$$

PROPERTY LOOK-UP

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, m_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle}{\langle \mu_1, r_0, m_1, \Gamma_1, \Sigma_1 \rangle \mathcal{R}_{Proto} \langle r', \sigma' \rangle \quad \langle v, \sigma \rangle = \begin{cases} \langle \mu_1(r')(m_1), \sigma_0 \sqcup \sigma_1 \sqcup \sigma' \sqcup \Gamma_1(r')(m_1) \rangle & \text{if } r' \neq null \\ \langle \text{undefined}, \sigma_0 \sqcup \sigma_1 \sqcup \sigma' \rangle & \text{otherwise} \end{cases}}
$$
$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0[e_1], \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_1, v, \Gamma_1, \Sigma_1, \sigma \rangle}{\quad}
$$

PROPERTY ASSIGNMENT

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, m_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle}{r, \sigma_{pc} \vdash \langle \mu_1, e_2, \Gamma_1, \Sigma_1 \rangle \Downarrow_{IF} \langle \mu_2, v_2, \Gamma_2, \Sigma_2, \sigma_2 \rangle \quad \Gamma' = \Gamma_2 [r_0 \mapsto \Gamma_2(r_0) [m_1 \mapsto \sigma_0 \sqcup \sigma_1 \sqcup \sigma_2]]} \\
\frac{\mu' = \mu_2 [r_0 \mapsto \mu_2(r_0) [m_1 \mapsto v_2]] \quad m_1 \in \mu_2(r_0) \Rightarrow \sigma_0 \sqcup \sigma_1 \le \Gamma_2(r_0)(m_1) \quad m_1 \notin \mu_2(r_0) \Rightarrow \sigma_0 \sqcup \sigma_1 \le \Sigma_2(r_0)}{r, \sigma_{pc} \vdash \langle \mu, e_0[e_1] = e_2, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu', v_2, \Gamma', \Sigma_2, \sigma_2 \rangle}
$$

FUNCTION LITERAL

$$
\frac{r_f \notin dom(\mu) \quad \mu' = \mu [r_f \mapsto [@fscope \mapsto r, @code \mapsto \lambda x.e]]}{\Gamma' = \Gamma [r_f \mapsto [@fscope \mapsto \sigma_{pc}, @code \mapsto \sigma_{pc}]] \quad \Sigma' = \Sigma [r_f \mapsto \sigma_{pc}]} \\
\frac{r, \sigma_{pc} \vdash \langle \mu, function(x) \{e\}, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu', r_f, \Gamma', \Sigma', \sigma_{pc} \rangle}{\quad}
$$

OBJECT LITERAL

$$
\frac{r_o \notin dom(\mu) \quad \mu' = \mu [r_o \mapsto [-prot_- \mapsto null]]}{\Gamma' = \Gamma [r_o \mapsto [-prot_- \mapsto \sigma_{pc}]] \quad \Sigma' = \Sigma [r_o \mapsto \sigma_{pc}]} \\
\frac{r, \sigma_{pc} \vdash \langle \mu, \{\}, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu', r_o, \Gamma', \Sigma', \sigma_{pc} \rangle}{\quad}
$$

FUNCTION CALL

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, v_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle}{\langle \mu_1, \Gamma_1, \Sigma_1, r_0, v_1, \#glob, \sigma_0, \sigma_1 \rangle \mathcal{R}_{NewScope} \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma}, \hat{r}, \hat{\sigma}_{pc} \rangle \quad \hat{r}, \hat{\sigma}_{pc} \vdash \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma} \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma \rangle} \\
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0(e_1), \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma \rangle}{\quad}
$$

METHOD CALL

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, m_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle}{r, \sigma_{pc} \vdash \langle \mu_1, e_2, \Gamma_1, \Sigma_1 \rangle \Downarrow_{IF} \langle \mu_2, v_2, \Gamma_2, \Sigma_2, \sigma_2 \rangle \quad \langle \mu_2, r_0, m_1, \Gamma_2, \Sigma_2 \rangle \mathcal{R}_{Proto} \langle r_m, \sigma_m \rangle \quad r_f = \mu_2(r_m)(m_1)} \\
\frac{\langle \mu_2, \Gamma_2, \Sigma_2, r_f, v_2, r_0, \sigma_0 \sqcup \sigma_1 \sqcup \Gamma_2(r_m)(m_1) \sqcup \sigma_m, \sigma_2 \rangle \mathcal{R}_{NewScope} \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma}, \hat{r}, \hat{\sigma}_{pc} \rangle \quad \hat{r}, \hat{\sigma}_{pc} \vdash \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma} \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma \rangle}{r, \sigma_{pc} \vdash \langle \mu, e_0[e_1](e_2), \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma \rangle}
$$

SEQUENCE

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, v_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle}{r, \sigma_{pc} \vdash \langle \mu, (e_0, e_1), \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_2, v_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle}
$$

CONDITIONAL

$$
\frac{r, \sigma_{pc} \vdash \langle \mu, \hat{e}, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \hat{\mu}, \hat{v}, \hat{\Gamma}, \hat{\Sigma}, \hat{\sigma} \rangle \quad i = \begin{cases} 0 & \text{if } \hat{v} \notin \{0, \text{false}, \text{undefined}, \text{null}\} \\ 1 & \text{otherwise} \end{cases}}{r, \sigma_{pc} \sqcup \hat{\sigma} \vdash \langle \hat{\mu}, e_i, \hat{\Gamma}, \hat{\Sigma} \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma \rangle} \\
\frac{r, \sigma_{pc} \vdash \langle \mu, \hat{e} ? (e_0) : (e_1), \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma \rangle}{\quad}
$$

<caption>Fig. 2. Monitored Core JavaScript Semantics</caption>
## 3 Monitor-Inlining

This section presents a new information flow monitor-inlining compiler for Core JavaScript, which instruments programs in order to simulate their execution in the monitored semantics presented in Section 2. This instrumentation rests on a technique that consists in pairing up each variable/property with a new one, called its *shadow* variable/property [7,11], that holds its corresponding security level. Since the compiled program has to handle security levels, we include them in the set of program values, which means adding them to the syntax of the language as such, as well as adding two new binary operators corresponding to $\le$ (the order relation) and $\sqcup$ (the least upper bound).

In the design of the compiler, we assume the existence of a given a set of variable and property names, denoted by $\mathcal{I}_C$, that do not overlap with those available for the programmer. In particular, the compilation of every *indexed expression* requires extra variables that are meant to store the corresponding value and security level, so that they can be later used in the compilation of other expressions that include it. Hence, we assume the set of compiler variables to include two indexed sets of variables $\{\$\hat{i}\}_{i \in \mathbb{N}}$ and $\{\$\hat{v}_i\}_{i \in \mathbb{N}}$ that are used to store the levels and the values of intermediate expressions, respectively. Given a variable $x$, we denote by $\$l_x$ the corresponding shadow variable. In contrast to variables, whose names are available at compile time, property names are dynamically computed. Therefore, we assume the existence of a runtime function $\$shadow$ that given a property name outputs the name of the corresponding shadow property. Given an expression $e$ to compile, the compiler guarantees that $e$ does not use variable and property names in $\mathcal{I}_C$ by (1) statically verifying that the variables in $e$ do not overlap with $\mathcal{I}_C$ and (2) dynamically verifying that $e$ does not look-up/create/update properties whose names belong to $\mathcal{I}_C$. To this end, the compiler makes use of a runtime function $\$legal$ that returns true when its argument does not belong to $\mathcal{I}_C$. For clarity, all identifiers reserved for the compiler are prefixed with a dollar sign, $\$$. By making sure that compiler identifiers do not overlap with those of the programs to compile, we guarantee the soundness of the proposed transformation even when it receives as input *malicious programs*. Malicious programs try to bypass the inlined runtime enforcement mechanism by rewriting some of its internal variables/properties. For instance, the compilation of the expression $\$\hat{l}_h = L, l = h$ fails, because this program tries to tamper with the internal state of the runtime enforcement mechanism in order to be allowed to leak confidential information. Concretely, this program tries to transfer the content of $h$ to $l$ without raising the level of $l$ by setting the level associated with variable $h$ to low.

Besides adding to every object $o$ an additional shadow property $\$l_p$ for every property $p$ in its domain, the inlined monitoring code also adds to $o$ a special property $\$struct$ that stores its structure security level. Hence, given an object $o = [p \mapsto v_0, q \mapsto v_1]$ pointed to by $r_o$ and a labeling $\langle \Gamma, \Sigma \rangle$, such that $\Gamma(r_o) = [p \mapsto H, q \mapsto L]$ and $\Sigma(r_o) = L$, the instrumented counterpart of $o$ labeled by $\langle \Gamma, \Sigma \rangle$ is $\hat{o} = [p \mapsto v_0, q \mapsto v_1, \$l_p \mapsto H, \$l_q \mapsto L, \$struct \mapsto L]$.
**Formal Specification.** The inlining compiler is defined as a function $C$, given in Figure 3, that expects as input an expression $e$ and produces a tuple $(\hat{e}, i)$, where $\hat{e}$ is the expression that simulates the execution of $e$ in the monitored semantics and $i$ an index such that, after the execution of $\hat{e}$, $\hat{v}_i$ stores the value to which $e$ evaluates in the monitored semantics and $\hat{l}_i$ its corresponding reading effect. Besides the runtime functions `$shadow` and `$legal``, the compiler makes use of (1) a runtime function `$check$` that diverges when its argument is different from `true`, (2) a runtime function `$inspect$` that expects as input an object and a property and outputs the level associated with the corresponding prototype-chain inspection procedure, and (3) an additional binary operator `hasOwnProp` that checks whether the object given as its left operand defines the property given as its right one. In practice, this operator does not exist; instead, there is a method `hasOwnProperty`, which is accessible to every object via its corresponding prototype chain, that checks whether the object on which it is invoked defines the property given as its argument. We chose not to model this feature of the language exactly as it is in practice in order to keep the model as simple as possible. Doing it otherwise would imply cluttering the already complex semantics of the language by having an alternative case for the Rule [*METHOD CALL*], which would model the semantics of the `hasOwnProperty` method call. During the evaluation of the instrumented code, the level of the execution context, $\sigma_{pc}$, is assumed to be stored in a variable `$pc$. To this end, function literals are instrumented in order to receive as input the level of the argument and the level of the context in which they are invoked. Function/method calls are instrumented accordingly. Furthermore, the instrumented code of a function/method call must have access to both the return value of the original function/method and the level that is to be associated with that value. Therefore, every function literal returns an object that defines two properties: (1) a property `$v$` where it stores the return value of the original function and (2) a property `$l$` where it stores the level to be associated with that value. Each compiler rule precisely mimics the corresponding monitor rule. However, the compiler must also keep track of the variables in which the security level and the value of the expression to compile are stored during execution. This is done by assigning the value to which the expression evaluates to a new variable $\hat{v}_i$ and the security level to a new variable $\hat{l}_i$. The compilation of every variable/property assignment and sequence expression does not introduce additional variables because the corresponding value and reading effect are already available in the indexed variables introduced by the corresponding subexpressions.

**Correctness.** Definition 5 presents a *similarity relation* between labeled memories in the monitored semantics and instrumented memories in the original semantics, denoted by $S_\beta$. $S_\beta$ requires that for every object in the labeled memory, the corresponding labeling coincide with the instrumented labeling (except for some internal properties whose levels can be automatically inferred) and that the property values of the original object be similar to those of its instrumented counterpart according to a new version of the $\beta$-equality called $C(\beta)$-equality. This relation, denoted by $\sim_{C(\beta)}$, differs from $\sim_\beta$ in that it relates each parsed
$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\textbf{VALUE} & \textbf{VARIABLE} & \textbf{THIS} \\
\hat{e} = \$\hat{l}_i = \$pc, \ \$v\hat{i} = v & \hat{e} = \$\hat{l}_i = \$pc \sqcup \$l_x, \ \$v\hat{i} = x & \hat{e} = \$\hat{l}_i = \$pc, \ \$v\hat{i} = \text{this} \\
\mathcal{C}\langle v^i \rangle = \langle \hat{e}, i \rangle & \mathcal{C}\langle x^i \rangle = \langle \hat{e}, i \rangle & \mathcal{C}\langle \text{this}^i \rangle = \langle \hat{e}, i \rangle
\end{array}
$$

BINARY OPERATION

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, j \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, j \rangle} \mathcal{C}\langle e_1 \rangle = \langle \hat{e}_1, k \rangle
  \end{array}
}{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle^{\text{op}^i} = \langle \hat{e}_0, e_1 \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle^{\text{op}^i} = \langle \hat{e}_0, e_1 \rangle} \mathcal{C}\langle e_1 \rangle^{\text{op}^i} = \langle \hat{e}_1, e_1 \rangle
  \end{array}
}
$$

VARIABLE ASSIGNMENT

$$
\frac{
  \begin{array}{@{}l@{}}
    x \notin \mathcal{I}_C \\
    \mathcal{C}\langle e \rangle = \langle e', i \rangle
  \end{array}
}{
  \begin{array}{@{}l@{}}
    \hat{e} = e', \ \mathit{check}(\$pc \le \$l_x), \ \$l_x = \$\hat{l}_i, \ x = \$v\hat{i} \\
    \mathcal{C}\langle x = e \rangle = \langle \hat{e}, i \rangle
  \end{array}
}
$$

PROPERTY LOOK-UP

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, k \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, k \rangle} \mathcal{C}\langle e_1 \rangle = \langle \hat{e}_1, j \rangle
  \end{array}
}{
  \begin{array}{@{}l@{}}
    e_{lev} = \$\hat{l}_i = \$\hat{l}_k \sqcup \$\hat{l}_j \sqcup \mathit{inspect}(\$v\hat{k}, \$v\hat{j}) \\
    \phantom{e_{lev} = \$\hat{l}_i = \$\hat{l}_k \sqcup \$\hat{l}_j \sqcup \mathit{inspect}(} \hat{e} = \hat{e}_0, \ \hat{e}_1, \ \mathit{check}(\$legal(\$v\hat{j})), \ e_{lev}, \ \$v\hat{i} = \$v\hat{k}[\$v\hat{j}]
  \end{array}
}
$$

PROPERTY ASSIGNMENT

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle} \mathcal{C}\langle e_1 \rangle = \langle \hat{e}_1, j \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle} \mathcal{C}\langle e_2 \rangle = \langle \hat{e}_2, k \rangle
  \end{array}
}{
  \begin{array}{@{}l@{}}
    e_{enf} = \$v\hat{i} \text{ hasOwnProp } \$v\hat{j} ? \; (\mathit{check}(\$\hat{l}_i \sqcup \$\hat{l}_j \le \$v\hat{i}[\mathit{shadow}(\$v\hat{j})])) : \; (\mathit{check}(\$\hat{l}_i \sqcup \$\hat{l}_j \le \$v\hat{i}.\mathit{struct})) \\
    \phantom{e_{enf} = \$v\hat{i} \text{ hasOwnProp } \$v\hat{j} ? \; (\mathit{check}(\;)} \hat{e} = \hat{e}_0, \ \hat{e}_1, \ \hat{e}_2, \ \mathit{check}(\$legal(\$v\hat{j})), \ e_{enf}, \ \$v\hat{i}[\mathit{shadow}(\$v\hat{j})] = \$\hat{l}_i \sqcup \$\hat{l}_j \sqcup \$\hat{l}_k, \ \$v\hat{i}[\$v\hat{j}] = \$v\hat{k} \\
    \mathcal{C}\langle e_0[\hat{e}_1]^i \rangle = \langle \hat{e}, i \rangle
  \end{array}
}
$$

FUNCTION LITERAL

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e \rangle = \langle \hat{e}_f, j \rangle \\
    \phantom{\mathcal{C}\langle e \rangle = \langle \hat{e}_f, j \rangle} e_{fbody} = \hat{e}_f, \ \$ret = \{\}, \ \$ret.\$v = \$v\hat{j}, \ \$ret.\$l = \$\hat{l}_j, \ \$ret \\
    \{i_1, \dots, i_k\} = \mathit{indexes}(e)
  \end{array}
}{
  \begin{array}{@{}l@{}}
    e_f = \$v\hat{i} = \mathbf{function}(x, \$l_x, \$pc)\{\mathbf{var} \ y_1, \dots, y_n, \ \$v\hat{i}_1, \ \$\hat{l}_1, \dots, \ \$v\hat{i}_k, \ \$\hat{l}_k; \ e_{fbody}\} \\
    \phantom{e_f = \$v\hat{i} = \mathbf{function}(x, \$l_x, \$pc)\{\mathbf{var} \ } \hat{e} = e_f, \ \$v\hat{i}.\mathit{struct} = \$pc, \ \$v\hat{i}.\mathit{struct} = \$pc, \ \$\hat{l}_i = \$pc, \ \$v\hat{i} \\
    \mathcal{C}\langle \mathbf{function}^i(x)\{\mathbf{var} \ y_1, \dots, y_n; \ e\} \rangle = \langle \hat{e}, i \rangle
  \end{array}
}
$$

OBJECT LITERAL

$$
\frac{
  \begin{array}{@{}l@{}}
    e' = \$v\hat{i}.\mathit{struct} = \$pc, \ \$v\hat{i}.\$l_{proto} = \$pc \\
    \phantom{e' = \$v\hat{i}.\mathit{struct} = \$pc, \ } \hat{e} = \$v\hat{i} = \{\}, \ e', \ \$\hat{l}_i = \$pc, \ \$v\hat{i}
  \end{array}
}{
  \mathcal{C}\langle \{\}^i \rangle = \langle \hat{e}, i \rangle
}
$$

FUNCTION CALL

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, j \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, j \rangle} \mathcal{C}\langle e_1 \rangle = \langle \hat{e}_1, k \rangle \\
    e' = \$\hat{l}_{ctx} = \$v\hat{j}.\$l_{@fscope} \sqcup \$\hat{l}_j, \ \$ret = \$v\hat{j}(\$v\hat{k}, \$\hat{l}_k \sqcup \$\hat{l}_{ctx}, \$\hat{l}_{ctx}) \\
    \phantom{e' = \$\hat{l}_{ctx} = \$v\hat{j}.\} \hat{e} = \hat{e}_0, \ \hat{e}_1, \ e', \ \$\hat{l}_i = \$ret.\$l, \ \$v\hat{i} = \$ret.\$v
  \end{array}
}{
  \mathcal{C}\langle e_0(e_1)^i \rangle = \langle \hat{e}, i \rangle
}
$$

METHOD CALL

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, j \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, j \rangle} \mathcal{C}\langle e_1 \rangle = \langle \hat{e}_1, k \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, j \rangle} \mathcal{C}\langle e_2 \rangle = \langle \hat{e}_2, l \rangle \\
    e' = \hat{e}_0, \ \hat{e}_1, \ \hat{e}_2, \ \$\hat{l}_{ctx} = \$\hat{l}_j \sqcup \$\hat{l}_k \sqcup \mathit{inspect}(\$v\hat{k}, \$v\hat{j}) \sqcup \$v\hat{j}[\$v\hat{k}].\$l_{@fscope} \\
    \phantom{e' = \hat{e}_0, \ } \hat{e} = e', \ \$ret = \$v\hat{j}[\$v\hat{k}](\$v\hat{l}, \$\hat{l}_{ctx} \sqcup \$\hat{l}_j, \$\hat{l}_{ctx}), \ \$\hat{l}_i = \$ret.\$l, \ \$v\hat{i} = \$ret.\$v
  \end{array}
}{
  \mathcal{C}\langle e_0[\hat{e}_1](e_2)^i \rangle = \langle \hat{e}, i \rangle
}
$$

SEQUENCE

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle} \mathcal{C}\langle e_1 \rangle = \langle \hat{e}_1, j \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle} \hat{e} = \hat{e}_0, \ \hat{e}_1
  \end{array}
}{
  \mathcal{C}\langle e_0, e_1 \rangle = \langle \hat{e}, j \rangle
}
$$

CONDITIONAL

$$
\frac{
  \begin{array}{@{}l@{}}
    \mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle} \mathcal{C}\langle e_1 \rangle = \langle \hat{e}_1, j \rangle \\
    \phantom{\mathcal{C}\langle e_0 \rangle = \langle \hat{e}_0, i \rangle} \mathcal{C}\langle e_2 \rangle = \langle \hat{e}_2, k \rangle \\
    e_{cond} = \$v\hat{i} ? \; (\hat{e}_1, \ \$v\hat{t} = \$v\hat{j}, \ \$\hat{l}_t = \$\hat{l}_j) : \; (\hat{e}_2, \ \$v\hat{t} = \$v\hat{k}, \ \$\hat{l}_t = \$\hat{l}_k) \\
    \phantom{e_{cond} = \$v\hat{i} ? \ } \hat{e} = \hat{e}_0, \ \$\hat{l}_s = \$pc, \ \$pc = \$pc \sqcup \$\hat{l}_i, \ e_{cond}, \ \$pc = \$\hat{l}_s, \ \$v\hat{t}
  \end{array}
}{
  \mathcal{C}\langle e_0 ?^{s,t} (e_1) : (e_2) \rangle = \langle \hat{e}, t \rangle
}
$$

<caption>Fig. 3. Information Flow Monitor Inlining Compiler</caption>
function with its corresponding compilation and in that it allows the domain of
the instrumented object to be larger than the one of the original object.

**Definition 5 (Memory Similarity).** A memory $\mu$ labeled by $\langle\Gamma, \Sigma\rangle$ is similar to a memory $\mu'$ w.r.t. $\beta$, written $\langle\mu, \Gamma, \Sigma\rangle S_\beta \mu'$, if and only if $dom(\beta) = dom(\mu)$ and for every reference $r \in dom(\beta)$, if $o = \mu(r)$ and $o' = \mu'(\beta(r))$, then $\Sigma(r) = o'(\$struct)$ and for all properties $p \in dom(o)\$\{|@scope, @this, @code\}$, $o(p) \sim_{C(\beta)} o'(p)$ and $\Gamma(r)(p) = o'(\$l_p)$

The Correctness Theorem states that, provided that a program and its com-
piled counterpart are evaluated in similar configurations, the evaluation of the
original one in the monitored semantics terminates if and only if the evaluation
of its compilation also terminates in the original semantics, in which case the
final configurations as well as the computed values are similar. Therefore, since
the monitored semantics only allows secure executions to go through, we guar-
antee that, when using the inlining compiler, programs are rewritten in such a
way that only their secure executions are allowed to terminate.

**Theorem 2 (Correctness).** Provided that *e* does not use identifiers in *I*<sub>*C*</sub>, for any labeled and instrumented configurations ⟨μ, *e*, Γ, Σ⟩ and ⟨μ', *e*′⟩, function *β*, and reference *r* in *μ*, such that ⟨μ, Γ, Σ⟩ *S*<sub>β</sub> *μ*′ and *C*⟨*e*⟩ = ⟨*e*', *i*⟩, for some index *i*; there exists ⟨μ<sub>*f*</sub>, *v*<sub>*f*</sub>, Γ<sub>*f*</sub>, *σ*⟩ such that *r*, ⊥ ⊢ ⟨μ, *e*, Γ, Σ⟩ ⇝<sub>IF</sub> ⟨μ<sub>*f*</sub>, *v*<sub>*f*</sub>, Γ<sub>*f*</sub>, Σ<sub>*f*</sub>, *σ*<sub>*f*</sub>⟩ iff there exists ⟨μ'<sub>*f*</sub>, *v*'<sub>*f*</sub>⟩ such that *β*(*r*) ⊢ ⟨⟨μ', *e*′⟩⟩ ⇝ ⟨⟨μ'<sub>*f*</sub>, *v*'<sub>*f*</sub>⟩⟩, in which case the following statements hold: (1) ⟨μ<sub>*f*</sub>, Γ<sub>*f*</sub>, Σ<sub>*f*</sub>⟩ *S*<sub>β'</sub> *μ*'<sub>*f*</sub>, (2) *v*<sub>*f*</sub> ∼<sub>*C(β)*</sub> *v*'<sub>*f*</sub>, and (3) *σ*<sub>*f*</sub> = *μ*'<sub>*f*</sub>(β(*r*))($\hat{l}_i$).

4 Discussion and Related Work

*JavaScript Semantics.* Since scope objects are assumed not to have a prototype and since we do not include the JavaScript with construct, Core JavaScript programs are syntactically scoped. This means that we could have modeled the binding of variables using substitution, as in other works targeting subsets of the whole language, as [8]. However, we have chosen to model scope using scope objects, as in [10], for two main reasons. First, we envisage to extend the model to deal with a larger subset of the language. Second, by modeling the binding of variables in the same way we model the binding of properties, we do not need to introduce an extra labeling function for the labeling of variables.

*Monitoring Secure Information Flow.* Information flow monitors can be divided in two main classes. *Purely dynamic monitors* (such as [3] and [4]) do not make use of any kind of static analysis. By this, we also mean that purely dynamic monitors do not expect the program to be annotated with the output of a static analysis to be later used at runtime. On the contrary, *hybrid monitors* (such as [12]) make use of static analyses to reason about the implicit flows that can arise due to untaken execution paths. Naturally, such static analyses are not meant to be performed at runtime. Instead, programs are usually annotated
with the output of the analysis, which is then used by the monitor during execution. Austin and Flanagan propose two different strategies for designing purely dynamic information flow monitors. The no-sensitive-upgrade strategy [3] forbids programs to update the value of low variables in high contexts. Alternatively, the permissive-upgrade strategy allows programs to perform sensitive upgrades, but it marks resources that were subject to such upgrades and forbids programs to branch depending on the content of those resources. Our choice for the inlining of a purely dynamic monitor has to do with the fact that the dynamic features of JavaScript make it very difficult to approximate the resources created/updated in untaken program branches. Hedin and Sabelfeld [9] have been the first to design, prove sound, and implement an information flow monitor for a realistic core of JavaScript. Their monitor is purely dynamic and enforces the no-sensitive-upgrade discipline. This monitor has been designed in order to guide a browser instrumentation and not an inlining transformation. Furthermore, it differs from ours in that it labels values instead of variables/properties. Bichhawat et al. [6] have recently proposed a hybrid monitor that makes use of a sophisticated static analysis to minimize performance overhead [6].

*Monitor-Inlining Transformations.* Chudnov and Naumann [7] propose an information flow monitor inlining transformation for a WHILE language, which inlines the hybrid information flow monitor presented in [12]. Hence, their inlining compiler includes a simple static analysis that estimates the set of variables updated in untaken program branches. Simultaneously, Magazinius et al. [11] propose the inlining of a purely dynamic information flow monitor that enforces the no-sensitive-upgrade discipline for a simple imperative language that features global functions, a let construct, and an *eval* expression that allows for dynamic code evaluation. Both compilers pair up each variable with a *shadow* variable. We extend this technique to handle object properties by pairing up each property with a shadow property. The languages modeled in both [7] and [11] only feature primitive values and do not feature scope composition (in [7] there are no functions and in [11] every function is executed in a “clean” environment and does not produce side-effects). Hence, in both [7] and [11], the reading effect of an expression *e* corresponds to the least upper bound on the levels of the variables of *e*. Therefore, the instrumented code for computing the level of *e* is simply $l_{x_1} \sqcup \dots \sqcup l_{x_n}$, where $\{x_1, \dots, x_n\}$ are the variables that explicitly occur in *e*. In Core JavaScript (as in JavaScript) this does not hold. First, one can immediately see that expressions that feature property look-ups or function/method calls do not generally verify this property. Second, expressions may be composed of expressions that have side effects. Therefore, the level associated with the whole expression can actually be lower than the least upper bound on the levels of the variables that it includes. As an example, consider the expression $(x = y) + x$. Since $x = y$ evaluates to the value of *y* (besides assigning the value of *y* to *x*), the level of the whole expression only depends on the initial level of *y*. In order to handle these two issues, the inlining transformation must introduce extra variables to keep track of the values and levels of intermediate expressions. For instance, consider the following expression:
$o_0 = \{\}, o_1 = \{p : \text{"q"}, q : 0\}, o_0[(o_0 = o_1)[\text{"p"}]] = o_0[\text{"q"}]$. After the evaluation of this expression the object pointed by `$\#o_1$` is: $[p \mapsto \text{"q"}, q \mapsto \text{"q"}]$. An uncareful instrumentation may ignore the fact that during its evaluation $o_0$ is updated with `$\#o_1$`. Finally, both [7] and [11] ignore the problem of malicious programs.

In summary, we have presented the first compiler for securing information flow in an important subset of JavaScript. The presented compiler is proven sound even when it is given as input malicious code that actively tries to bypass the inlined enforcement mechanism. A prototype of the compiler is available online [1] together with a broad set of examples that illustrate its applicability.

*Acknowledgements* This work was partially supported by the Portuguese Government via the PhD grant SFRH/BD/71471/2010.

## References

1. Information flow monitor-inlining compiler. http://www-sop.inria.fr/indes/ifJS.

2. The 5th edition of ECMA 262 June 2011. ECMAScript Language Specification. Technical report, ECMA, 2011.

3. T. H. Austin and C. Flanagan. Efficient purely-dynamic information flow analysis. In *PLAS*, 2009.

4. T. H. Austin and C. Flanagan. Permissive dynamic information flow analysis. In *PLAS*, 2010.

5. A. Banerjee and D. A. Naumann. Secure information flow and pointer confinement in a java-like language. In *CSFW*, 2002.

6. A. Bichhawat, V. Rajani, D. Garg, and C. Hammer. Information flow control in WebKits JavaScript bytecode. In *POST*, 2014.

7. A. Chudnov and D. A. Naumann. Information flow monitor inlining. In *CSF*, 2010.

8. A. Guha, C. Saftoiu, and S. Krishnamurthi. The essence of Javascript. In *ECOOP*, 2010.

9. D. Hedin and A. Sabelfeld. Information-flow security for a core of JavaScript. In *CSF*, 2012.

10. S. Maffeis, J. C. Mitchell, and A. Taly. An operational semantics for JavaScript. In *APLAS*, 2008.

11. J. Magazinius, A. Russo, and A. Sabelfeld. On-the-fly inlining of dynamic security monitors. *Computers & Security*, 2012.

12. A. Russo and A. Sabelfeld. Dynamic vs. static flow-sensitive security analysis. In *CSF*, 2010.

13. A. Sabelfeld and A. C. Myers. Language-based information-flow security. *IEEE Journal on Selected Areas in Communications*, 2003.
# A Proofs of Section 2

## A.1 Properties of the Low-Equality

**β-Equalitiy** When $\beta$ corresponds to the identity function, the $\beta$-Equality relation is an equivalence relation. This fact is formally presented in Lemmas 2, 3 and 4. In the following, $O|_R$ corresponds to the set of objects that only use references in $R$ (where $R \subseteq Ref$). Likewise, $Pse|_R$ corresponds to the extension of this definition to pseudo-values.

**Lemma 2 (Reflexivity of $\sim_{id}$).** Given a set of references $R \subseteq Ref$, for every pseudo-value $v \in Pse|_R$, $v \sim_{id} v$, where id is the identity function defined on $R$.

*Proof.* The proof proceeds by induction on the derivation of $v \sim_{id} v$. The base cases are: $v \in \text{Prim}$, $v \in \mathcal{F}_{\lambda}$, and $v \in R$. The inductive case is $v \in O|_R$.

- $v \in \text{Prim}$. By inspection of the Rule [PRIM], the result follows.

- $v \in \mathcal{F}_{\lambda}$. By inspection of the Rule [FUN], the result follows.

- $v \in R$. Since id is defined on $R$, we conclude that $v = id(v)$. Hence, by inspection of the Rule [REFERENCE], the result follows.

- $v \in O|_R$. For every property $p \in \text{dom}(v)$, $v(p) \in \text{Prim} \cup R \cup \mathcal{F}_{\lambda}$. Hence, we apply the induction hypothesis to conclude that $v(p) \sim_{id} v(p)$. Thus, by inspection of the Rule [OBJECT], the result follows.

**Lemma 3 (Symmetry of $\sim_{\beta}$).** Given an injective function $\beta$ and two pseudo-values $v_0, v_1 \in Pse$ such that: $v_0 \sim_{\beta} v_1$, then $v_1 \sim_{\beta^{-1}} v_0$.

*Proof.* The proof proceeds by induction on the derivation of $v_0 \sim_{id} v_1$. The base cases are: $v_0, v_1 \in \text{Prim}$, $v_0, v_1 \in \mathcal{F}_{\lambda}$, and $v_0, v_1 \in R$. The inductive case is $v_0, v_1 \in O|_R$.

- $v_0, v_1 \in \text{Prim}$. By inspection of the Rule [PRIM], we conclude that $v_0 = v_1$, and hence $v_1 = v_0$. Thus, applying the same rule, the result follows.

- $v_0, v_1 \in \mathcal{F}_{\lambda}$. By inspection of the Rule [FUN], we conclude that $v_0 = v_1$, and hence $v_1 = v_0$. Thus, applying the same rule, the result follows.

- $v_0, v_1 \in Ref$. By inspection of the Rule [REFERENCE], we conclude that $v_1 = \beta(v_0)$. Since $\beta$ is injective, $\beta^{-1}$ is defined on the range of $\beta$ and particularly, $\beta^{-1}(v_1) = v_0$, from which the result follows (applying the same rule).

- $v_0, v_1 \in O$. By inspection of the Rule [OBJECT], we conclude that:

$$ \text{dom}(v_0) = \text{dom}(v_1) = P $$

and that for every property $p \in P$, $v_0(p) \sim_{\beta} v_1(p)$. Since $v_0(p)$ and $v_1(p)$ are either in $\text{Prim}$, in $\text{Ref}$, or in $\mathcal{F}_{\lambda}$, we apply the induction hypothesis to conclude that: $v_1(p) \sim_{\beta^{-1}} v_0(p)$ for every property $p \in P$, thus proving the result.

**Lemma 4 (Transitivity of $\sim_{\beta}$).** Given two injective functions $\beta_0, \beta_1 : Ref \to Ref$ and three pseudo-values $v_0, v_1, v_2 \in Pse$ such that $v_0 \sim_{\beta_0} v_1$ and $v_1 \sim_{\beta_1} v_2$, then $v_0 \sim_{\beta_1 \circ \beta_0} v_2$.
**Proof.** The proof proceeds by case analysis on the derivations of $v_0 \sim_{\beta_0} v_1$ and $v_1 \sim_{\beta_1} v_2$. There are four different cases: (1) $v_0, v_1, v_2 \in \mathcal{P}rim$, (2) $v_0, v_1, v_2 \in \mathcal{F}_{\lambda}$, (3) $v_0, v_1, v_2 \in \mathcal{R}ef$, and (4) $v_0, v_1, v_2 \in \mathcal{O}$.

- $v_0, v_1, v_2 \in \mathcal{P}rim$. By inspection of the [PRIM], we conclude that $v_0 = v_1$ and $v_1 = v_2$, thus following that $v_0 = v_2$ and therefore: $v_0 \sim_{\beta_1 \circ \beta_0} v_2$.

- $v_0, v_1, v_2 \in \mathcal{F}_{\lambda}$. By inspection of the Rule [FUN], we conclude that $v_0 = v_1$ and $v_1 = v_2$, thus following that $v_0 = v_2$ and therefore: $v_0 \sim_{\beta_1 \circ \beta_0} v_2$.

- $v_0, v_1, v_2 \in \mathcal{R}ef$. By inspection of the Rule [REFERENCE], we conclude that $v_1 = \beta_0(v_0)$ and $v_2 = \beta_1(v_1)$, thus following that $v_2 = \beta_1(\beta_0(v_0)) = \beta_1 \circ \beta_0(v_0)$, from which it follows that: $v_0 \sim_{\beta_1 \circ \beta_0} v_2$.

- $v_0, v_1, v_2 \in \mathcal{O}$. By inspection of the Rule [OBJECT], we conclude that $\text{dom}(v_0) = \text{dom}(v_1) = \text{dom}(v_2) = P$. For every property $p \in P$, $v_0(p) \sim_{\beta_0} v_1(p)$ and $v_1(p) \sim_{\beta_1} v_2(p)$. Since $v_0(p)$, $v_1(p)$, and $v_2(p)$ are either in $\mathcal{P}rim$, in $\mathcal{R}ef$, or in $\mathcal{F}_{\lambda}$, we use the two first cases to conclude that for every property $p \in P$, $v_0(p) \sim_{\beta_1 \circ \beta_0} v_2(p)$, thus proving the result.

**Lemma 5 (Lateral Transitivity of $\sim_{\beta}$).** For any four pseudo-values $v_0, v'_0$, $v_1$, and $v'_1$ in $\mathcal{P}se$ such that $v_0 \sim_{id_0} v'_0$, $v_1 \sim_{id_1} v'_1$ and $v_0 \sim_{\beta} v_1$, where $id_0$ and $id_1$ correspond to the identity function on references defined on the domain of $\beta$ and on the range of $\beta$, respectively. Then, it follows that $v'_0 \sim_{id_1 \circ \beta \circ id_0} v'_1$.

**Proof.** The proof proceeds by case analysis.

- $v_0, v'_0, v_1, v'_1 \in \mathcal{P}rim$. By inspection of the Rule [PRIM], it follows that $v_0 = v_1, v_0 = v'_0$, and $v_1 = v'_1$, from which it follows that $v'_0 = v'_1$, entailing that $v'_0 \sim_{\beta} v'_1$.

- $v_0, v'_0, v_1, v'_1 \in \mathcal{F}_{\lambda}$. By inspection of the Rule [FUN], it follows that $v_0 = v_1, v_0 = v'_0$, and $v_1 = v'_1$, from which it follows that $v'_0 = v'_1$, entailing that $v'_0 \sim_{\beta} v'_1$.

- $v_0, v'_0, v_1, v'_1 \in \mathcal{R}ef$. By inspection of the Rule [REFERENCE], it follows that $v'_0 = v_0, v'_1 = v_1$, and $v_1 = \beta(v_0)$, from which it follows that $v'_1 = \beta(v'_0)$, entailing that $v'_0 \sim_{\beta} v'_1$.

- $v_1, v'_1, v_2, v'_2 \in \mathcal{O}$. By inspection of the Rule [OBJECT], it follows that:

$$ \text{dom}(v'_0) = \text{dom}(v_0) = \text{dom}(v_1) = \text{dom}(v'_1) = P $$

For every property $p \in P$, $v_0(p) \sim_{\beta} v_1(p)$, $v_0(p) \sim_{id_0} v'_0(p)$, and $v_1(p) \sim_{id_1} v'_1(p)$. Since $v_1(p), v'_1(p), v_2(p)$, and $v'_2(p)$ are either in $\mathcal{P}rim$, in $\mathcal{R}ef$, or in $\mathcal{F}_{\lambda}$, we can apply one of the previous cases to conclude that: $v'_0(p) \sim_{\beta} v'_1(p)$ for every property $p \in P$, thus proving the result.

## Low-Equality

**Lemma 6.** Given four security levels $\sigma_0, \sigma_1, \sigma_2, \sigma \in \mathcal{L}$ and three sets of references $R_0, R_1, R_2 \subseteq \mathcal{R}ef$, such that:

$$ (\sigma_0 \le \sigma \lor \sigma_1 \le \sigma) \Rightarrow (\sigma_0 \sqcup \sigma_1 \le \sigma \land R_0 = R_1) \quad (\text{hyp.1}) $$

$$ (\sigma_1 \le \sigma \lor \sigma_2 \le \sigma) \Rightarrow (\sigma_1 \sqcup \sigma_2 \le \sigma \land R_1 = R_2) \quad (\text{hyp.2}) $$

Then, it follows that $(\sigma_0 \le \sigma \lor \sigma_2 \le \sigma) \Rightarrow (\sigma_0 \sqcup \sigma_2 \le \sigma \land R_0 = R_2)$.
Proof. Suppose that $\sigma_0 \le \sigma$ (hyp.3).

$$ - \sigma_0 \sqcup \sigma_1 \le \sigma \text{ and } R_0 = R_1 \quad (1) - \text{hyp.1} + \text{hyp.3} $$

$$ - \sigma_1 \le \sigma \quad (2) - (1) $$

$$ - \sigma_1 \sqcup \sigma_2 \le \sigma \text{ and } R_1 = R_2 \quad (3) - \text{hyp.2} + (2) $$

$$ - \sigma_2 \le \sigma \quad (4) - (3) $$

$$ - \sigma_0 \sqcup \sigma_2 \le \sigma \text{ and } R_0 = R_2 \quad (5) - \text{hyp.3} + (1) + (3) + (4) $$

Analogously, assuming that $\sigma_2 \le \sigma$, we conclude that $(\sigma_0 \sqcup \sigma_2 \le \sigma \wedge R_0 = R_2)$. Therefore, the claim of the lemma holds.

**Lemma 7 (Transitivity of $\approx_{\beta,\sigma}$).** For any three memories $\mu_0, \mu_1$ and $\mu_2$, labelings $\langle \Gamma_0, \Sigma_0 \rangle, \langle \Gamma_1, \Sigma_1 \rangle$, and $\langle \Gamma_2, \Sigma_2 \rangle$, security level $\sigma$, and two functions $\beta_0$ and $\beta_1$ such that: $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta_0,\sigma} \mu_1, \Gamma_1, \Sigma_1$ (hyp.1) and $\mu_1, \Gamma_1, \Sigma_1 \approx_{\beta_1,\sigma} \mu_2, \Gamma_2, \Sigma_2$ (hyp.2). Then, it follows that $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta_1 \circ \beta_0,\sigma} \mu_2, \Gamma_2, \Sigma_2$.

Proof. Suppose that $r_0 \in \text{dom}(\beta_1 \circ \beta_0)$ and $r_2 = \beta_1 \circ \beta_0(r_0)$ (hyp.3).

$$ - r_0 \in \text{dom}(\beta_0) \quad (1) - \text{hyp.3} $$

$$ - r_1 = \beta_0(r_0) \in \text{dom}(\beta_1) \text{ and } r_2 = \beta_1(r_1), \text{ for some } r_1 \quad (2) - \text{hyp.3} $$

$$ - \Gamma_0(r_0)|_{\sigma} = \Gamma_1(r_1)|_{\sigma} = P_0 \quad (3) - \text{hyp.1} + (2) $$

$$ - \mu_0(r_0)|_{P_0} \sim_{\beta_0} \mu_1(r_1)|_{P_0} \quad (4) - \text{hyp.1} + (2) $$

$$ - (\Sigma_0(r_0) \le \sigma \lor \Sigma_1(r_1) \le \sigma) \Rightarrow \begin{cases} \text{dom}(\mu_0(r_0)) = \text{dom}(\mu_1(r_1)) \\ \Sigma_0(r_0) \sqcup \Sigma_1(r_1) \le \sigma \end{cases} \quad (5) - \text{hyp.1} + (2) $$

$$ - \Gamma_1(r_1)|_{\sigma} = \Gamma_2(r_2)|_{\sigma} = P_1 \quad (6) - \text{hyp.2} + (2) $$

$$ - \mu_1(r_1)|_{P_1} \sim_{\beta_1} \mu_2(r_2)|_{P_1} \quad (7) - \text{hyp.2} + (2) $$

$$ - (\Sigma_1(r_1) \le \sigma \lor \Sigma_2(r_2) \le \sigma) \Rightarrow \begin{cases} \text{dom}(\mu_1(r_1)) = \text{dom}(\mu_2(r_2)) \\ \Sigma_1(r_1) \sqcup \Sigma_2(r_2) \le \sigma \end{cases} \quad (8) - \text{hyp.2} + (2) $$

$$ - \Gamma_0(r_0)|_{\sigma} = \Gamma_2(r_2)|_{\sigma} = P = P_0 = P_1 \quad (9) - (3) + (6) $$

$$ - \mu_0(r_0)|_P \sim_{\beta_1 \circ \beta_0} \mu_2(r_2)|_P \quad (10) - (4) + (7) + \text{Transitivity of } \sim_{\beta} $$

$$ - (\Sigma_0(r_0) \le \sigma \lor \Sigma_2(r_2) \le \sigma) \Rightarrow \begin{cases} \text{dom}(\mu_0(r_0)) = \text{dom}(\mu_2(r_2)) \\ \Sigma_0(r_0) \sqcup \Sigma_2(r_2) \le \sigma \end{cases} \quad (11) - (5) + (8) + \text{Lemma 6} $$

Since all references in $\text{dom}(\beta_1 \circ \beta_0)$ verify (9), (10), and (11), the claim of the lemma follows.

**Lemma 8 (Reflexivity of $\approx_{id,\sigma}$).** For any security level $\sigma \in \mathcal{L}$, and two memories $\mu$ and $\mu'$, two labelings $\langle \Gamma, \Sigma \rangle$ and $\langle \Gamma', \Sigma' \rangle$, such that $\mu \le \mu'$ (hyp.1) and $\langle \Gamma, \Sigma \rangle \le \langle \Gamma', \Sigma' \rangle$ (hyp.2), then $\mu, \Gamma, \Sigma \approx_{id,\sigma} \mu', \Gamma', \Sigma'$, where id is the identity function defined on the domain of $\mu$.

Proof. Suppose that $r \in \text{dom}(\mu)$ (hyp.3):

$$ - \Gamma(r)|_{\sigma} = \Gamma'(r)|_{\sigma} = P \quad (1) - \text{hyp.2} + \text{hyp.3} $$

$$ - \mu(r)|_P \sim_{id} \mu'(r)|_P \quad (2) - \text{hyp.1} + \text{hyp.3} $$
$$ - (\Sigma(r) \le \sigma \lor \Sigma'(r) \le \sigma) \Rightarrow \begin{cases} \operatorname{dom}(\mu(r)) = \operatorname{dom}(\mu'(r)) \\ \Sigma(r) \sqcup \Sigma'(r) \le \sigma \end{cases} \quad (3) - \operatorname{hyp.1} + \operatorname{hyp.2} \\ + \operatorname{hyp.3} $$

Since all references in $dom(id)$ verify (1), (2), and (3), the claim of the lemma follows.

**Lemma 9 (High Property Update).** Given a security level $\sigma \in \mathcal{L}$ and two memories $\mu$ and $\mu'$ respectively labeled by $\langle \Gamma, \Sigma \rangle$ and $\langle \Gamma', \Sigma' \rangle$, such that $\mu$ coincides with $\mu'$ everywhere except for some reference $r$ and property $p$ for which $\sigma \not\le \Gamma(r)(p)$ and $\sigma \not\le \Gamma'(r)(p)$; then: $\mu, \Gamma, \Sigma \approx_{id,\sigma} \mu', \Gamma', \Sigma'$, where $id$ is the identity function defined in the domain of $\mu$.

*Proof.* The low-equality conditions hold for every reference $\hat{r} \ne r$. In order to see that they also hold for $r$, one simply has to note that $p \notin \Gamma(r)|_{\sigma}$ and $p \notin \Gamma'(r)|_{\sigma}$.

**Lemma 10 (Low Property Update/Creation).** Given three security levels $\sigma, \sigma_0, \sigma_1 \in \mathcal{L}$, two memories $\mu_0$ and $\mu_1$ respectively labeled by $\langle \Gamma_0, \Sigma_0 \rangle$ and $\langle \Gamma_1, \Sigma_1 \rangle$, two references $r_0, r_1 \in \mathcal{Ref}$, two values $v_0, v_1 \in \mathcal{Val}$ and a function $\beta$ on $\mathcal{Ref}$, such that: $r_1 = \beta(r_0)$ (hyp.1), $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta,\sigma} \mu_1, \Gamma_1, \Sigma_1$ (hyp.2), and $\sigma_0 \sqcup \sigma_1 \le \sigma \Rightarrow v_0 \sim_{\beta} v_1$ (hyp.3). Then, it follows that $\mu'_0, \Gamma'_0, \Sigma_0 \approx_{\beta,\sigma} \mu'_1, \Gamma'_1, \Sigma_1$, for:

$$ - \mu'_0 = \mu_0 [r_0 \mapsto \mu_0(r_0) [m \mapsto v_0]] \quad (\text{hyp.4}), $$

$$ - \mu'_1 = \mu_1 [r_1 \mapsto \mu_1(r_1) [m \mapsto v_1]] \quad (\text{hyp.5}), $$

$$ - \Gamma'_0 = \Gamma_0 [r_0 \mapsto \Gamma_0(r_0) [m \mapsto \sigma_0]] \quad (\text{hyp.6}), $$

$$ - \Gamma'_1 = \Gamma_1 [r_1 \mapsto \Gamma_1(r_1) [m \mapsto \sigma_1]] \quad (\text{hyp.7}). $$

*Proof.* From hyp.1, we conclude that the low-equality conditions hold for every reference $r \ne r_0$. There are two cases to consider; either $v_0 \not\sim_{\beta} v_1$ or $v_0 \sim_{\beta} v_1$.

**Case** $\sigma_0 \sqcup \sigma_1 \le \sigma$ (hyp.8):

$$ - m \notin \Gamma'_0(r_0)|_{\sigma} \text{ and } m \notin \Gamma'_1(r_1)|_{\sigma} \quad (1) - \text{hyp.2} + \text{hyp.6} + \text{hyp.7} + \text{hyp.8} $$

$$ - \Gamma'_0(r_0)|_{\sigma} = \Gamma'_1(r_1)|_{\sigma} = P \quad (2) - \text{hyp.1} + \text{hyp.2} + \text{hyp.6} + \text{hyp.7} + (1) $$

$$ - \mu'_0(r_0)|_P \sim_{\beta} \mu'_1(r_1)|_P \quad (3) - \text{hyp.1} + \text{hyp.2} + \text{hyp.4} + \text{hyp.5} + (1) $$

$$ - \text{Case } \Sigma_0(r_0) \le \sigma \lor \Sigma_1(r_1) \le \sigma \quad (\text{hyp.9}): $$

$$ \bullet \Sigma_0(r_0) \sqcup \Sigma_1(r_1) \le \sigma \quad (4.1) - \text{hyp.1} + \text{hyp.2} $$

$$ \bullet \operatorname{dom}(\mu_0(r_0)) = \operatorname{dom}(\mu_1(r_1)) \quad (4.2) - \text{hyp.1} + \text{hyp.2} $$

$$ \bullet \operatorname{dom}(\mu'_0(r_0)) = \operatorname{dom}(\mu'_1(r_1)) \quad (4.3) - \text{hyp.4} + \text{hyp.5} + (4.2) $$

$$ \bullet (\Sigma_0(r_0) \le \sigma \lor \Sigma_1(r_1) \le \sigma) \Rightarrow \begin{cases} \operatorname{dom}(\mu'_0(r_0)) = \operatorname{dom}(\mu'_1(r_1)) \\ \Sigma_0(r_0) \sqcup \Sigma_1(r_1) \le \sigma \end{cases} \quad (4) - \text{hyp.9} + (4.1) + (4.3) $$

**Case** $\sigma_0 \sqcup \sigma_1 \le \sigma$ (hyp.8):

$$ - v_0 \sim_{\beta} v_1 \quad (1) - \text{hyp.3} + \text{hyp.8} $$

$$ - \Gamma'_0(r_0)|_{\sigma} = \Gamma'_1(r_1)|_{\sigma} = P \quad (2) - \text{hyp.1} + \text{hyp.2} + \text{hyp.6} + \text{hyp.7} $$

$$ - \mu'_0(r_0)|_P \sim_{\beta} \mu'_1(r_1)|_P \quad (3) - \text{hyp.1} + \text{hyp.2} + \text{hyp.4} + \text{hyp.5} + (1) $$
- Case $\Sigma_0(r_0) \le \sigma \lor \Sigma_1(r_1) \le \sigma$ (hyp.9):

• $\Sigma_0(r_0) \sqcup \Sigma_1(r_1) \le \sigma$ (4.1) - hyp.1 + hyp.2

• $\text{dom}(\mu_0(r_0)) = \text{dom}(\mu_1(r_1))$ (4.2) - hyp.1 + hyp.2

• $\text{dom}(\mu'_0(r_0)) = \text{dom}(\mu'_1(r_1))$ (4.3) - hyp.4 + hyp.5 + (4.2)

• $(\Sigma_0(r_0) \le \sigma \lor \Sigma_1(r_1) \le \sigma) \Rightarrow \begin{cases} \text{dom}(\mu'_0(r_0)) = \text{dom}(\mu'_1(r_1)) \\ \Sigma_0(r_0) \sqcup \Sigma_1(r_1) \le \sigma \\ (4) - \text{hyp.9} + (4.1) + (4.3) \end{cases}$

**Lemma 11 (Low-Equality Preserving Object Creation).** Given a security level $\sigma \in \mathcal{L}$, four consistent memories $\mu_1, \mu'_1, \mu_2$, and $\mu'_2$ respectively well-labeled by $\Gamma_1, \Gamma'_1, \Gamma_2$, and $\Gamma'_2$, two references $r_1, r_2 \in \mathcal{R}ef$ respectively free in $\mu_1$ and $\mu_2$, two objects $o_1, o_2 \in \mathcal{O}$, and a partial injective function $\beta$ defined on $\mathcal{R}ef$, such that: $\mu_1, \Gamma_1 \approx_{\beta, \sigma} \mu_2, \Gamma_2$, $\mu'_1 = \mu_1[r_1 \mapsto o_1]$, $\mu'_2 = \mu_2[r_1 \mapsto o_1]$, and $o_1|_{\sigma}^{r_1, \Gamma_1} \sim_{\beta} o_2|_{\sigma}^{r_2, \Gamma_2}$. Then: $\mu'_1, \Gamma'_1 \approx_{\beta', \sigma} \mu'_2, \Gamma'_2$, where $\beta' = \beta \cup \{(r_1, r_2)\}$.

**Lemma 12.** Given a security level $\sigma \in \mathcal{L}$ and four consistent memories $\mu_1, \mu'_1, \mu_2$, and $\mu'_2$ respectively labeled by $\Gamma_1, \Gamma'_1, \Gamma_2$, and $\Gamma'$ and a partial injective function $\beta$ defined on $\mathcal{R}ef$, such that:

$$\mu_1, \Gamma_1 \approx_{id_1, \sigma} \mu'_1, \Gamma'_1$$

$$\mu_2, \Gamma_2 \approx_{id_2, \sigma} \mu'_2, \Gamma'_2$$

$$\mu_1, \Gamma_1 \approx_{\beta, \sigma} \mu_2, \Gamma_2$$

Where $id_1$ and $id_2$ correspond to the identity function defined on the domain of $\mu_1$ and the identity function defined on the domain of $\mu_2$ respectively. Then, it follows that: $\mu'_1, \Gamma'_1 \approx_{\beta, \sigma} \mu'_2, \Gamma'_2$.

## A.2 Proofs: Confinement and Noninterference

**Lemma 13 (Confinement).** Given a program $s$, a memory $\mu$, a labeling $\langle \Gamma, \Sigma \rangle$, a level $\sigma_{pc}$ and a reference $r$ s.t.: $r, \sigma_{pc} \vdash \langle \mu, e, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma \rangle$ (hyp.1) for some memory $\mu'$, value $v$, labeling $\langle \Gamma', \Sigma' \rangle$ and security level $\sigma$; then for every security level $\sigma' \in \mathcal{L}$ such that $\sigma_{pc} \le \sigma'$ (hyp.2): $\mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu', \Gamma', \Sigma'$, where $id$ is the identity function defined on the domain of $\mu$.

*Proof.* Consider an arbitrary $\sigma'$ such that $\sigma_{pc} \le \sigma'$, the proof proceeds by induction on the depth of the derivation tree of: $\sigma_{pc}, r_s \vdash \langle \mu, e, \Gamma \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \sigma \rangle$. We distinguish two types of base cases:

- Those that do not change neither the memory nor the labeling: [VALUE], [THIS], and [VARIABLE]. Since $\mu' = \mu, \Gamma' = \Gamma$, and $\Sigma = \Sigma'$, using the reflexivity of $\approx_{id, \sigma'}$, we conclude that $\mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu', \Gamma', \Sigma'$.

- Those that change the heap by adding a new object: [FUNCTION LITERAL] and [OBJECT LITERAL].

Analogously, we distinguish four types of inductive cases:
1. Those that do not directly change the heap: [BINARY OPERATION], [PROPERTY LOOK-UP], [SEQUENCE], and [CONDITIONAL].

2. Those that directly change the heap by allocating a new object: [FUNCTION CALL] and [METHOD CALL].

3. Those that directly change the heap either by creating a new property or by updating the value of an existing property of an object: [VARIABLE ASSIGNMENT] and [PROPERTY ASSIGNMENT].

We prove one case of each type (the others are analogous).

[FUNCTION LITERAL] Suppose that $e = \text{function}(x)\{e\}$ (hyp.3). We conclude that there is a reference $r_f$ such that:

$$ - \mu' = \mu[r_f \mapsto [\text{@fscope} \mapsto r, \text{@code} \mapsto \lambda x.e]] \quad (1) - \text{hyp.1} + \text{hyp.3} $$

$$ - \Gamma' = \Gamma[r_f \mapsto [\text{@fscope} \mapsto \sigma_{pc}, \text{@code} \mapsto \sigma_{pc}]] \quad (2) - \text{hyp.1} + \text{hyp.3} $$

$$ - \Sigma' = \Sigma[r_f \mapsto \sigma_{pc}] \quad (3) - \text{hyp.1} + \text{hyp.3} $$

$$ - \mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu', \Gamma', \Sigma' \quad (4) - \text{hyp.2} + (1) - (3) + \text{High Object Creation Lemma} $$

[PROPERTY ASSIGNMENT] Suppose that $e = e_0[e_1] = e_2$ (hyp.3). We conclude that there are three memories $\mu_0$, $\mu_1$, and $\mu_2$, three labelings $\langle \Gamma_0, \Sigma_0 \rangle$, $\langle \Gamma_1, \Sigma_1 \rangle$, and $\langle \Gamma_2, \Sigma_2 \rangle$, a reference $r_0$, a string $m_1 \in \text{Str}$, and three security levels $\sigma_0$, $\sigma_1$, and $\sigma_2$ such that:

$$ - r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad (1) - \text{hyp.1} + \text{hyp.3} $$

$$ - r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, m_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle \quad (2) - \text{hyp.1} + \text{hyp.3} $$

$$ - r, \sigma_{pc} \vdash \langle \mu_1, e_2, \Gamma_1, \Sigma_1 \rangle \Downarrow_{IF} \langle \mu_2, v_2, \Gamma_2, \Sigma_2, \sigma_2 \rangle \quad (3) - \text{hyp.1} + \text{hyp.3} $$

$$ - \mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu_0, \Gamma_0, \Sigma_0 \quad (4) - \text{hyp.2} + (1) + \text{ih} $$

$$ - \mu_0, \Gamma_0, \Sigma_0 \approx_{id, \sigma'} \mu_1, \Gamma_1, \Sigma_1 \quad (5) - \text{hyp.2} + (2) + \text{ih} $$

$$ - \mu_1, \Gamma_1, \Sigma_1 \approx_{id, \sigma'} \mu_2, \Gamma_2, \Sigma_2 \quad (6) - \text{hyp.2} + (3) + \text{ih} $$

$$ - \mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu_2, \Gamma_2, \Sigma_2 \quad (7) - (4) - (6) + \text{Transitivity of } \approx_{id, \sigma'} $$

$$ - \sigma_{pc} \le \sigma_0 \sqcap \sigma_1 \sqcap \sigma_2 \quad (8) - (1) - (3) + \text{Conservation Lemma} $$

$$ - \sigma_0 \sqcap \sigma_1 \sqcap \sigma_2 \le \sigma' \quad (9) - \text{hyp.2} + (8) $$

$$ - \mu' = \mu_2[r_0 \mapsto \mu_2(r_0)[m_1 \mapsto v_2]] \quad (10) - \text{hyp.1} + \text{hyp.3} $$

$$ - \Gamma' = \Gamma_2[r_0 \mapsto \Gamma_2(r_0)[m_1 \mapsto \sigma_0 \sqcup \sigma_1 \sqcup \sigma_2]] \quad (11) - \text{hyp.1} + \text{hyp.3} $$

$$ - \Sigma' = \Sigma \quad (12) - \text{hyp.1} + \text{hyp.3} $$

Case $m_1 \in \mu_2(r_0)$ (hyp.4):

$$ \bullet \sigma_0 \sqcup \sigma_1 \le \Gamma_2(r_0)(m_1) \quad (13.1) - \text{hyp.1} + \text{hyp.3} + \text{hyp.4} $$

$$ \bullet \Gamma_2(r_0)(m_1) \le \sigma' \quad (13.2) - (9) + (13.1) $$

$$ \bullet \mu_2, \Gamma_2, \Sigma_2 \approx_{id, \sigma'} \mu', \Gamma', \Sigma' \quad (13.3) - (10) - (12) + (13.2) + \text{High Property Update Lemma} $$

$$ \bullet \mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu', \Gamma', \Sigma' \quad (13.4) - (7) + (13.3) + \text{Transitivity of } \approx_{id, \sigma'} $$

Case $m_1 \notin \mu_2(r_0)$ (hyp.4):

$$ \bullet \sigma_0 \sqcup \sigma_1 \le \Sigma_2(r_0) \quad (14.1) - \text{hyp.1} + \text{hyp.3} + \text{hyp.4} $$

$$ \bullet \Sigma_2(r_0) \le \sigma' \quad (14.2) - (9) + (14.1) $$

$$ \bullet \mu_2, \Gamma_2, \Sigma_2 \approx_{id, \sigma'} \mu', \Gamma', \Sigma' \quad (14.3) - (10) - (12) + (14.2) + \text{High Property Creation Lemma} $$

$$ \bullet \mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu', \Gamma', \Sigma' \quad (14.4) - (7) + (11.3) + \text{Transitivity of } \approx_{id, \sigma'} $$

$$ - \mu, \Gamma, \Sigma \approx_{id, \sigma'} \mu', \Gamma', \Sigma' \quad (15) - (13) + (14) $$
[FUNCTION CALL] Suppose that $e = e_0(e_1)$ (hyp.3). We conclude that there are three memories $\mu_0, \mu_1$, and $\hat{\mu}$, three labelings $\langle \Gamma_0, \Sigma_0 \rangle, \langle \Gamma_1, \Sigma_1 \rangle$, and $\langle \hat{\Gamma}, \hat{\Sigma} \rangle$, a reference $r_0$, a value $v_1$, four security levels $\sigma_0, \sigma_1, \sigma_2$, and $\hat{\sigma}$, and an expression $\hat{e}$ such that:

$$- r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad (1) - \text{hyp.1} + \text{hyp.3}$$

$$- r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, m_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle \quad (2) - \text{hyp.1} + \text{hyp.3}$$

$$- \langle \mu_1, \Gamma_1, \Sigma_1, r_0, v_1, \#glob, \sigma_0, \sigma_1 \rangle \mathcal{R}_{\text{NewScope}} \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma}, \hat{r}, \hat{\sigma}_{pc} \rangle \quad (3) - \text{hyp.1} + \text{hyp.3}$$

$$- \hat{r}, \hat{\sigma}_{pc} \vdash \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma} \rangle \Downarrow_{IF} \langle \mu', v, \Gamma', \Sigma', \sigma' \rangle \quad (4) - \text{hyp.1} + \text{hyp.3}$$

$$- \mu, \Gamma, \Sigma \approx_{id,\sigma'} \mu_0, \Gamma_0, \Sigma_0 \quad (5) - \text{hyp.2} + (1) + \mathbf{ih}$$

$$- \mu_0, \Gamma_0, \Sigma_0 \approx_{id,\sigma'} \mu_1, \Gamma_1, \Sigma_1 \quad (6) - \text{hyp.2} + (2) + \mathbf{ih}$$

$$- \mu, \Gamma, \Sigma \approx_{id,\sigma'} \mu_1, \Gamma_1, \Sigma_1 \quad (7) - (5) + (6) + \text{Transitivity of } \approx_{id,\sigma'}$$

$$- \sigma_{pc} \le \sigma_0 \sqcap \sigma_1 \quad (8) - (1) + (2) + \sigma_{pc} - \text{Conservation Lemma}$$

$$- \sigma_0 \sqcap \sigma_1 \le \sigma' \quad (9) - \text{hyp.2} + (8)$$

$$- \mu_1, \Gamma_1, \Sigma_1 \approx_{id,\sigma'} \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \quad (10) - (3) + (9) + \text{High Scope Object Creation}$$

$$- \hat{\sigma}_{pc} \le \sigma' \quad (11) - (3) + (9) + \text{High Scope Object Creation}$$

$$- \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \approx_{id,\sigma'} \mu', \Gamma', \Sigma' \quad (12) - (4) + (11) + \mathbf{ih}$$

$$- \mu, \Gamma, \Sigma \approx_{id,\sigma'} \mu', \Gamma', \Sigma' \quad (13) - (7) + (10) + (12) + \text{Transitivity of } \approx_{id,\sigma'}$$

**Lemma 14 (Scope-Chain Indistinguishability).** Given two memories $\mu_0$ and $\mu_1$, two labelings $\langle \Gamma_0, \Sigma_0 \rangle$ and $\langle \Gamma_1, \Sigma_1 \rangle$, two references $r_0$ and $r_1$, a security level $\sigma$, and a string $m \in \text{Str}$ such that: $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta,\sigma} \mu_1, \Gamma_1, \Sigma_1$ (hyp.1), $r_0 \sim_{\beta} r_1$ (hyp.2), $\langle \mu_0, r_0, m \rangle \mathcal{R}_{\text{Scope}} r'_0$ (hyp.3), $\langle \mu_1, r_1, m \rangle \mathcal{R}_{\text{Scope}} r'_1$ (hyp.4), $\Sigma_0(r_0) \sqcup \Sigma_1(r_1) \le \sigma$ (hyp.5), it follows that: $r'_0 \sim_{\beta} r'_1$.

*Proof.* We proceed by induction on the derivation of $\langle \mu_0, r_0, m \rangle \mathcal{R}_{\text{Scope}} r'_0$. The base cases are [NULL] and [BASE], whereas the inductive case is [LOOK-UP].

[NULL] Suppose that $r_0 = \text{null}$ (hyp.6). We conclude that:

$$- r'_0 = \text{null} \quad (1) - \text{hyp.3} + \text{hyp.6}$$

$$- r'_1 = \text{null} \quad (2) - \text{hyp.2} + (1)$$

$$- r'_0 \sim_{\beta} r'_1 \quad (3) - (1) + (2)$$

[BASE] Suppose that $m \in \text{dom}(\mu_0(r_0))$ (hyp.6). We conclude that:

$$- r'_0 = r_0 \quad (1) - \text{hyp.3} + \text{hyp.6}$$

$$- \text{dom}(\mu_0(r_0)) = \text{dom}(\mu_1(r_1)) \quad (2) - \text{hyp.2} + \text{hyp.5}$$

$$- m \in \text{dom}(\mu_1(r_1)) \quad (3) - \text{hyp.6} + (2)$$

$$- r'_1 = r_1 \quad (4) - \text{hyp.4} + (3)$$

$$- r'_0 \sim_{\beta} r'_1 \quad (5) - \text{hyp.2} + (1) + (4)$$

[LOOK-UP] Suppose that $m \notin \text{dom}(\mu_0(r_0))$ (hyp.6) and $r_0 \ne \text{null}$ (hyp.7). We conclude that:

$$- \langle \mu_0, r''_0, m \rangle \mathcal{R}_{\text{Scope}} r'_0, \text{ where: } r''_0 = \mu_0(r_0) \text{ (@scope)} \quad (1) - \text{hyp.3} + \text{hyp.6} + \text{hyp.7}$$

$$- \text{dom}(\mu_0(r_0)) = \text{dom}(\mu_1(r_1)) \quad (2) - \text{hyp.2} + \text{hyp.5}$$

$$- m \notin \text{dom}(\mu_1(r_1)) \text{ and } r_1 \ne \text{null} \quad (3) - \text{hyp.6} + \text{hyp.7} + (2)$$

$$- \langle \mu_1, r''_1, m \rangle \mathcal{R}_{\text{Scope}} r'_1, \text{ where: } r''_1 = \mu_1(r_1) \text{ (@scope)} \quad (4) - \text{hyp.4} + (3)$$
$$- \Sigma_i(r_i'') \le \Sigma_i(r_i) = \Gamma_i(r_i)(@scope) \text{ for } i = 0, 1 \qquad (5) - (1) + (4) + \text{Well-ordered scope-chains}$$

$$- \Gamma_i(r_i)(@scope) \le \sigma, \text{ for } i = 0, 1 \qquad (6) - \text{hyp. 5} + (5)$$

$$- r_0'' \sim_{\beta} r_1'' \qquad (7) - \text{hyp. 1} + \text{hyp. 2} + (6)$$

$$- \Sigma_i(r_i'') \le \sigma, \text{ for } i = 0, 1 \qquad (8) - \text{hyp. 5} + (5)$$

$$- r_0' \sim_{\beta} r_1' \qquad (9) - \text{hyp. 1} + (1) + (4) + (7) + (8) + \mathbf{ih}$$

**Lemma 15 (Prototype-Chain Indistinguishability).** Given two memories $\mu_0$ and $\mu_1$, two labeling $\langle \Gamma_0, \Sigma \rangle$ and $\langle \Gamma_1, \Sigma_1 \rangle$, two references $r_0$ and $r_1$, a security level $\sigma$, a function $\beta$, and a string $m \in \text{Str}$ such that: $\mu_0, \Gamma_0 \approx_{\beta, \sigma} \mu_1, \Gamma_1$ (hyp.1), $r_0 \sim_{\beta} r_1$ (hyp.2), $\langle \mu_0, r_0, m, \Gamma_0 \rangle \mathcal{R}_{\text{Proto}} \langle r_0', \sigma_0 \rangle$ (hyp.3), $\langle \mu_1, r_1, m, \Gamma_1 \rangle \mathcal{R}_{\text{proto}} \langle r_1', \sigma_1 \rangle$ (hyp.4); it holds that: $\sigma_i \le \sigma \Rightarrow (r_0' \sim_{\beta} r_1' \wedge \sigma_0 \sqcup \sigma_1 \le \sigma)$, for $i = 0, 1$.

*Proof.* To prove the result one has to prove the implication for $i = 0$ and $i = 1$. We prove the result for $i = 0$. The proof for $i = 1$ is symmetric. We proceed by induction on the derivation of hyp.3 and we assume that $\sigma_0 \le \sigma$ (hyp.5). The base cases are [NULL] and [BASE], whereas the inductive case is [LOOK-UP].

[NULL] Suppose that $r_0 = \text{null}$ (hyp.6). We conclude that:

$$- r_0' = \text{null} \text{ and } \sigma_0 = \perp \qquad (1) - \text{hyp. 3} + \text{hyp. 6}$$

$$- r_1 = \text{null} \qquad (2) - \text{hyp. 2} + \text{hyp. 6}$$

$$- r_1' = \text{null} \text{ and } \sigma_1 = \perp \qquad (3) - \text{hyp. 4} + (2)$$

$$- r_0' \sim_{\beta} r_1' \text{ and } \sigma_0 \sqcup \sigma_1 \le \sigma \qquad (4) - (1) + (3)$$

[BASE] Suppose that $m \in \text{dom}(\mu_0(r_0))$ (hyp.6). We conclude that:

$$- r_0' = r_0 \text{ and } \sigma_0 = \Gamma_0(r_0)(m) \qquad (1) - \text{hyp. 3} + \text{hyp. 6}$$

$$- \Gamma_0(r_0)(m) \le \sigma \qquad (2) - \text{hyp. 5} + (1)$$

$$- m \in \text{dom}(\mu_1(r_1)) \text{ and } \Gamma_0(r_0)(m) \sqcup \Gamma_1(r_1)(m) \le \sigma \qquad (3) - \text{hyp. 1} + \text{hyp. 2} + (2)$$

$$- r_1' = r_1 \text{ and } \sigma_1 = \Gamma_1(r_1)(m) \qquad (4) - \text{hyp. 4} + (3)$$

$$- r_0' \sim_{\beta} r_1' \text{ and } \sigma_0 \sqcup \sigma_1 \le \sigma \qquad (5) - (1) + (3) + (4)$$

[LOOK-UP] Suppose that $m \notin \text{dom}(\mu_0(r_0))$ (hyp.6) and $r_0 \ne \text{null}$ (hyp.7). We conclude that there is a security level $\sigma_0'$ such that:

$$- \langle \mu_0, r_0'', m, \Gamma_0, \Sigma_0 \rangle \mathcal{R}_{\text{Proto}} \langle r_0', \sigma_0' \rangle \text{ and } \sigma_0 = \Gamma_0(r_0)(\text{-prot}_-) \sqcup \Sigma_0(r_0) \sqcup \sigma_0' \qquad (1) - \text{hyp. 3} + \text{hyp. 6} + \text{hyp. 7}$$

$$- \Sigma_0(r_0) \le \sigma \qquad (2) - \text{hyp. 5} + (1)$$

$$- r_1 \ne \text{null} \qquad (3) - \text{hyp. 2} + \text{hyp. 7}$$

$$- \text{dom}(\mu_0(r_0)) = \text{dom}(\mu_1(r_1)) \text{ and } \Sigma_1(r_1) \le \sigma \qquad (4) - \text{hyp. 1} + \text{hyp. 2} + (2)$$

$$- m \notin \text{dom}(\mu_1(r_1)) \qquad (5) - \text{hyp. 6} + (4)$$

$$- \langle \mu_1, r_1'', m, \Gamma_1, \Sigma_1 \rangle \mathcal{R}_{\text{Proto}} \langle r_1', \sigma_1' \rangle \text{ and } \sigma_1 = \Gamma_1(r_1)(\text{-prot}_-) \sqcup \Sigma_1(r_1) \sqcup \sigma_1' \qquad (6) - \text{hyp. 4} + (3) + (4)$$

$$- \Gamma_0(r_0)(\text{-prot}_-) \le \sigma \qquad (7) - \text{hyp. 5} + (1)$$

$$- r_0'' \sim_{\beta} r_1'' \text{ and } \Gamma_i(r_i)(\text{-prot}_-) \le \sigma \text{ for } i = 0, 1 \qquad (8) - \text{hyp. 1} + \text{hyp. 2} + (1) + (6) + (7)$$

$$- \sigma_0' \le \sigma \Rightarrow (r_0' \sim_{\beta} r_1' \wedge \sigma_0' \sqcup \sigma_1' \le \sigma) \qquad (9) - \text{hyp. 1} + (1) + (6) + (8) + \mathbf{ih}$$

$$- \sigma_0' \le \sigma \qquad (10) - \text{hyp. 5} + (1)$$

$$- \sigma_0' \le \sigma \qquad (10) - \text{hyp. 5} + (1)$$
$$ - \sigma_1' \le \sigma \text{ and } r_0' \sim \beta r_1' \qquad (11) - (9) + (10) $$

$$ - \sigma_1 \le \sigma_0 \qquad (12) - (4) + (6) + (8) + (11) $$

**Lemma 16 (Noninterference).** For any expression $e$, memories $\mu$ and $\mu'$, respectively labeled by $\langle\Gamma, \Sigma\rangle$ and $\langle\Gamma', \Sigma'\rangle$, a reference $r$, and security levels $\sigma_{pc}$ and $\sigma$, if there exists a function $\beta$ on $\mathcal{R}ef$ such that: $\mu, \Gamma, \Sigma \approx_{\beta, \sigma} \mu', \Gamma', \Sigma'$ (hyp.1), $r, \sigma_{pc} \vdash \langle\mu, e, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f\rangle$ (hyp.2), and $\beta(r), \sigma_{pc} \vdash \langle\mu', e, \Gamma', \Sigma'\rangle \Downarrow_{IF} \langle\mu'_f, v'_f, \Gamma'_f, \Sigma'_f, \sigma'_f\rangle$ (hyp.3); it follows that there exists a function $\beta'$ that extends $\beta$ s.t. $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f$ and $(\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta'} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma)$.

*Proof.* If $\sigma_{pc} \le \sigma$, we apply the Confinement Lemma (Lemma 13) to the hyp.2 and hyp.3 and conclude that $\mu, \Gamma, \Sigma \approx_{id, \sigma} \mu_f, \Gamma_f, \Sigma_f$ and $\mu', \Gamma', \Sigma' \approx_{id, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f$. Applying the Lateral Transitivity of $\approx_{id, \sigma}$, we conclude that $\mu', \Gamma' \approx_{\beta, \sigma} \mu'_f, \Gamma'_f$. Applying the $\sigma_{pc}$-Conservation Lemma, we conclude that $\sigma_{pc} \le \sigma_f \sqcap \sigma'_f$. Since we are assuming that $\sigma_{pc} \le \sigma$, we conclude that both $v_f$ and $v'_f$ are not observable.

In the following, we assume $\sigma_{pc} \le \sigma$ (hyp.4). We proceed by induction on the depth of the derivation tree of hyp.2. In the following let $\beta(r) = r'$. With respect to the second claim of the theorem, in every case, we only prove $\sigma_f \le \sigma \Rightarrow v_f \sim_{\beta'} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma$. The proof of the symmetric implication $\sigma'_f \le \sigma \Rightarrow v_f \sim_{\beta'} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma$ is always done in the exact same way.

[VALUE] Suppose that $e = v$ (hyp.5). We conclude that:

$$ - r, \sigma_{pc} \vdash \langle\mu, v, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu, v, \Gamma, \Sigma, \sigma_{pc}\rangle \qquad (1) - \text{hyp.2} + \text{hyp.5} $$

$$ - r', \sigma_{pc} \vdash \langle\mu', v, \Gamma', \Sigma'\rangle \Downarrow_{IF} \langle\mu', v, \Gamma', \Sigma', \sigma_{pc}\rangle \qquad (2) - \text{hyp.3} + \text{hyp.5} $$

$$ - \mu_f = \mu, \Gamma_f = \Gamma, \Sigma_f = \Sigma, v_f = v, \text{ and } \sigma_f = \sigma_{pc} \qquad (3) - \text{hyp.3} + (1) $$

$$ - \mu'_f = \mu', \Gamma'_f = \Gamma', \Sigma'_f = \Sigma', v'_f = v', \text{ and } \sigma'_f = \sigma_{pc} \qquad (4) - \text{hyp.4} + (2) $$

$$ - \mu_f, \Gamma_f, \Sigma_f \approx_{\beta', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \qquad (5) - \text{hyp.1} + (3) + (4) $$

$$ - v_f \sim_{\beta} v'_f \text{ and } \sigma_f \sqcup \sigma'_f \le \sigma \qquad (6) - \text{hyp.4} + (3) + (4) $$

$$ - \sigma_f \le \sigma \Rightarrow v_f \sim_{\beta} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma \qquad (7) - (6) $$

[THIS] Suppose that $e = \text{this}$ (hyp.5). We conclude that:

$$ - r, \sigma_{pc} \vdash \langle\mu, \text{this}, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu, v_f, \Gamma, \Sigma, \sigma_f\rangle \qquad (1) - \text{hyp.2} + \text{hyp.5} $$

$$ - r', \sigma_{pc} \vdash \langle\mu', \text{this}, \Gamma', \Sigma'\rangle \Downarrow_{IF} \langle\mu', v'_f, \Gamma', \Sigma', \sigma'_f\rangle \qquad (2) - \text{hyp.3} + \text{hyp.5} $$

$$ - \mu_f = \mu, \Gamma_f = \Gamma, \Sigma_f = \Sigma, \mu'_f = \mu', \Gamma'_f = \Gamma', \text{ and } \Sigma'_f = \Sigma' \qquad (3) - \text{hyp.2} + \text{hyp.3} + (1) + (2) $$

$$ - \mu_f, \Gamma_f, \Sigma_f \approx_{\beta', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \qquad (4) - \text{hyp.1} + (3) $$

$$ - \Gamma(r)(@this) \le \sigma \Rightarrow v_f \sim_{\beta} v'_f \land \Gamma(r)(@this) \sqcup \Gamma'(r')(@this) \le \sigma \qquad (5) - \text{hyp.1} $$

$$ - \sigma_f \le \sigma \Rightarrow v_f \sim_{\beta} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma \qquad (6) - (1) + (2) + (5) $$

[BINARY OPERATION] Suppose that $e = e_0 \circ p e_1$ (hyp.5). We conclude that:

$$ - r, \sigma_{pc} \vdash \langle\mu, e_0, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0\rangle \qquad (1) - \text{hyp.2} + \text{hyp.5} $$
- $r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, v_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle$ (2) - hyp.2 + hyp.5

- $r', \sigma_{pc} \vdash \langle \mu', e_0, \Gamma', \Sigma' \rangle \Downarrow_{IF} \langle \mu'_0, v'_0, \Gamma'_0, \Sigma'_0, \sigma'_0 \rangle$ (3) - hyp.3 + hyp.5

- $r', \sigma_{pc} \vdash \langle \mu'_0, e_1, \Gamma'_0, \Sigma'_0 \rangle \Downarrow_{IF} \langle \mu'_1, v'_1, \Gamma'_1, \Sigma'_1, \sigma'_1 \rangle$ (4) - hyp.3 + hyp.5

- $v_f = v_0 \text{ op } v_1$ and $\sigma_f = \sigma_0 \sqcup \sigma_1$ (5) - hyp.2 + hyp.5

- $v'_f = v'_0 \text{ op } v'_1$ and $\sigma'_f = \sigma'_0 \sqcup \sigma'_1$ (6) - hyp.3 + hyp.5

- $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta', \sigma} \mu'_0, \Gamma'_0, \Sigma'_0$, for some $\beta'$ extending $\beta$ (7) - hyp.1 + (1) + (3) + \text{ih}$

- $(\sigma_0 \le \sigma \lor \sigma'_0 \le \sigma) \Rightarrow (v_0 \sim_{\beta'} v'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma)$ (8) - hyp.1 + (1) + (3) + \text{ih}$

- $\mu_1, \Gamma_1, \Sigma_1 \approx_{\beta'', \sigma} \mu'_1, \Gamma'_1, \Sigma'_1$, for some $\beta''$ extending $\beta''$ (9) - (2) + (4) + (7) + \text{ih}$

- $(\sigma_1 \le \sigma \lor \sigma'_1 \le \sigma) \Rightarrow (v_1 \sim_{\beta''} v'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma)$ (10) - (2) + (4) + (7) + \text{ih}$

- $\sigma_f \le \sigma \Rightarrow v_f \sim_{\beta} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma$ Suppose: $\sigma_f \le \sigma$ (hyp.6):

• $\sigma_0 \sqcup \sigma_1 \le \sigma$ (11.1) - hyp.6 + (5)

• $v_0 \sim_{\beta'} v'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma$ (11.2) - (8) + (11.1)

• $v_1 \sim_{\beta''} v'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma$ (11.3) - (10) + (11.2)

• $v_f \sim_{\beta''} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma$ (11.4) - (5) + (6) + (11.1) - (11.3)

[VARIABLE] Suppose that $e = x$ (hyp.5). We conclude that:

- $\mu_f = \mu, \Gamma_f = \Gamma, \Sigma_f = \Sigma, \langle \mu, r, x \rangle \mathcal{R}_{Scope} r_x, v_f = \mu(r_x)(x), \sigma_f = \Gamma(r_x)(x) \sqcup \sigma_{pc}$ (1) - hyp.2 + hyp.5

- $\mu'_f = \mu', \Gamma'_f = \Gamma', \Sigma'_f = \Sigma', \langle \mu', r', x \rangle \mathcal{R}_{Scope} r'_x, v'_f = \mu'(r'_x)(x), \sigma'_f = \Gamma'(r'_x)(x) \sqcup \sigma_{pc}$ (2) - hyp.3 + hyp.5

- $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f$ (3) - hyp.1 + (1) + (2)

- $\Sigma(r) \sqcup \Sigma'(r') \le \sigma_{pc}$ (4) - Well-formed big-step transitions

- $\Sigma(r) \sqcup \Sigma'(r') \le \sigma$ (5) - hyp.4 + (4)

- $r_x \sim_{\beta} r'_x$ (6) - hyp.1 + (1) + (2) + (5) + Scope-Chain Indistinguishability

- $\Gamma(r_x)(x) \le \sigma \Rightarrow v_f \sim_{\beta} v'_f \land \Gamma(r_x)(x) \sqcup \Gamma'(r'_x)(x) \le \sigma$ (7) - hyp.1 + (6)

- $\sigma_f \le \sigma \Rightarrow v_f \sim_{\beta} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma$ (8) - (1) + (2) + (7)

[VARIABLE ASSIGNMENT] Suppose that $e = x = e$ (hyp.5). We conclude that:

- $r, \sigma_{pc} \vdash \langle \mu, e, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, v_f, \Gamma_0, \Sigma_0, \sigma_f \rangle$ (1) - hyp.2 + hyp.5

- $\langle \mu_0, r, x \rangle \mathcal{R}_{Scope} r_x, \sigma_{pc} \le \Gamma_0(r_x)(x)$, and $r_x \ne \text{null}$ (2) - hyp.2 + hyp.5

- $\Gamma_f = \Gamma_0 [r_x \mapsto \Gamma_0(r_x)] [x \mapsto \sigma_f]$ and $\mu_f = \mu_0 [r_x \mapsto \mu_0(r_x)] [x \mapsto v_f]$ (3) - hyp.2 + hyp.5

- $r', \sigma_{pc} \vdash \langle \mu', e, \Gamma', \Sigma' \rangle \Downarrow_{IF} \langle \mu'_0, v'_f, \Gamma'_0, \Sigma'_0, \sigma'_f \rangle$ (4) - hyp.3 + hyp.5

- $\langle \mu'_0, r', x \rangle \mathcal{R}_{Scope} r'_x, \sigma_{pc} \le \Gamma'_0(r'_x)(x)$, and $r'_x \ne \text{null}$ (5) - hyp.3 + hyp.5

- $\Gamma'_f = \Gamma'_0 [r'_x \mapsto \Gamma'_0(r'_x)] [x \mapsto \sigma'_f]$ and $\mu'_f = \mu'_0 [r'_x \mapsto \mu'_0(r'_x)] [x \mapsto v'_f]$ (6) - hyp.3 + hyp.5

- $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta', \sigma} \mu'_0, \Gamma'_0, \Sigma'_0$, for some $\beta'$ extending $\beta$ (7) - hyp.1 + (1) + (4) + \text{ih}$

- $(\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta'} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma)$ (8) - hyp.1 + (1) + (4) + \text{ih}$

- $\Sigma(r) \sqcup \Sigma'(r') \le \sigma_{pc}$ (9) - Well-formed big-step transitions

- $\Sigma(r) \sqcup \Sigma'(r') \le \sigma$ (10) - hyp.4 + (9)

- $r_x \sim_{\beta} r'_x$ (11) - hyp.1 + (2) + (5) + (10) + Scope-Chain Indistinguishability

- $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f$ (12) - (3) + (6) + (7) + (8) + Low-Equality Preserving Update

[PROPERTY LOOK-UP] Suppose that $e = e_0[e_1]$ (hyp.5). We conclude that:

- $r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle$ (1) - hyp.2 + hyp.5

- $r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_f, m_1, \Gamma_f, \Sigma_f, \sigma_1 \rangle$ (2) - hyp.2 + hyp.5
- $r', \sigma_{pc} \vdash \langle \mu', e_0, \Gamma', \Sigma' \rangle \Downarrow_{IF} \langle \mu'_0, r'_0, \Gamma'_0, \Sigma'_0, \sigma'_0 \rangle$ (3) - hyp.3 + hyp.5

- $r', \sigma_{pc} \vdash \langle \mu'_0, e_1, \Gamma'_0, \Sigma'_0 \rangle \Downarrow_{IF} \langle \mu'_f, m'_1, \Gamma'_f, \Sigma'_f, \sigma'_f \rangle$ (4) - hyp.3 + hyp.5

- $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta', \sigma} \mu'_0, \Gamma'_0, \Sigma'_0$, for some $\beta'$ extending $\beta$ (7) - hyp.1 + (1) + (3) + ih

- $(\sigma_0 \le \sigma \lor \sigma'_0 \le \sigma) \Rightarrow (r_0 \sim_{\beta'} r'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma)$ (8) - hyp.1 + (1) + (3) + ih

- $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta'', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f$, for some $\beta''$ extending $\beta'$ (9) - (2) + (4) + (7) + ih

- $(\sigma_1 \le \sigma \lor \sigma'_1 \le \sigma) \Rightarrow (m_1 \sim_{\beta''} m'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma)$ (10) - (2) + (4) + (7) + ih

- $\langle \mu_f, r_0, m_1, \Gamma_1, \Sigma_1 \rangle \mathcal{R}_{Proto} \langle \hat{r}, \hat{\sigma} \rangle$ and $\langle \mu'_f, r'_0, m'_1, \Gamma'_1, \Sigma'_1 \rangle \mathcal{R}_{Proto} \langle \hat{r}', \hat{\sigma}' \rangle$ (11) - hyp.2 + hyp.3 + hyp.5

- $\sigma_f \le \sigma \Rightarrow v_f \sim_{\beta''} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma$

Suppose: $\sigma_f \le \sigma$ (hyp.6) + $\hat{r} \neq null$ (hyp.7):

- $\sigma_f = \sigma_0 \sqcup \sigma_1 \sqcup \hat{\sigma} \sqcup \Gamma_f(\hat{r})(m_1)$ (12.1) - hyp.2 + hyp.5 + hyp.7

- $\sigma_0 \sqcup \sigma_1 \sqcup \hat{\sigma} \sqcup \Gamma_f(\hat{r})(m_1) \le \sigma$ (12.2) - hyp.6 + (12.1)

- $r_0 \sim_{\beta'} r'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma$ (12.3) - (8) + (12.2)

- $m_1 = m'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma$ (12.4) - (10) + (12.2)

- $\hat{r} \sim_{\beta''} \hat{r}'$ and $\hat{\sigma} \sqcup \hat{\sigma}' \le \sigma$ (12.5) - (9) + (11) + (12.2) + (12.3) + Prototype-Chain Indistinguishability

- $\hat{r}' \neq null$ (12.6) - hyp.7 + (12.5)

- $v_f = \mu_f(\hat{r})(m_1)$ and $v'_f = \mu'_f(\hat{r}')(m_1)$ (12.7) - hyp.2 + hyp.5 + hyp.7 + (12.6)

- $\Gamma_f(\hat{r})(m_1) \sqcup \Gamma'_f(\hat{r}')(m_1) \le \sigma$ and $v_f \sim_{\beta''} v'_f$ (12.8) - (9) + (12.1) + (12.5) + (12.7)

- $\sigma_f \sqcup \sigma'_f \le \sigma$ (12.9) - (12.2) + (12.3) + (12.4) + (12.8)

Suppose: $\sigma_f \le \sigma$ (hyp.6) + $\hat{r} = null$ (hyp.7):

- $\sigma_f = \sigma_0 \sqcup \sigma_1 \sqcup \hat{\sigma}$ (12.10) - hyp.2 + hyp.5 + hyp.7

- $\sigma_0 \sqcup \sigma_1 \sqcup \hat{\sigma} \le \sigma$ (12.11) - hyp.6 + (12.10)

- $r_0 \sim_{\beta'} r'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma$ (12.12) - (8) + (12.11)

- $m_1 = m'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma$ (12.13) - (10) + (12.11)

- $\hat{r} \sim_{\beta''} \hat{r}'$ and $\hat{\sigma} \sqcup \hat{\sigma}' \le \sigma$ (12.14) - (9) + (11) + (12.12) + (12.3) + Proptoype-Chain Indistinguishability

- $\hat{r}' = null$ (12.15) - hyp.7 + (12.14)

- $v_f = undefined$ and $v'_f = undefined$ (12.16) - hyp.2 + hyp.5 + hyp.7 + (12.15)

- $\sigma_f \sqcup \sigma'_f \le \sigma$ (12.17) - (12.11) + (12.13) + (12.14)

[PROPERTY ASSIGNMENT] Suppose that $e = e_0[e_1] = e_2$ (hyp.5). We conclude that:

- $r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle$ (1) - hyp.2 + hyp.5

- $r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, m_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle$ (2) - hyp.2 + hyp.5

- $r, \sigma_{pc} \vdash \langle \mu_1, e_2, \Gamma_1, \Sigma_1 \rangle \Downarrow_{IF} \langle \mu_2, v_f, \Gamma_2, \Sigma_f, \sigma_f \rangle$ (3) - hyp.2 + hyp.5

- $\mu_f = \mu_2 [r_0 \mapsto \mu_2(r_0) [m_1 \mapsto v_f]]$ and $\Gamma_f = \Gamma_2 [r_0 \mapsto \Gamma_2(r_0) [m_1 \mapsto \sigma_0 \sqcup \sigma_1 \sqcup \sigma_f]]$ (4) - hyp.2 + hyp.5

- $r', \sigma_{pc} \vdash \langle \mu', e_0, \Gamma', \Sigma' \rangle \Downarrow_{IF} \langle \mu'_0, r'_0, \Gamma'_0, \Sigma'_0, \sigma'_0 \rangle$ (5) - hyp.3 + hyp.5

- $r', \sigma_{pc} \vdash \langle \mu'_0, e_1, \Gamma'_0, \Sigma'_0 \rangle \Downarrow_{IF} \langle \mu'_1, m'_1, \Gamma'_1, \Sigma'_1, \sigma'_1 \rangle$ (6) - hyp.3 + hyp.5

- $r', \sigma_{pc} \vdash \langle \mu'_1, e_2, \Gamma'_1, \Sigma'_1 \rangle \Downarrow_{IF} \langle \mu'_2, v'_f, \Gamma'_2, \Sigma'_f, \sigma'_f \rangle$ (7) - hyp.3 + hyp.5

- $\mu'_f = \mu'_2 [r'_0 \mapsto \mu'_2(r'_0) [m'_1 \mapsto v'_f]]$ and $\Gamma'_f = \Gamma'_2 [r'_0 \mapsto \Gamma'_2(r'_0) [m'_1 \mapsto \sigma'_0 \sqcup \sigma'_1 \sqcup \sigma'_f]]$ (8) - hyp.3 + hyp.5

- $\mu_0, \Gamma_0, \Sigma_0 \approx_{\beta', \sigma} \mu'_0, \Gamma'_0, \Sigma'_0$, for some $\beta'$ extending $\beta$ (9) - hyp.1 + (1) + (5) + ih

- $(\sigma_0 \le \sigma \lor \sigma'_0 \le \sigma) \Rightarrow (r_0 \sim_{\beta'} r'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma)$ (10) - hyp.1 + (1) + (3) + ih

- $\mu_1, \Gamma_1, \Sigma_1 \approx_{\beta'', \sigma} \mu'_1, \Gamma'_1, \Sigma'_1$, for some $\beta''$ extending $\beta'$ (11) - (2) + (6) + (9) + ih

- $(\sigma_1 \le \sigma \lor \sigma'_1 \le \sigma) \Rightarrow (m_1 = m'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma)$ (12) - (2) + (6) + (9) + ih
- $\mu_2, \Gamma_2, \Sigma_f \approx_{\beta''',\sigma} \mu'_2, \Gamma'_2, \Sigma'_f$, for some $\beta''''$ extending $\beta''$

$$ (13) - (3) + (7) + (11) + \mathbf{ih} $$

- $(\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta''''} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma)$

$$ (14) - (3) + (7) + (11) + \mathbf{ih} $$

- $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta''',\sigma} \mu'_f, \Gamma'_f, \Sigma'_f$

Suppose: $\sigma_0 \sqcup \sigma_1 \le \sigma$ (hyp.6):

- $r_0 \sim_{\beta'} r'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma$ (15.1) - hyp.6 + (10)

- $m_1 = m'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma$ (15.2) - hyp.6 + (12)

- $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta''',\sigma} \mu'_f, \Gamma'_f, \Sigma'_f$

$$ (15.3) - (4) + (8) + (13) - (15.2) + \text{Visible Property Assignment} $$

There are four additional subcases to consider. We only consider one of them.

Suppose: $\sigma_0 \sqcup \sigma_1 \le \sigma$ (hyp.6), $m_1 \in \text{dom}(\mu_2(r_0))$ (hyp.7), and $m'_1 \notin \text{dom}(\mu'_2(r'_0))$ (hyp.8):

- $\sigma'_0 \sqcup \sigma'_1 \le \sigma$ (15.1) - hyp.6 + (10) + (12)

- $\sigma_0 \sqcup \sigma_1 \le \Gamma_2(r_0)(m_1)$ (15.2) - hyp.2 + hyp.5 + hyp.7

- $\Gamma_2(r_0)(m_1) \le \sigma$ (15.3) - hyp.6 + (15.2)

- $\sigma'_0 \sqcup \sigma'_1 \le \Sigma'_f(r'_0)$ (15.4) - hyp.3 + hyp.5 + hyp.8

- $\Sigma'_f(r'_0) \le \sigma$ (15.5) - (15.1) + (15.4)

- $\mu_2, \Gamma_2, \Sigma_f \approx_{id,\sigma} \mu_f, \Gamma_f, \Sigma_f$

$$ (15.6) - \text{hyp.7} + (4) + (15.3) + \text{Confined Property Update} $$

- $\mu'_2, \Gamma'_2, \Sigma'_f \approx_{id,\sigma} \mu'_f, \Gamma'_f, \Sigma'_f$

$$ (15.7) - \text{hyp.8} + (8) + (15.5) + \text{Confined Property Creation} $$

- $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta''',\sigma} \mu'_f, \Gamma'_f, \Sigma'_f$

$$ (15.8) - (13) + (15.6) + (15.7) + \text{Lateral} $$

Transitivity of $\approx_{\beta,\sigma}$

[FUNCTION LITERAL] Suppose that $e = \text{function}(x)\{e\}$ (hyp.5). We conclude that there are two references $r_f$ and $r'_f$ such that:

- $\mu_f = \mu[r_f \mapsto [\text{@fscope} \mapsto r, \text{@code} \mapsto \lambda x.e]]$ (1) - hyp.2 + hyp.5

- $\Gamma_f = \Gamma[r_f \mapsto [\text{@fscope} \mapsto \sigma_{pc}, \text{@code} \mapsto \sigma_{pc}]]$ and $\Sigma_f = \Sigma[r_f \mapsto \sigma_{pc}]$

$$ (2) - \text{hyp.2} + \text{hyp.5} $$

- $v_f = r_f, \sigma_f = \sigma_{pc}$, and $r_f \notin \text{dom}(\mu)$ (3) - hyp.2 + hyp.5

- $\mu'_f = \mu'[r'_f \mapsto [\text{@fscope} \mapsto r', \text{@code} \mapsto \lambda x.e]]$ (4) - hyp.3 + hyp.5

- $\Gamma'_f = \Gamma'[r'_f \mapsto [\text{@fscope} \mapsto \sigma_{pc}, \text{@code} \mapsto \sigma_{pc}]]$ and $\Sigma_f = \Sigma'[r'_f \mapsto \sigma_{pc}]$

$$ (5) - \text{hyp.3} + \text{hyp.5} $$

- $v'_f = r'_f, \sigma'_f = \sigma_{pc}$, and $r'_f \notin \text{dom}(\mu')$ (6) - hyp.3 + hyp.5

Let $\beta' = \beta[r_f \mapsto r'_f]$ (hyp.6). We conclude that:

- $\mu_f, \Gamma_f, \Sigma_f \approx_{\beta',\sigma} \mu'_f, \Gamma'_f, \Sigma'_f$ (7) - hyp.1 + hyp.6 + (1) + (2) + (4) + (5)

- $v_f \sim_{\beta'} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma$ (8) - hyp.4 + hyp.6 + (3) + (6)

- $(\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta'} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma)$ (9) - (8)

[OBJECT LITERAL] Suppose that $e = \{\}$ (hyp.5). We conclude that there are two references $r_o$ and $r'_o$ such that:

- $\mu_f = \mu[r_o \mapsto [-\text{prot}_- \mapsto \text{null}]]$ (1) - hyp.2 + hyp.5

- $\Gamma_f = \Gamma[r_o \mapsto [-\text{prot}_- \mapsto \sigma_{pc}]]$ and $\Sigma_f = \Sigma[r_o \mapsto \sigma_{pc}]$ (2) - hyp.2 + hyp.5

- $v_f = r_o, \sigma_f = \sigma_{pc}$, and $r_o \notin \text{dom}(\mu)$ (3) - hyp.2 + hyp.5

- $\mu'_f = \mu'[r'_o \mapsto [-\text{prot}_- \mapsto \text{null}]]$ (4) - hyp.3 + hyp.5

- $\Gamma'_f = \Gamma'[r'_o \mapsto [-\text{prot}_- \mapsto \sigma_{pc}]]$ and $\Sigma'_f = \Sigma'[r'_o \mapsto \sigma_{pc}]$ (5) - hyp.3 + hyp.5
$$ - v'_{f} = r'_{o}, \sigma'_{f} = \sigma_{pc}, \text{ and } r'_{o} \notin \text{dom}(\mu') \quad (6) - \text{hyp.3 + hyp.5} $$

Let $\beta' = \beta[r_o \mapsto r'_o]$ (hyp.6). We conclude that:

$$ - \mu_f, \Gamma_f, \Sigma_f \approx_{\beta', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (7) - \text{hyp.1 + hyp.6 + (1) + (2) + (4) + (5)} $$

$$ - v_f \sim_{\beta'} v'_f \wedge \sigma_f \sqcup \sigma'_f \le \sigma \quad (8) - \text{hyp.4 + hyp.6 + (3) + (6)} $$

$$ - (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta'} v'_f \wedge \sigma_f \sqcup \sigma'_f \le \sigma) \quad (9) - (8) $$

**[FUNCTION CALL]** Suppose that $e = e_0(e_1)$ (hyp.5). We conclude that:

$$ - r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad (1) - \text{hyp.2 + hyp.5} $$

$$ - r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, v_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle \quad (2) - \text{hyp.2 + hyp.5} $$

$$ - r', \sigma_{pc} \vdash \langle \mu', e_0, \Gamma', \Sigma' \rangle \Downarrow_{IF} \langle \mu'_0, r'_0, \Gamma'_0, \Sigma'_0, \sigma'_0 \rangle \quad (3) - \text{hyp.3 + hyp.5} $$

$$ - r', \sigma_{pc} \vdash \langle \mu'_0, e_1, \Gamma'_0, \Sigma'_0 \rangle \Downarrow_{IF} \langle \mu'_1, v'_1, \Gamma'_1, \Sigma'_1, \sigma'_1 \rangle \quad (4) - \text{hyp.3 + hyp.5} $$

$$ - \mu_0, \Gamma_0, \Sigma_0 \approx_{\beta', \sigma} \mu'_0, \Gamma'_0, \Sigma'_0, \text{ for some } \beta' \text{ extending } \beta \quad (5) - \text{hyp.1 + (1) + (3) + ih} $$

$$ - (\sigma_0 \le \sigma \lor \sigma'_0 \le \sigma) \Rightarrow (r_0 \sim_{\beta'} r'_0 \wedge \sigma_0 \sqcup \sigma'_0 \le \sigma) \quad (6) - \text{hyp.1 + (1) + (3) + ih} $$

$$ - \mu_1, \Gamma_1, \Sigma_1 \approx_{\beta'', \sigma} \mu'_1, \Gamma'_1, \Sigma'_1, \text{ for some } \beta'' \text{ extending } \beta' \quad (7) - (2) + (4) + (5) + ih $$

$$ - (\sigma_1 \le \sigma \lor \sigma'_1 \le \sigma) \Rightarrow (v_1 \sim_{\beta''} v'_1 \wedge \sigma_1 \sqcup \sigma'_1 \le \sigma) \quad (8) - (2) + (4) + (5) + ih $$

$$ - \langle \mu_1, \Gamma_1, \Sigma_1, r_0, v_1, \#glob, \sigma_0, \sigma_1 \rangle \mathcal{R}_{NewScope} \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma}, \hat{r}, \hat{\sigma}_{pc} \rangle \quad (9) - \text{hyp.2 + hyp.5} $$

$$ - \hat{r}, \hat{\sigma}_{pc} \vdash \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma} \rangle \Downarrow_{IF} \langle \mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f \rangle \quad (10) - \text{hyp.2 + hyp.5} $$

$$ - \langle \mu'_1, \Gamma'_1, \Sigma'_1, r'_0, v'_1, \#glob, \sigma'_0, \sigma'_1 \rangle \mathcal{R}_{NewScope} \langle \hat{\mu}', \hat{e}', \hat{\Gamma}', \hat{\Sigma}', \hat{r}', \hat{\sigma}'_{pc} \rangle \quad (11) - \text{hyp.3 + hyp.5} $$

$$ - \hat{r}', \hat{\sigma}'_{pc} \vdash \langle \hat{\mu}', \hat{e}', \hat{\Gamma}', \hat{\Sigma}' \rangle \Downarrow_{IF} \langle \mu'_f, v'_f, \Gamma'_f, \Sigma'_f, \sigma'_f \rangle \quad (12) - \text{hyp.3 + hyp.5} $$

We consider two distinct cases: $\sigma_0 \le \sigma$ and $\sigma_0 \not\le \sigma$.

Suppose that $\sigma_0 \le \sigma$ (hyp.6):

$$ - \sigma_0 \sqcup \sigma'_0 \le \sigma \text{ and } r_0 \sim_{\beta''} r'_0 \quad (13) - \text{hyp.6 + (6)} $$

$$ - \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \approx_{\beta''', \sigma} \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}', \hat{e} = \hat{e}', \hat{\sigma}'_{pc} = \hat{\sigma}_{pc} = \sigma_0 = \sigma'_0 \le \sigma \quad (14) - (6) - (9) + (11) + (13) + \text{Visible Scope All.} $$

$$ - \mu_f, \Gamma_f, \Sigma_f \approx_{\beta''', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \text{ and } (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta''''} v'_f \wedge \sigma_f \sqcup \sigma'_f \le \sigma) \quad (15) - (10) + (12) + (14) + ih $$

Suppose that $\sigma_0 \not\le \sigma$ (hyp.6):

$$ - \sigma'_0 \not\le \sigma \quad (16) - \text{hyp.6 + (6)} $$

$$ - \mu_1, \Gamma_1, \Sigma_1 \approx_{id, \sigma} \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \text{ and } \hat{\sigma}_{pc} \not\le \sigma \quad (17) - \text{hyp.6 + (9) + Invisible Scope All.} $$

$$ - \mu'_1, \Gamma'_1, \Sigma'_1 \approx_{id, \sigma} \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}' \text{ and } \hat{\sigma}'_{pc} \not\le \sigma \quad (18) - (11) + \text{Invisible Scope All.} $$

$$ - \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \approx_{id, \sigma} \mu_f, \Gamma_f, \Sigma_f \quad (19) - (10) + (17) + \text{Confinement} $$

$$ - \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}' \approx_{id, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (20) - (12) + (18) + \text{Confinement} $$

$$ - \mu_1, \Gamma_1, \Sigma_1 \approx_{id, \sigma} \mu_f, \Gamma_f, \Sigma_f \quad (21) - (17) + (19) + \text{Transtivity of } \approx_{id, \sigma} $$

$$ - \mu'_1, \Gamma'_1, \Sigma'_1 \approx_{id, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (22) - (18) + (20) + \text{Transtivity of } \approx_{id, \sigma} $$

$$ - \mu_f, \Gamma_f, \Sigma_f \approx_{\beta'', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (23) - (7) + (21) + (22) + \text{Lateral Transtivity of } \approx_{\beta, \sigma} $$

$$ - \hat{\sigma}_{pc} \le \sigma_f \text{ and } \hat{\sigma}'_{pc} \le \sigma'_f \quad (24) - (10) + (12) + \sigma_{pc}\text{-Conservation} $$

$$ - \sigma_f \not\le \sigma \text{ and } \sigma'_f \not\le \sigma \quad (25) - (17) + (18) + (24) $$

$$ - (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta''''} v'_f \wedge \sigma_f \sqcup \sigma'_f \le \sigma) \quad (26) - (25) $$

**[METHOD CALL]** Suppose that $e = e_0[e_1](e_2)$ (hyp.5). We conclude that:

$$ - r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, r_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad (1) - \text{hyp.2 + hyp.5} $$

$$ - r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_1, m_1, \Gamma_1, \Sigma_1, \sigma_1 \rangle \quad (2) - \text{hyp.2 + hyp.5} $$
$$-r, \sigma_{pc} \vdash \langle \mu_1, e_2, \Gamma_1, \Sigma_1 \rangle \Uparrow_{IF} \langle \mu_2, v_2, \Gamma_2, \Sigma_2, \sigma_2 \rangle \quad (3) - \text{hyp.2} + \text{hyp.5}$$

$$- r', \sigma_{pc} \vdash \langle \mu', e_0, \Gamma', \Sigma' \rangle \Uparrow_{IF} \langle \mu'_0, r'_0, \Gamma'_0, \Sigma'_0, \sigma'_0 \rangle \quad (4) - \text{hyp.3} + \text{hyp.5}$$

$$- r', \sigma_{pc} \vdash \langle \mu'_0, e_1, \Gamma'_0, \Sigma'_0 \rangle \Uparrow_{IF} \langle \mu'_1, m'_1, \Gamma'_1, \Sigma'_1, \sigma'_1 \rangle \quad (5) - \text{hyp.3} + \text{hyp.5}$$

$$- r', \sigma_{pc} \vdash \langle \mu'_1, e_2, \Gamma'_1, \Sigma'_1 \rangle \Uparrow_{IF} \langle \mu'_2, v'_2, \Gamma'_2, \Sigma'_2, \sigma'_2 \rangle \quad (6) - \text{hyp.3} + \text{hyp.5}$$

$$- \mu_0, \Gamma_0, \Sigma_0 \approx_{\beta_0, \sigma} \mu'_0, \Gamma'_0, \Sigma'_0, \text{ for some } \beta_0 \text{ extending } \beta \quad (7) - \text{hyp.1} + (1) + (4) + \text{ih}$$

$$-(\sigma_0 \le \sigma \lor \sigma'_0 \le \sigma) \Rightarrow (r_0 \sim_{\beta_0} r'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma) \quad (8) - \text{hyp.1} + (1) + (4) + \text{ih}$$

$$- \mu_1, \Gamma_1, \Sigma_1 \approx_{\beta_1, \sigma} \mu'_1, \Gamma'_1, \Sigma'_1, \text{ for some } \beta_1 \text{ extending } \beta' \quad (9) - (2) + (5) + (7) + \text{ih}$$

$$-(\sigma_1 \le \sigma \lor \sigma'_1 \le \sigma) \Rightarrow (m_1 = m'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma) \quad (10) - (2) + (5) + (7) + \text{ih}$$

$$- \mu_2, \Gamma_2, \Sigma_2 \approx_{\beta_2, \sigma} \mu'_2, \Gamma'_2, \Sigma'_2, \text{ for some } \beta_2 \text{ extending } \beta' \quad (11) - (3) + (6) + (9) + \text{ih}$$

$$-(\sigma_2 \le \sigma \lor \sigma'_2 \le \sigma) \Rightarrow (v_2 \sim_{\beta_2} v'_2 \land \sigma_2 \sqcup \sigma'_2 \le \sigma) \quad (12) - (3) + (6) + (9) + \text{ih}$$

$$- \langle \mu_2, r_0, m_1, \Gamma_2, \Sigma_2 \rangle \mathcal{R}_{Proto} \langle r_m, \sigma_m \rangle \text{ and } r_f = \mu_2(r_m)(m_1) \quad (13) - \text{hyp.2} + \text{hyp.5}$$

$$- \langle \mu'_2, r'_0, m'_1, \Gamma'_2, \Sigma'_2 \rangle \mathcal{R}_{Proto} \langle r'_m, \sigma'_m \rangle \text{ and } r'_f = \mu'_2(r'_m)(m'_1) \quad (14) - \text{hyp.3} + \text{hyp.5}$$

$$- \langle \mu_2, \Gamma_2, \Sigma_2, r_f, v_2, r_0, \sigma_0 \sqcup \sigma_1 \sqcup \Gamma_2(r_m)(m_1) \sqcup \sigma_m, \sigma_2 \rangle \mathcal{R}_{NewScope} \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma}, \hat{r}, \hat{\sigma}_{pc} \rangle \quad (15) - \text{hyp.2} + \text{hyp.5}$$

$$- \hat{r}, \hat{\sigma}_{pc} \vdash \langle \hat{\mu}, \hat{e}, \hat{\Gamma}, \hat{\Sigma} \rangle \Uparrow_{IF} \langle \mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f \rangle \quad (16) - \text{hyp.2} + \text{hyp.5}$$

$$- \langle \mu'_2, \Gamma'_2, \Sigma'_2, r'_f, v'_2, r'_0, \sigma'_0 \sqcup \sigma'_1 \sqcup \Gamma'_2(r'_m)(m'_1) \sqcup \sigma'_m, \sigma'_2 \rangle \mathcal{R}_{NewScope} \langle \hat{\mu}', \hat{e}', \hat{\Gamma}', \hat{\Sigma}', \hat{r}', \hat{\sigma}'_{pc} \rangle \quad (17) - \text{hyp.3} + \text{hyp.5}$$

$$- \hat{r}', \hat{\sigma}'_{pc} \vdash \langle \hat{\mu}', \hat{e}', \hat{\Gamma}', \hat{\Sigma}' \rangle \Uparrow_{IF} \langle \mu'_f, v'_f, \Gamma'_f, \Sigma'_f, \sigma'_f \rangle \quad (18) - \text{hyp.3} + \text{hyp.5}$$

We consider two distinct cases: $\sigma_0 \sqcup \sigma_1 \sqcup \Gamma_2(r_m)(m_1) \sqcup \sigma_m \le \sigma$ and $\sigma_0 \sqcup \sigma_1 \sqcup \Gamma_2(r_m)(m_1) \sqcup \sigma_m \not\le \sigma$. Suppose that $\sigma_0 \sqcup \sigma_1 \sqcup \Gamma_2(r_m)(m_1) \sqcup \sigma_m \le \sigma$ (hyp.6):

$$- r_0 \sim_{\beta_0} r'_0 \land \sigma_0 \sqcup \sigma'_0 \le \sigma \quad (19) - \text{hyp.6} + (8)$$

$$- m_1 = m'_1 \land \sigma_1 \sqcup \sigma'_1 \le \sigma \quad (20) - \text{hyp.6} + (10)$$

$$- r_m \sim_{\beta_2} r'_m \land \sigma_m \sqcup \sigma'_m \le \sigma \quad (21) - \text{hyp.6} + (11) + (13) + (14) + (19) + (20) + \text{ih}$$

$$- r_f \sim_{\beta_2} r'_f \land \Gamma_2(r_m)(m_1) \sqcup \Gamma'_2(r'_m)(m_1) \le \sigma \quad (22) - \text{hyp.6} + (11) + (13) + (14) + (21)$$

$$- \hat{\sigma}'_{pc} = \hat{\sigma}_{pc} \le \sigma \quad (23) - \text{hyp.6} + (19) - (22)$$

$$- \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \approx_{\hat{\beta}, \sigma} \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}' \text{ and } \hat{e} = \hat{e}' \text{ for some } \hat{\beta} \text{ extending } \beta_2 \quad (24) - (11) + (12) + (15) + (17) + (19) + (22) + (23) + \text{Visible Scope All.}$$

$$- \mu_f, \Gamma_f, \Sigma_f \approx_{\beta'''', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \text{ and } (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta''''} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma) \quad (25) - (16) + (18) + (24) + \text{ih}$$

Suppose that $\sigma_0 \sqcup \sigma_1 \sqcup \Gamma_2(r_m)(m_1) \sqcup \sigma_m \not\le \sigma$ (hyp.6):

$$- \sigma'_0 \sqcup \sigma'_1 \sqcup \Gamma'_2(r'_m)(m'_1) \sqcup \sigma'_m \not\le \sigma \quad (26) - \textit{Multiple steps}$$

$$- \hat{\sigma}_{pc} \le \sigma \text{ and } \hat{\sigma}'_{pc} \le \sigma \quad (27) - \text{hyp.6} + (26)$$

$$- \mu_2, \Gamma_2, \Sigma_2 \approx_{id, \sigma} \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \quad (28) - (15) + (27) + \text{Invisible Scope All.}$$

$$- \mu'_2, \Gamma'_2, \Sigma'_2 \approx_{id, \sigma} \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}' \quad (29) - (17) + (27) + \text{Invisible Scope All.}$$

$$- \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \approx_{id, \sigma} \mu_f, \Gamma_f, \Sigma_f \quad (30) - (16) + (27) + \text{Confinement}$$

$$- \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}' \approx_{id, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (31) - (18) + (27) + \text{Confinement}$$

$$- \mu_2, \Gamma_2, \Sigma_2 \approx_{id, \sigma} \mu_f, \Gamma_f, \Sigma_f \quad (32) - (28) + (30) + \text{Transtivity of } \approx_{id, \sigma}$$

$$- \mu'_2, \Gamma'_2, \Sigma'_2 \approx_{id, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (33) - (29) + (31) + \text{Transtivity of } \approx_{id, \sigma}$$

$$- \mu_f, \Gamma_f, \Sigma_f \approx_{\beta'', \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (34) - (11) + (32) + (33) + \text{Lateral Transtivity of } \approx_{\beta, \sigma}$$

$$- \hat{\sigma}_{pc} \le \sigma_f \text{ and } \hat{\sigma}'_{pc} \le \sigma'_f \quad (35) - (16) + (18) + \sigma_{pc}\text{-Conservation}$$

$$- \sigma_f \not\le \sigma \text{ and } \sigma'_f \not\le \sigma \quad (36) - (27) + (35)$$

$$- (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta''''} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma) \quad (37) - (36)$$

[SEQUENCE] Suppose that $e = e_0, e_1$ (hyp.5). We conclude that:
$$-r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle \quad (1) - \text{hyp.2} + \text{hyp.5}$$

$$-r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f \rangle \quad (2) - \text{hyp.2} + \text{hyp.5}$$

$$-r', \sigma_{pc} \vdash \langle \mu', e_0, \Gamma', \Sigma' \rangle \Downarrow_{IF} \langle \mu'_0, v'_0, \Gamma'_0, \Sigma'_0, \sigma'_0 \rangle \quad (3) - \text{hyp.3} + \text{hyp.5}$$

$$-r', \sigma_{pc} \vdash \langle \mu'_0, e_1, \Gamma'_0, \Sigma'_0 \rangle \Downarrow_{IF} \langle \mu'_f, v'_f, \Gamma'_f, \Sigma'_f, \sigma'_f \rangle \quad (4) - \text{hyp.3} + \text{hyp.5}$$

$$- \mu_0, \Gamma_0, \Sigma_0 \approx_{\beta_0, \sigma} \mu'_0, \Gamma'_0, \Sigma'_0, \text{ for some } \beta_0 \text{ extending } \beta \quad (5) - \text{hyp.1} + (1) + (3) + \mathbf{ih}$$

$$- \mu_f, \Gamma_f, \Sigma_f \approx_{\beta_f, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f, \text{ for some } \beta_f \text{ extending } \beta_0 \text{ and } (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta_f} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma) \quad (6) - (2) + (4) + (5) + \mathbf{ih}$$

[CONDITIONAL] Suppose that $e = \hat{e} ?$ ($e_0$) : ($e_1$) (hyp.5). We conclude that:

$$-r, \sigma_{pc} \vdash \langle \mu, \hat{e}, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \hat{\mu}, \hat{v}, \hat{\Gamma}, \hat{\Sigma}, \hat{\sigma} \rangle \quad (1) - \text{hyp.2} + \text{hyp.5}$$

$$-r, \sigma_{pc} \sqcup \hat{\sigma} \vdash \langle \hat{\mu}, e_i, \hat{\Gamma}, \hat{\Sigma} \rangle \Downarrow_{IF} \langle \mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f \rangle \quad (2) - \text{hyp.2} + \text{hyp.5}$$

$$- \hat{v} \notin V_f \Rightarrow i = 0 \land \hat{v} \notin V_f \Rightarrow i = 1 \quad (3) - \text{hyp.2} + \text{hyp.5}$$

$$-r', \sigma_{pc} \vdash \langle \mu', \hat{e}, \Gamma', \Sigma' \rangle \Downarrow_{IF} \langle \hat{\mu}', \hat{v}', \hat{\Gamma}', \hat{\Sigma}', \hat{\sigma}' \rangle \quad (4) - \text{hyp.3} + \text{hyp.5}$$

$$-r', \sigma_{pc} \sqcup \hat{\sigma}' \vdash \langle \hat{\mu}', e_j, \hat{\Gamma}', \hat{\Sigma}' \rangle \Downarrow_{IF} \langle \mu'_f, v'_f, \Gamma'_f, \Sigma'_f, \sigma'_f \rangle \quad (5) - \text{hyp.3} + \text{hyp.5}$$

$$- \hat{v}' \notin V_f \Rightarrow j = 0 \land \hat{v}' \notin V_f \Rightarrow j = 1 \quad (6) - \text{hyp.3} + \text{hyp.5}$$

$$- \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \approx_{\hat{\beta}, \sigma} \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}' \text{ for some } \hat{\beta} \text{ extending } \beta \text{ and } (\hat{\sigma} \le \sigma \lor \hat{\sigma}' \le \sigma) \Rightarrow (\hat{v} \sim_{\hat{\beta}} \hat{v}' \land \hat{\sigma} \sqcup \hat{\sigma}' \le \sigma) \quad (7) - \text{hyp.1} + (1) + (4) + \mathbf{ih}$$

Without loss of generality, we assume $i = 0$ (hyp.6) (the case $i = 1$ is symmetric). We proceed by case analysis. Suppose that $\hat{\sigma} \le \sigma$ (hyp.7). We conclude:

$$- \hat{\mu} \sim_{\hat{\beta}} \hat{v}' \land \hat{\sigma} \sqcup \hat{\sigma}' \le \sigma \quad (8) - \text{hyp.7} + (7)$$

$$- j = 0 \quad (9) - \text{hyp.6} + (8)$$

$$- \mu_f, \Gamma_f, \Sigma_f \approx_{\beta_f, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \text{ for some } \beta_f \text{ extending } \beta \text{ and } (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta_f} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma) \quad (10) - \text{hyp.6} + (2) + (4) + (7) + (9) + \mathbf{ih}$$

Suppose that $\hat{\sigma} \le \sigma$ (hyp.7). We conclude:

$$- \hat{\sigma}' \le \sigma \quad (11) - \text{hyp.7} + (7)$$

$$- \hat{\mu}, \hat{\Gamma}, \hat{\Sigma} \approx_{id, \sigma} \mu_f, \Gamma_f, \Sigma_f \quad (12) - \text{hyp.7} + (2) + \text{Confinement}$$

$$- \hat{\mu}', \hat{\Gamma}', \hat{\Sigma}' \approx_{id, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (13) - (5) + (11) + \text{Confinement}$$

$$- \mu_f, \Gamma_f, \Sigma_f \approx_{\beta, \sigma} \mu'_f, \Gamma'_f, \Sigma'_f \quad (14) - (7) + (12) + (13) + \text{Lateral Transitivity of } \approx_{\beta, \sigma}$$

$$- \hat{\sigma} \le \sigma_f \text{ and } \hat{\sigma}' \le \sigma'_f \quad (15) - (2) + (5) + \sigma_{pc}\text{-Conservation}$$

$$- \sigma_f \le \sigma \text{ and } \sigma'_f \le \sigma \quad (16) - \text{hyp.7} + (11) + (15)$$

$$- (\sigma_f \le \sigma \lor \sigma'_f \le \sigma) \Rightarrow (v_f \sim_{\beta} v'_f \land \sigma_f \sqcup \sigma'_f \le \sigma) \quad (17) - (16)$$

## B Proofs of Section 3

**Lemma 17 (Scope-Chain Indistinguishability).** Given a function $\beta$, two memories $\mu$ and $\mu'$, and a labeling $\langle \Gamma, \Sigma \rangle$ s.t. $\langle \mu, \Gamma, \Sigma \rangle S_\beta \mu'$. Then, for any reference $r \in \text{dom}(\beta)$ and identifier $x$, $\langle \mu, r, x \rangle \mathcal{R}_{Scope} r_x$ iff $\langle \mu', \beta(r), x \rangle \mathcal{R}_{Scope} \beta(r_x)$.

**Lemma 18 (Prototype-Chain Indistinguishability).** Given a function $\beta$, two memories $\mu$ and $\mu'$, and a labeling $\langle \Gamma, \Sigma \rangle$ s.t. $\langle \mu, \Gamma, \Sigma \rangle S_\beta \mu'$. Then, for any two references $r, r' \in \text{dom}(\beta)$, property $p$, and security level $\sigma$, $\langle \mu, r, p, \Gamma, \Sigma \rangle \mathcal{R}_{proto} \langle r', \sigma \rangle$ iff $\langle \mu', \beta(r), p \rangle \mathcal{R}_{proto} \beta(r')$.
**Lemma 19 (Correctness).** Provided that $e$ does not use identifiers in $\mathcal{I}_C$, for any labeled and instrumented configurations $\langle\mu, e, \Gamma, \Sigma\rangle$ and $\langle\mu', e'\rangle$, function $\beta$, and reference $r$ in $\mu$, such that $\langle\mu, \Gamma, \Sigma\rangle S_\beta \mu'$, $C\langle e\rangle = \langle e', i\rangle$, and $\sigma_{pc} = \mu'(\beta(r))($pc), for some index $i$; there exists $\langle\mu_f, v_f, \Gamma_f, \sigma\rangle$ such that $r, \sigma_{pc} \vdash \langle\mu, e, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f\rangle$ iff there exists $\langle\mu'_f, v'_f\rangle$ such that $\beta(r) \vdash \langle\langle\mu', e'\rangle\rangle \Downarrow \langle\langle\mu'_f, v'_f\rangle\rangle$, in which case the following statements hold: (1) $\langle\mu_f, \Gamma_f, \Sigma_f\rangle S_{\beta'} \mu'_f$, (2) $v_f \sim_{C(\beta)} v'_f$, (3) $v'_f = \mu'_f(\beta(r))($\hat{v}_i)$, (4) $\sigma_f = \mu'_f(\beta(r))($\hat{l}_i)$, and (5) $\sigma_{pc} = \mu'_f(\beta(r))($pc).

*Proof.* In order to prove the claim, we have to prove both sides of the equivalence. Since the proof is analogous, we choose to prove the right-to-left implication, which immediately implies security. Hence, assuming that: $\beta(r) \vdash \langle\langle\mu', e'\rangle\rangle \Downarrow \langle\langle\mu'_f, v'_f\rangle\rangle$ (hyp.1), $\langle\mu, \Gamma, \Sigma\rangle S_\beta \mu'$ (hyp.2), $C\langle e\rangle = \langle e', i\rangle$ (hyp.3), and $\sigma_{pc} = \mu'(\beta(r))($pc) (hyp.4), we need to show that: $r, \sigma_{pc} \vdash \langle\mu, e, \Gamma, \Sigma\rangle \Downarrow_{IF} \langle\mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f\rangle$, $\langle\mu_f, \Gamma_f, \Sigma_f\rangle S_{\beta'} \mu'_f$, $v_f \sim_{C(\beta)} v'_f$, $v'_f = \mu'_f(\beta(r))($\hat{v}_i)$, $\sigma_f = \mu'_f(\beta(r))($\hat{l}_i)$, and $\sigma_{pc} = \mu'_f(\beta(r))($pc). The proof proceeds by induction on the derivation of hyp.1. In the following let $r' = \beta(r)$.

[VALUE] Suppose that $e = v^i$ (hyp.5). We conclude that:

$$- e' = \hat{l}_i = \$pc, \ \$v_i = v \qquad (1) \text{ - hyp.3 + hyp.5}$$

$$- \mu_f = \mu, \Gamma_f = \Gamma, \Sigma_f = \Sigma, v_f = v, \text{ and } \sigma_f = \sigma_{pc} \qquad (2) \text{ - hyp.5}$$

$$- \mu'_f = \mu' [r' \mapsto \mu'(r') [\hat{v}_i \mapsto v, \hat{l}_i \mapsto \sigma_{pc}]], v'_f = v \qquad (3) \text{ - hyp.1 + hyp.5}$$

$$- \langle\mu_f, \Gamma_f, \Sigma_f\rangle S_\beta \mu'_f, v_f \sim_{C(\beta)} v'_f, v'_f = \mu'_f(\beta(r))($\hat{v}_i$), \text{ and } \sigma_f = \mu'_f(\beta(r))($\hat{l}_i$). \qquad (4) \text{ - hyp.2 + hyp.4 + (2) + (3)}$$

$$- \sigma_{pc} = \mu'_f(r')($pc) \qquad (5) \text{ - hyp.4 + (3)}$$

[THIS] Suppose that $e = \text{this}^i$ (hyp.5). We conclude that:

$$- e' = \hat{l}_i = \$pc, \ \$v_i = \text{this} \qquad (1) \text{ - hyp.3 + hyp.5}$$

$$- \mu_f = \mu, \Gamma_f = \Gamma, \Sigma_f = \Sigma, v_f = \mu(r)(@this), \text{ and } \sigma_f = \Gamma(r)(@this) \sqcup \sigma_{pc} \qquad (2) \text{ - hyp.5}$$

$$- \mu'_f = \mu' [r' \mapsto \mu'(r') [\hat{v}_i \mapsto v'_f, \hat{l}_i \mapsto \sigma_{pc}]], v'_f = \mu(r)(@this) \qquad (3) \text{ - hyp.1 + hyp.5}$$

$$- \langle\mu_f, \Gamma_f, \Sigma_f\rangle S_\beta \mu'_f, v_f \sim_{C(\beta)} v'_f, \text{ and } v'_f = \mu'_f(\beta(r))($\hat{v}_i$) \qquad (4) \text{ - hyp.2 + (2) + (3)}$$

$$- \Gamma(r)(@this) \leq \sigma_{pc} \qquad (5) \text{ - this-Invariant}$$

$$- \sigma_f = \mu'_f(\beta(r))($\hat{l}_i) \qquad (6) \text{ - hyp.4 + (2) + (3)}$$

$$- \sigma_{pc} = \mu'_f(r')($pc) \qquad (7) \text{ - hyp.4 + (3)}$$

[VARIABLE] Suppose that $e = x^i$ (hyp.5). We conclude that:

$$- e' = \hat{l}_i = \$pc \sqcup \$l_x, \ \$v_i = x \qquad (1) \text{ - hyp.3 + hyp.5}$$

$$- \langle\mu', r', x\rangle \mathcal{R}_{Scope} r'_x, r'_x \neq \text{null}, v'_f = \mu'(r'_x)(x) \qquad (2) \text{ - hyp.1 + hyp.5}$$

$$- \langle\mu', r', \$l_x\rangle \mathcal{R}_{Scope} r'_x, \sigma'_f = \mu'(r'_x)(\$l_x) \sqcup \sigma_{pc} \qquad (3) \text{ - hyp.1 + hyp.5}$$

$$- \mu'_f = \mu' [r' \mapsto \mu'(r') [\hat{v}_i \mapsto v'_f, \hat{l}_i \mapsto \sigma'_f]] \qquad (4) \text{ - hyp.1 + hyp.5}$$

$$- \langle\mu, r, x\rangle \mathcal{R}_{Scope} r_x, r_x \neq \text{null}, \text{ and } r_x \sim_{C(\beta)} r'_x \qquad (5) \text{ - hyp.2 + (2) + Scope Indistinguishability}$$

$$- \mu_f = \mu, \Gamma_f = \Gamma, \Sigma_f = \Sigma, v_f = \mu(r_x)(x), \sigma_f = \Gamma(r_x)(x) \sqcup \sigma_{pc} \qquad (6) \text{ - hyp.5 + (5)}$$
- $v_f \sim_{C(\beta)} v'_f$ and $\sigma_f = \sigma'_f$ (7) - hyp.2 + (2) + (3) + (5) + (6)

- $\langle \mu_f, \Gamma_f, \Sigma_f \rangle S_\beta \mu'_f$, (8) - hyp.2 + (4) + (6)

- $v_f \sim_{C(\beta)} v'_f$, $v'_f = \mu'_f(r')($$\hat{v}_i)$$, and $\sigma_f = \mu'_f(r')($$\hat{l}_i)$ (9) - hyp.2 + (4) + (6) + (7)

- $\sigma_{pc} = \mu'_f(r')($$pc)$ (10) - hyp.4 + (4)

[BINARY OPERATION] Suppose that $e_0 \text{ op}^i e_1$ (hyp.5). We conclude that:

- $e' = e'_0, e'_1, \$\hat{l}_i = \$\hat{l}_j \sqcup \$\hat{l}_k, \$\hat{v}_i = \$\hat{v}_j \text{ op } \$\hat{v}_k$, where: $C\langle e_0 \rangle = \langle e'_0, j \rangle$ and $C\langle e_1 \rangle = \langle e'_1, k \rangle$ (1) - hyp.3 + hyp.5

- $r' \vdash (\langle \mu', e'_0 \rangle) \vdash (\langle \mu'_0, v'_0 \rangle)$ and $r' \vdash (\langle \mu'_1, e'_1 \rangle) \vdash (\langle \mu'_1, v'_1 \rangle)$ (2) - hyp.1 + hyp.3 + hyp.5 + (1)

- $r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \downarrow_{\text{IF}} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle, \langle \mu_0, \Gamma_0, \Sigma_0 \rangle S_{\beta_0} \mu'_0, v_0 \sim_{C(\beta_0)} v'_0, v'_0 = \mu'_0(r')($$\hat{v}_j)$$, and $\sigma_0 = \mu'_0(r')($$\hat{l}_j)$$, and $\sigma_{pc} = \mu'_0(r')($$\hat{pc})$$$ (3) - hyp.2 + hyp.4 + (1) + (2) + \text{ih}

- $r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \downarrow_{\text{IF}} \langle \mu_f, v_1, \Gamma_f, \Sigma_f, \sigma_1 \rangle, \langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_1} \mu'_1, v_1 \sim_{C(\beta_0)} v'_1, v'_1 = \mu'_1(r')($$\hat{v}_k)$$, $\sigma_1 = \mu'_1(r')($$\hat{l}_k)$$, and $\sigma_{pc} = \mu'_1(r')($$\hat{pc})$$$ (4) - hyp.4 + (1)-(3) + \text{ih}

- $\sigma_f = \sigma_0 \sqcup \sigma_1, \sigma'_f = \mu'(r'_x)($$\hat{l}_x)$$ \sqcup \sigma_{pc}, v_f = v_0 \text{ op } v_1$, and $v'_f = v'_0 \text{ op } v'_1$ (5) - hyp.1 + hyp.3 + hyp.5 + (3) + (4)

- $\mu'_f = \mu' \left[ r' \mapsto \mu'(r') \left[ \$\hat{v}_i \mapsto v'_f, \$\hat{l}_i \mapsto \sigma'_f \right] \right]$ (6) - hyp.1 + hyp.5 + (5)

- $\langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_1} \mu'_f$ (7) - (4) + (6)

- $v_f \sim_{C(\beta_1)} v'_f$, $v'_f = \mu'_f(r')($$\hat{v}_i)$$, and $\sigma_f = \mu'_f(r')($$\hat{l}_i)$$$ (8) - hyp.2 + (4) + (6) + (7)

- $\sigma_{pc} = \mu'_f(r')($$pc)$ (9) - hyp.4 + (4)

[VARIABLE ASSIGNMENT] Suppose that $x = e_0$ (hyp.5). We conclude that:

- $e' = e'_0, \$check($pc \leq $l_x)$, \$l_x = \$\hat{l}_i$, $x = \$\hat{v}_i$, where: $x \notin \mathcal{I}_C$ and $C\langle e_0 \rangle = \langle e'_0, i \rangle$ (1) - hyp.3 + hyp.5

- $r' \vdash (\langle \mu', e'_0 \rangle) \vdash (\langle \mu'_0, v'_0 \rangle)$ (2) - hyp.1 + hyp.3 + hyp.5 + (1)

- $\langle \mu'_0, r', x \rangle \mathcal{R}_{\text{Scope}} r'_x, r'_x \neq \text{null}, \langle \mu', r', \$l_x \rangle \mathcal{R}_{\text{Scope}} r'_x$ (3) - hyp.1 + hyp.5

- $r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \downarrow_{\text{IF}} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle, \langle \mu_0, \Gamma_0, \Sigma_0 \rangle S_{\beta_0} \mu'_0, v_0 \sim_{C(\beta_0)} v'_0, v'_0 = \mu'_0(r')($$\hat{v}_i)$$, and $\sigma_0 = \mu'_0(r')($$\hat{l}_i)$$, and $\sigma_{pc} = \mu'_0(r')($$\hat{pc})$$$ (4) - hyp.2 + hyp.4 + (1) + (2) + \text{ih}

- $\sigma'_f = \sigma'_0, v'_f = v'_0, \mu'_0(r')($$\hat{pc})$$ \leq \mu'_0(r'_x)($$\hat{l}_x)$ (5) - hyp.1 + hyp.3 + hyp.4 + hyp.5

- $\mu'_f = \mu' \left[ r' \mapsto \mu'(r') \left[ \$\hat{v}_i \mapsto v'_f, \$\hat{l}_i \mapsto \sigma'_f \right], r'_x \mapsto \mu'(r'_x) \left[ x \mapsto v'_f, \$l_x \mapsto \sigma'_f \right] \right]$ (6) - hyp.1 + hyp.4 + hyp.5 + (4)

- $\langle \mu_0, r, x \rangle \mathcal{R}_{\text{Scope}} r_x, r_x \neq \text{null}$, and $r_x \sim_{C(\beta)} r'_x$ (7) - (4) + Scope Indistinguishability

- $\sigma_{pc} \leq \Gamma_0(r_x)(x)$ (8) - (4) + (5) + (7)

- $\Gamma_f = \Gamma_0 [r_x \mapsto \Gamma_0(r_x) [x \mapsto \sigma_0]]$, $\mu_f = \mu_0 [r_x \mapsto \mu_0(r_x) [x \mapsto v_0]]$, $v_f = v_0$, and $\sigma_f = \sigma_0$ (9) - hyp.5 + (4) + (8)

- $\langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_1} \mu'_f$ (10) - (4) + (6) + (9)

- $v_f \sim_{C(\beta_1)} v'_f$, $\sigma_f = \sigma'_f$, $v'_f = \mu'_f(r')($$\hat{v}_i)$$, and $\sigma_f = \mu'_f(r')($$\hat{l}_i)$$$ (11) - hyp.2 + (4) + (6) + (7)

- $\sigma_{pc} = \mu'_f(r')($$pc)$ (12) - hyp.4 + (4)
[SEQUENCE] Suppose that $e_0, e_1$ (hyp.5). We conclude that:

$$ - e' = e'_0, e'_1 \text{ where: } C\langle e_0 \rangle = \langle e'_0, j \rangle \text{ and } C\langle e_1 \rangle = \langle e'_1, k \rangle \quad (1) - \text{hyp.3} + \text{hyp.5} $$

$$ - r' \vdash \langle\langle\mu', e'_0\rangle\rangle \Downarrow \langle\langle\mu'_0, v'_0\rangle\rangle \text{ and } r' \vdash \langle\langle\mu'_0, e'_1\rangle\rangle \Downarrow \langle\langle\mu'_f, v'_f\rangle\rangle \quad (2) - \text{hyp.1} + \text{hyp.3} + \text{hyp.5} + (1) $$

$$ - r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle, \langle \mu_0, \Gamma_0, \Sigma_0 \rangle S_{\beta_0} \mu'_0, v_0 \sim_{C(\beta_0)} v'_0, \\ v'_0 = \mu'_0(r') (\hat{v}_j), \sigma_0 = \mu'_0(r') (\hat{l}_j), \text{ and } \sigma_{pc} = \mu'_0(r') (\hat{pc}) \quad (3) - \text{hyp.2} + \text{hyp.4} + (1) + (2) + \text{ih} $$

$$ - r, \sigma_{pc} \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f \rangle, \langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_f} \mu'_1, v_f \sim_{C(\beta_f)} v'_f, \\ v'_f = \mu'_f(r') (\hat{v}_k), \sigma_f = \mu'_f(r') (\hat{l}_k), \text{ and } \sigma_{pc} = \mu'_f(r') (\hat{pc}) \quad (4) - \text{hyp.4} + (1) - (3) + \text{ih} $$

[CONDITIONAL] Suppose that $e = e_0$ ?$s,t$ ($e_1$) : ($e_2$) (hyp.5). We conclude that:

$$ - e' = e'_0, \hat{l}_s = \hat{pc}, \hat{pc} = \hat{pc} \sqcup \hat{l}_i, e_{cond}, \hat{pc} = \hat{l}_s, \hat{v}_t \text{ where: } C\langle e_0 \rangle = \langle e'_0, i \rangle \text{ and } C\langle e_1 \rangle = \langle e'_1, j \rangle, C\langle e_2 \rangle = \langle e'_2, k \rangle, e_{cond} = \hat{v}_i ? \quad (e'_1, \hat{v}_t = \hat{v}_j, \hat{l}_t = \hat{l}_j) : \\ (e'_2, \hat{v}_t = \hat{v}_k, \hat{l}_t = \hat{l}_k) \quad (1) - \text{hyp.3} + \text{hyp.5} $$

$$ - r' \vdash \langle\langle\mu', e'_0\rangle\rangle \Downarrow \langle\langle\mu'_0, v'_0\rangle\rangle \quad (2) - \text{hyp.1} + \text{hyp.3} + \text{hyp.5} $$

$$ - r, \sigma_{pc} \vdash \langle \mu, e_0, \Gamma, \Sigma \rangle \Downarrow_{IF} \langle \mu_0, v_0, \Gamma_0, \Sigma_0, \sigma_0 \rangle, \langle \mu_0, \Gamma_0, \Sigma_0 \rangle S_{\beta_0} \mu'_0, v_0 \sim_{C(\beta_0)} v'_0, \\ v'_0 = \mu'_0(r') (\hat{v}_i), \sigma_0 = \mu'_0(r') (\hat{l}_i), \text{ and } \sigma_{pc} = \mu'_0(r') (\hat{pc}) \quad (3) - \text{hyp.2} + \text{hyp.4} + (1) + (2) + \text{ih} $$

We assume without loss of generality that $v'_0 \notin V_f$ (hyp.6). It follows that:

$$ - \mu_0'' = \mu_0' [r' \mapsto \mu_0'(r') [\hat{v}_s \mapsto \sigma_{pc}, \hat{pc} \mapsto \sigma_{pc} \sqcup \sigma_0]] \quad (4) - \text{hyp.1} + \text{hyp.3} + \text{hyp.4} + (1) + (3) $$

$$ - r' \vdash \langle\langle\mu_0'', e'_1\rangle\rangle \Downarrow \langle\langle\mu'_1, v'_f\rangle\rangle \quad (5) - \text{hyp.1} + \text{hyp.3} + \text{hyp.4} + (1) + (3) $$

$$ - v_0 \notin V_f \quad (6) - \text{hyp.6} + (3) $$

$$ - \langle \mu_0, \Gamma_0, \Sigma_0 \rangle S_{\beta_f} \mu'_1 \quad (7) - (3) + (4) + \textit{Preservation of Memory Similarity} $$

$$ - r, \sigma_{pc} \sqcup \sigma_0 \vdash \langle \mu_0, e_1, \Gamma_0, \Sigma_0 \rangle \Downarrow_{IF} \langle \mu_f, v_f, \Gamma_f, \Sigma_f, \sigma_f \rangle, \langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_f} \mu'_1, v_f \sim_{C(\beta_f)} v'_f, \\ v'_f = \mu_0''(r') (\hat{v}_j), \text{ and } \sigma_f = \mu_1'(r') (\hat{l}_j) \quad (8) - \text{hyp.4} + \text{hyp.5} + (5) + (7) + \text{ih} \\ - \mu'_f = \mu'_1 [r' \mapsto \mu_1'(r') [\hat{v}_t \mapsto v'_f, \hat{l}_t \mapsto \sigma_f, \hat{pc} \mapsto \sigma_{pc}]] \quad (9) - \text{hyp.5} + (1) $$

$$ - \langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_f} \mu'_f \quad (10) - (7) + (9) + \textit{Preservation of Memory Similarity} $$

[OBJECT LITERAL] Suppose that $e = \{\}^i$ (hyp.5). We conclude that:

$$ - e' = \hat{v}_i = \{\}, \hat{v}_i, \$struct = \hat{pc}, \hat{v}_i, \$l_{proto} = \hat{pc}, \hat{l}_i = \hat{pc}, \hat{v}_i \quad (1) - \text{hyp.3} + \text{hyp.5} $$

$$ - \mu_f = \mu [r_o \mapsto [-prot_- \mapsto null]], \Gamma_f = \Gamma [r_o \mapsto [-prot_- \mapsto \sigma_{pc}]], \Sigma' = \Sigma [r_o \mapsto \sigma_{pc}], \\ r_o \notin \text{dom}(\mu), v_f = r_o, \text{ and } \sigma_f = \sigma_{pc} \quad (2) - \text{hyp.5} $$

$$ - \mu'_f = \mu' [r'_o \mapsto [-prot_- \mapsto null, \$l_{proto} \mapsto \sigma_{pc}, \$struct \mapsto \sigma_{pc}], r' \mapsto [\hat{v}_i \mapsto r'_o, \hat{l}_i \mapsto \sigma_{pc}]] \\ r'_o \notin \text{dom}(\mu'), v'_f = r'_o \quad (3) - \text{hyp.5} $$

$$ - \sigma_{pc} = \mu'_f(r') (\hat{pc}) \quad (4) - \text{hyp.4} + (3) $$

Making $\beta_o = \beta [r_o \mapsto r'_o]$ (hyp.6). We conclude that:

$$ - \langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_o} \mu'_f, v_f \sim_{C(\beta_o)} v'_f, v'_f = \mu'_f(\beta(r)) (\hat{v}_i), \text{ and } \sigma_f = \mu'_f(\beta(r)) (\hat{l}_i). \quad (5) - \text{hyp.2} + \text{hyp.4} + \text{hyp.6} + (2) + (3) $$
[FUNCTION LITERAL] Suppose that $e = \mathbf{function}^i(x)\{\mathbf{var} \ y_1, \dots, y_n; \ \hat{e}\} \text{ (hyp.5).}$
We conclude that:

$$
- e' = \hat{v}_i = \emptyset, \quad \hat{v}_i \cdot \mathit{struct} = \mathit{pc}, \quad \hat{v}_i \cdot \mathit{l}_{\mathit{proto}} = \mathit{pc}, \quad \hat{l}_i = \mathit{pc}, \quad \hat{v}_i \tag{1} \text{- hyp.3 + hyp.5}
$$

$$
- \mu_f = \mu[r_f \mapsto [\mathit{@fscope} \mapsto r, \mathit{@code} \mapsto \lambda x. \{\mathbf{var} \ y_1, \dots, y_n; \ \hat{e}\}\}], \\
\Gamma_f = \Gamma[r_f \mapsto [\mathit{@fscope} \mapsto \sigma_{pc}, \mathit{@code} \mapsto \sigma_{pc}]], \Sigma_f = \Sigma[r_o \mapsto \sigma_{pc}], \\
r_f \notin \mathrm{dom}(\mu), \quad v_f = r_f, \quad \text{and} \quad \sigma_f = \sigma_{pc} \tag{2} \text{- hyp.5}
$$

$$
- \mu'_{f} = \mu' \left[ \begin{array}{l} r'_{f} \mapsto [\mathcal{S}struct \mapsto \sigma_{pc}, \mathcal{A}fscope \mapsto r, \mathcal{A}code \mapsto \lambda x. \{\mathbf{var} \ y_1, \dots, y_n; \ \hat{e}\}] \\ r'_{f} \mapsto [\mathcal{S}\hat{v}_i \mapsto r'_{f}, \mathcal{S}\hat{l}_i \mapsto \sigma_{pc}] \end{array} \right], r'_{f} \notin \mathrm{dom}(\mu'), \\
v'_{f} = r'_{o} \tag{3} \text{- hyp.5}
$$

$$
- \sigma_{pc} = \mu'_{f}(r') (\$pc) \tag{4} - \text{hyp.4} + (3)
$$

Making $\beta_f = \beta[r_f \mapsto r_f']$ (hyp.6). We conclude that:

$$
- \langle \mu_f, \Gamma_f, \Sigma_f \rangle S_{\beta_o} \mu'_f, v_f \sim_{C(\beta_o)} v'_f, v'_f = \mu'_f(\beta(r))(\hat{v}_i), \text{ and } \sigma_f = \mu'_f(\beta(r))(\hat{l}_i). \tag{5} \text{- hyp.2 + hyp.4 + hyp.6 + (2) + (3)}
$$

The remaining cases are handled analogously.