2.1 Variables and Mutation

The core of Oxide is an imperative calculus with constants and variables. The abstract syntax for these features is below:

Constants are Oxide's atomic values and also the base-case for information flow. A constant's dependency is simply itself, expressed through the T-u32 rule:

Variables and mutation are introduced through let-bindings and assignment expressions, respectively. For example, this (location-annotated) program mutates a field of a tuple:

Here, $t$ is a variable and $t.1$ is a place, or a description of a specific region in memory. For information flow, the key idea is that let-bindings introduce a set of places into $\Theta$, and then assignment expressions change a place's dependencies within $\Theta$. In the above example, after binding $t$, then $\Theta$ is:

After checking "$t.1:=3$", then ${\ell }_3$ is added to $\Theta (t)$ and $\Theta (t.1)$, but not $\Theta (t.0)$. This is because the values of $t$ and $t.1$ have changed, but the value of $t.0$ has not. Formally, the let-binding rule is:

Again, this rule (and many others) contain aspects of Oxide that are not essential for understanding information flow such as the subtyping judgment ${{\tau }^{\text{SI}}}_1\lesssim {{\tau }^{\text{SI}}}_a$ or the metafunction $\mathsf{gc}\text{-}\mathsf{loans}$. For brevity we will not cover these aspects here, and instead refer the interested reader to $\text{Weiss et al. [2019]}$. We have deemphasized (in grey) the judgments which are not important to understanding our information flow additions.

The key concept is the formula ${\Theta }_1[\forall {\pi }^{\square }[x].\pi \mapsto {\kappa }_1]$. This introduces two shorthands: first, ${\pi }^{\square }[x]$ means "a place $\pi$ with root variable $x$ in a context ${\pi }^{\square }$", used to decompose a place. In T-let, the update to ${\Theta }_1$ happens for all places with a root variable $x$. Second, ${\Theta }_1[\pi \mapsto {\kappa }_1]$ means "set $\pi$ to ${\kappa }_1$ in ${\Theta }_1$". So this rule specifies that when checking $e_2$, all places within $x$ are initialized to the dependencies ${\Theta }_1$ of $e_1$.

Next, the assignment expression rule is defined as updating all the conflicts of a place $\pi$:

If you conceptualize a type as a tree and a path as a node in that tree, then a node's conflicts are its ancestors and descendants (but not siblings). Semantically, conflicts are the set of places whose value change if a given place is mutated. Recall from the previous example that $t.1$ conflicts with $t$ and $t.1$, but not $t.0$. Formally, we say two places are disjoint ($\#$) or conflict ($\sqcap$) when:

Then to update a place's conflicts in $\Theta$, we define the metafunction $\mathsf{update}\text{-}\mathsf{conflicts}$ to add $\kappa$ to all conflicting places $p^{\prime }$. (Note that this rule is actually defined over place expressions $p$, which are explained in the next subsection.)

Finally, the rule for reading places is simply to look up the place's dependencies in $\Theta$:

2.2 References

Beyond concrete places in memory, Oxide also contains references that point to places. As in Rust, these references have both a lifetime (called a "provenance") and a mutability qualifier (called an "ownership qualifier"). Their syntax is:

Provenances are created via a $\mathsf{letprov}$ expression, and references are created via a borrow expression $\&r\omega p$ that has an initial concrete provenance $r$ (abstract provenances are just used for types of function parameters). References are used in conjunction with place expressions $p$ that are places whose paths contain dereferences. For example, this program creates, reborrows, and mutates a reference:

Consider the information flow induced by $\ast z:=1_{\ell }$. We need to compute all places that $z$ could point-to, in this case $x.1$, so $\ell$ can be added to the conflicts of $x.1$. Essentially, we must perform a pointer analysis [$\text{Smaragdakis and Balatsouras 2015}$].

The key idea is that Oxide already does a pointer analysis! Performing one is an essential task in ensuring ownership-safety. All we have to do is extract the relevant information with Oxide's existing judgments. This is represented by the information flow extension to the reference-mutation rule:

Here, the important concept is Oxide's ownership safety judgment: $\Delta ;\Gamma {⊢}_{\omega }p\Rightarrow \{\overline{l}\}$, read as "in the contexts $\Delta$ and $\Gamma$, $p$ can be used $\omega$-ly and points to a loan in $\{\overline{l}\}$." A loan $l::={}^{\omega }p$ is a place expression with an ownership-qualifier. In Oxide, this judgment is used to ensure that a place is used safely at a given level of mutability. For instance, in the example at the top of this column, if $\ast z:=1$ was replaced with $x.1:=1$, then this would violate ownership-safety because $x$ is already borrowed by $y$ and $z$.

In the example as written, the ownership-safety judgment for $\ast z$ would compute the loan set:

Note that $x.1$ is in the loan set of $\ast z$. That suggests the loan set can be used as a pointer analysis. The complete details of computing the loan set can be found in $\text{Weiss et al. [2019, p. 12]}$, but the summary for this example is:

1. Checking the borrow expression "$\&r_1\mathsf{uniq}x$" gets the loan set for $x$, which is just $\{{}^{\mathsf{uniq}}x\}$, and so sets $\Gamma (r_1)=\{{}^{\mathsf{uniq}}x\}$.

2. Checking the assignment "$y=\&r_1\mathsf{uniq}x$" requires that $\&r_1\mathsf{uniq}(u32,u32)$ is a subtype of $\&r_2\mathsf{uniq}(u32,u32)$, which requires that $r_1$ "outlives" $r_2$, denoted $r_1:>r_2$.

3. The constraint $r_1:>r_2$ adds $\Gamma (r_1)$ to $\Gamma (r_2)$, so $\Gamma (r_2)=\{{}^{\mathsf{uniq}}x\}$.

4. Checking "$\&r_3\mathsf{uniq}(\ast y).1$" gets the loan set for $(\ast y).1$, which is:

   $$\{{}^{\mathsf{uniq}}p.1\mid {}^{\mathsf{uniq}}p\in \Gamma (r_2)\}\cup \{{}^{\mathsf{uniq}}(\ast y).1\}=\{{}^{\mathsf{uniq}}x.1,{}^{\mathsf{uniq}}(\ast y).1\}$$

   That is, the loans for $r_2$ are looked up in $\Gamma$ (to get $\{x\}$), and then the additional projection $\_.1$ is added on-top of each loan (to get $\{x.1\}$).

5. Then $\Gamma (r_4)=\Gamma (r_3)$ because $r_3:>r_4$.

6. Finally, the loan set for $\ast z$ is:

   $$\Gamma (r_4)\cup \{{}^{\mathsf{uniq}}(\ast z)\}=\{{}^{\mathsf{uniq}}x.1,{}^{\mathsf{uniq}}(\ast y).1,{}^{\mathsf{uniq}}(\ast z)\}$$

Applying this concept to the T-assignderef rule, we compute information flow for reference-mutation as: when mutating $p$ with loans $\{\overline{l}\}$, add ${\kappa }_e$ to all the conflicts for every loan ${}^{\mathsf{uniq}}{p}^{\prime }\in \{\overline{l}\}$.

2.3 Function Calls

Finally, we examine how to modularly compute information flow through function calls, starting with syntax:

Oxide functions are parameterized by frame variables $\phi$ (for closures), abstract provenances $\varrho$ (for provenance polymorphism), and type variables $\alpha$ (for type polymorphism). Unlike Oxide, we restrict to functions with one argument for simplicity in the formalism. Calling a function $f$ requires an argument $\pi$ and any type-level parameters $\Phi ,\rho$ and $\tau$.

The key question is: without inspecting its definition, what is the most precise assumption we can make about a function's information flow while still being sound? By "precise" we mean "if the analysis says there is a flow, then the flow actually exists", and by "sound" we mean "if a flow actually exists, then the analysis says that flow exists." For example consider this program:

First, what can $\mathsf{f}(t)$ mutate? Any data behind a shared reference is immutable, so only $\ast t.0$ could possibly be mutated, not $\ast t.1$. More generally, the argument's transitive mutable references must be assumed to be mutated.

Second, what are the inputs to the mutation of $\ast t.0$? This could theoretically be any possible value in the input, so both $\ast t.0$ and $\ast t.1$. More generally, every transitively readable place from the argument must be assumed to be to be an input to the mutation. So in this example, a modular analysis of the information flow from calling $\mathsf{cp}$ would add $\{{\ell }_1,{\ell }_2\}$ to $\Theta (x)$ but not $\Theta (y)$.

To formalize these concepts, we first need to describe the transitive references of a place. The $\omega \text{-}\mathsf{refs}(p,\tau )$ metafunction computes a place expression for every reference accessible from $p$. If $\omega =\mathsf{uniq}$ then this just includes unique references, otherwise it includes unique and shared ones.

Here, $\omega \lesssim {\omega }^{\prime }$ means "a loan at $\omega$ can be used as a loan at ${\omega }^{\prime }$", defined as $\mathsf{uniq}/\lesssim \mathsf{shrd}$ and $\omega \lesssim {\omega }^{\prime }$ otherwise. Then $\omega \text{-}\mathsf{loans}(p,\tau ,\Delta ,\Gamma )$ can be defined as the set of concrete places accessible from those transitive references:

Finally, the function application rule can be revised to include information flow as follows:

The collective dependencies of the input $\pi$ are collected into ${\kappa }_{\mathsf{arg}}$, and then every unique reference is updated with ${\kappa }_{\mathsf{arg}}$. Additionally, the function's return value is assumed to be influenced by any input, and so has dependencies ${\kappa }_{\mathsf{arg}}$.

Note that this rule does not depend on the body $e$ of the function $f$, only its type signature in $\Sigma$. This is the key to the modular approximation. Additionally, it means that this analysis can trivially handle higher-order functions. If $f$ were a parameter to the function being analyzed, then no control-flow analysis is needed to guess its definition.

4.1 Analyzing Control-Flow Graphs

The Rust compiler lowers programs into a "mid-level representation", or MIR, that represents programs as a control-flow graph. Essentially, expressions are flattened into sequences of instructions (basic blocks) which terminate in instructions that can jump to other blocks, like a branch or function call. Figure 1 shows an example CFG and its information flow.

To implement the modular information flow analysis for MIR, we reused standard static analysis techniques for CFGs, i.e., a flow-sensitive, forward dataflow analysis pass where:

• At each instruction, we maintain a mapping from place expressions to a set of locations in the CFG on which the place is dependent, comparable to $\Theta$ in Section 2.

• A transfer function updates $\Theta$ for each instruction, e.g. $p:=e$ follows the same rules as in T-assignderef by adding the dependencies of $e$ to all conflicts of aliases of $p$.

• The input ${\Theta }^{\mathsf{in}}$ to a basic block is the join of each of the output ${\Theta }_i^{\mathsf{out}}$ for each incoming edge, i.e. ${\Theta }^{\mathsf{in}}={\bigvee }_i{\Theta }_i^{\mathsf{out}}$ . The join operation is key-wise set union, or more precisely:

  $${\Theta }_1\vee {\Theta }_2\stackrel{\mathrm{def}}{=}\{x\mapsto {\Theta }_1(x)\cup {\Theta }_2(x)\mid x\in {\Theta }_1\vee x\in {\Theta }_2\}$$

• We iterate this analysis to a fixpoint, which we are guaranteed to reach because $⟨\Theta ,\vee ⟩$ forms a join-semilattice.

To handle indirect information flows via control flow, such as the dependence of h on contains_key in Figure 1, we compute the control-dependence between instructions. We define control-dependence following $\text{Ferrante et al. [1987]}$: an instruction $Y$ is control-dependent on $X$ if there exists a directed path $P$ from $X$ to $Y$ such that any $Z$ in $P$ is post-dominated by $Y$, and $X$ is not post-dominated by $Y$. An instruction $X$ is post-dominated by $Y$ if $Y$ is on every path from $X$ to a return node. We compute control-dependencies by generating the post-dominator tree and frontier of the CFG using the algorithms of $\text{Cooper et al. [2001]}$ and $\text{Cytron et al. [1989]}$, respectively.

Besides a return, the only other control-flow path out of a function in Rust is a panic. For example, each function call in Figure 1 actually has an implicit edge to a panic node (not depicted). Unlike exceptions in other languages, panics are designed to indicate unrecoverable failure. Therefore we exclude panics from our control-dependence analysis.

4.2 Computing Loan Sets from Lifetimes

To verify ownership-safety (perform "borrow-checking"), the Rust compiler does not explicitly build the loan sets of lifetimes (or provenances in Oxide terminology). The borrow checking algorithm performs a sort of flow-sensitive dataflow analysis that determines the range of code during which a lifetime is valid, and then checks for conflicts e.g. in overlapping lifetimes (see the non-lexical lifetimes RFC [$\text{Niko Matsakis 2017}$].

However, Rust's borrow checker relies on the same fundamental language feature as Oxide to verify ownership-safety: outlives-constraints. For a given Rust function, Rust can output the set of outlives-constraints between all lifetimes in the function. These lifetimes are generated in the same manner as in Oxide, such as from inferred subtyping requirements or user-provided outlives-constraints. Then given these constraints, we compute loan sets via a process similar to the ownership-safety judgment described in Section 2.2. In short, for all instances of borrow expressions $\&r\omega p$ in the MIR program, we initialize $\Gamma (r)=\{p\}$. Then we propagate loans via $\Gamma (r)={\bigcup }_{r^{\prime }:>r}\Gamma (r^{\prime })$ until $\Gamma$ reaches a fixpoint.

4.3 Handling Ownership-Unsafe Code

Rust has a concept of raw pointers whose behavior is comparable to pointers in C. For a type T, an immutable reference has type &T, while an immutable raw pointer has type *const T. Raw pointers are not subject to ownership restrictions, and they can only be used in blocks of code demarcated as unsafe. They are primarily used to interoperate with other languages like C, and to implement primitives that cannot be proved as ownership-safe via Rust's rules.

Our pointer and mutation analysis fundamentally relies on ownership-safety for soundness. We do not try to analyze information flowing directly through unsafe code, as it would be subject to the same difficulties of C++ in Section 1. While this limits the applicability of our analysis, empirical studies have shown that most Rust code does not (directly) use unsafe blocks [$\text{Astrauskas et al. 2020}$][$\text{Evans et al. 2020}$]. We further discuss the impact and potential mitigations of this limitation in Section 8.

5.1 Dataset

To empirically compare these modifications, we curated a dataset of Rust packages (or "crates") to analyze. We had two selection criteria:

1. To mitigate the single-crate limitation of Whole-Program, we preferred large crates so as to see a greater impact from the Whole-Program modification. We only considered crates with over 10,000 lines of code as measured by the cloc utility [$\text{Al Danial 2021}$].

2. To control for code styles specific to individual applications, we wanted crates from a wide range of domains.

After a manual review of large crates in the Rust ecosystem, we selected 10 crates, shown in Figure 2. We built each crate with as many feature flags enabled as would work on our Ubuntu 16.04 machine. Details like the specific flags and commit hashes can be found in the appendix.

For each crate, we ran the information flow analysis on every function in the crate, repeated under each of the 8 conditions. Within a function, for each local variable $x$, we compute the size of $\Theta (x)$ at the exit of the CFG — in terms of program slicing, we compute the size of the variable's backward slice at the function's return instructions. The resulting dataset then has four independent variables (crate, function, condition, variable name) and one dependent variable (size of dependency set) for a total of 3,487,832 data points.

Our main goal in this evaluation is to analyze precision, not performance. Our baseline implementation is reasonably optimized — the median per-function execution time was 370.24$\mu \text{s}$. But Whole-Program is designed to be as precise as possible, so its naive recursion is sometimes extremely slow. For example, when analyzing the GameEngine::render function of the rg3d crate (with thousands of functions in its call graph), the modular analysis takes 0.13s while the recursive analysis takes 23.18s, a 178$\times$ slowdown. Future work could compare our modular analysis to whole-program analyses across the precision/performance spectrum, such as in the extensive literature on context-sensitivity [$\text{Smaragdakis and Balatsouras 2015}$].

5.2 Quantitative Results

We observed no meaningful patterns from the interaction of modifications — for example, in a linear regression of the interaction of Mut-Blind and Pointer-Blind against the size of the dependency set, each condition is individually statistically significant ($p<0.001$) while their interaction is not ($p=0.337$). So to simplify our presentation, we focus only on four conditions: three for each modification individually active with the rest disabled, and one for all modifications disabled, referred to as Baseline.

5.3 Qualitative Results

The statistics convey a sense of how often each condition influences precision. But it is equally valuable to understand the kind of code that leads to such differences. For each condition, we manually inspected a sample of cases with non-zero differences vs. Baseline.

5.4 Threats to Validity

Finally, we address the issue: how meaningful are the results above? How likely would they generalize to arbitrary code rather than just our selected dataset? We discuss a few threats to validity below.

1. Are the results due to only a few crates?

   If differences between techniques only arose in a small number of situations that happen to be in our dataset, then our technique would not be as generally applicable. To determine the variation between crates, we generated a histogram of non-zero differences for the Baseline vs. Mut-Blind comparison, broken down by crate in Figure 5.