Linearity and Aliasing as a Confinement Discipline

A capability is only as strong as the guarantee that it cannot be duplicated. If a program handed a read-only reference can copy the reference and pass it on, then the reference is a name, and the authority it carries spreads without the granter’s knowledge. Type systems that restrict duplication and aliasing turn that guarantee from a runtime convention into a compile-time fact.

Duplication is the primitive that must be controlled

In a language where every value can be copied freely, any reference can become any number of references. The consequence for security is that “this module receives the reference” says nothing about where the reference ends up: it may be stored in a global, captured by a closure, written to a queue, or serialized. The authority granted to the module is the authority granted to every place the reference reaches, transitively, for the lifetime of the program.

A linear type system makes the opposite assumption. A value of linear type must be used exactly once: it cannot be dropped, and it cannot be copied. Affine systems relax this to at most once, allowing the value to be discarded. Rust’s ownership model is affine: a value may be moved between owners, borrowed temporarily, or dropped, but a non-Copy value cannot be duplicated by assignment. Duplication requires an explicit Clone, which the type’s author can decline to implement or can restrict.

The security reading is direct. A token type that does not implement Clone cannot be duplicated, so the number of places holding the token is bounded by the number of tokens constructed. If construction is private to the module that issues them, the issuer controls the total authority in circulation, which is the property a capability system needs.

use std::fs::File;
use std::io::{self, Write};

// No Clone impl, so the issuer controls how many exist.
pub struct WriteOnce {
    file: File,
}

impl WriteOnce {
    pub fn new(file: File) -> Self {
        WriteOnce { file }
    }
    // Takes self by value: the token is spent by the call.
    pub fn write(mut self, buf: &[u8]) -> io::Result<()> {
        self.file.write_all(buf)
    }
}

Consuming self in write is a stronger statement than merely preventing duplication: it makes the token single-use. Each call spends the capability. Whether that is the right semantics depends on the resource, but the point is that the type declares it and the compiler enforces it.

Borrowing and the temporary narrowing of authority

Rust separates ownership from access through borrowing. A shared reference &T permits reads and forbids mutation; a mutable reference &mut T permits mutation and excludes every other reference for its lifetime. The borrow checker enforces the exclusion statically by rejecting any program in which a borrow outlives its referent or overlaps an incompatible borrow.

For confinement, the useful half is the mutable reference. A function that takes &mut T has exclusive access to T for the duration of the call, which means the callee’s effect on T is bounded by the call. If the caller retains no other reference, then whatever the callee does to T is visible to the caller afterwards and to nobody else concurrently. This is the same guarantee a lock provides, obtained without a lock, and it is what makes it possible to hand a subsystem a mutable view of a data structure without worrying about concurrent modification from elsewhere.

The shared reference has a different role. Because &T cannot mutate, passing one to untrusted code grants read access and nothing else, and the compiler will reject any attempt by the callee to write through it. A sandbox API that accepts &Config rather than &mut Config has made a compile-time statement about what the callee can do.

The limit is that these guarantees concern memory safety and data races, not information flow. A callee holding &Config can copy the values out and return them, store them, or transmit them. Preventing that requires a different machinery: information-flow typing, where values carry a label and the type system rejects flows from a high label to a low sink. Rust’s types do not carry such labels, so a &Secret can be read and leaked by any code that receives it. The borrow checker says nothing about confidentiality.

Regions and the shape of an isolation proof

A region-based system groups allocations by lifetime and proves that no reference from one region escapes into another. The mechanism predates Rust and appears in Cyclone and in region inference for ML. Its security form is the statement that a value allocated in a compartment cannot be referenced from outside the compartment, which is precisely the property that makes colocated tenants safe.

The proof obligation has three parts. Allocation must be attributable to a region: the allocator must record which region an object belongs to, so that a reference can be checked. References must be typed by region: the type of a pointer must mention the region it may point into. Escape must be rejected: an assignment that would place a region-A pointer into a region-B location must fail to typecheck.

A system that discharges all three has a static guarantee that no pointer crosses between tenants. The guarantee is about pointers, not about the data they point to: a tenant can copy the bytes out and hand the copy to another tenant, because the copy is a value, not a reference. Isolation of memory is not isolation of information, and conflating the two is a recurring error.

Where the type-level proof is defeated

Every static guarantee in a systems language is conditional on the escape hatches being closed. Rust’s unsafe is the escape hatch, and it is not a small one: a block of unsafe code can transmute between types, dereference arbitrary addresses, and produce a reference with a lifetime the compiler did not verify. A single such reference, if it points at another tenant’s memory, invalidates the region proof for the whole program.

The soundness of the surrounding abstractions is therefore part of the security argument. Vec’s implementation uses unsafe internally and exposes a safe interface; the proof that the interface is safe is an argument about the implementation, made by a human, and it is not checked by the compiler. A vulnerability in a standard library abstraction, or in a third-party crate’s unsafe code, is a hole in the confinement exactly as a verifier bug is a hole in a bytecode sandbox.

There is a second and less obvious defeat. The affine rule permits dropping, and dropping runs a destructor. A destructor is code that executes at a moment the type system does not track, and it can do anything: it can enqueue the value, log it, or send it. If a capability’s destructor performs a privileged action, the authority is exercised at a point no borrow annotation covers. Destructors are effects, and effects escape the ownership discipline.

A third: interior mutability. Cell, RefCell, and atomics allow mutation through a shared reference, so &T no longer implies read-only. The compiler accepts this because the mutation is routed through a checked runtime path, but the security reading of “shared reference means read access” is lost. An API that means to grant read-only access must use types that genuinely cannot mutate, which in Rust means avoiding interior mutability in the exposed type.

The composition with runtime mediation

Type-level confinement and runtime mediation answer different questions. The type system says what a piece of code can express; the runtime says what the expressed operations are permitted to do. Neither substitutes for the other.

A borrow-checked interface can guarantee that a plugin cannot hold a reference after the call returns, which means the host can free or reuse the underlying resource immediately. That is a lifetime guarantee the host would otherwise need reference counting or a garbage collector to obtain. It is a real reduction in the trusted base, because reference counting and collection are both code that can be wrong.

Conversely, the type system cannot express policy. It can prove that a value is used once, but not that the value was issued to the right principal, or that the resource it designates is one the principal should reach. Policy lives in the construction of values, which is ordinary code, and the argument that construction is correct is an argument about the program, not a theorem about the language.

The practical arrangement puts the construction behind a narrow interface that the host owns, uses the type system to guarantee no duplication or escape, and keeps the resource itself behind the runtime’s mediation so that a defect in the type-level argument does not become a defect in the boundary. The relationship between the two layers is the same one described in the runtime as reference monitor, with the type system acting as a second, cheaper mediator that rejects programs before they run.

What linearity buys, stated plainly

Three properties, each of which is otherwise expensive:

Aliasing control. No two live mutable references to the same data, so no data race and no surprise modification from a path the caller did not consider.

Uniqueness for ownership transfer. A value moved into a subsystem is no longer available to the sender, so the subsystem’s authority over it is exclusive. This is the mechanism by which a resource can be handed over rather than shared.

Bounded authority per value. A token that cannot be cloned bounds the number of grants by the number of tokens constructed, which turns a policy question into a counting question.

The costs are equally concrete. Every transfer must be explicit, so interfaces grow lifetime parameters and ownership annotations. Cyclic data structures require an escape into reference counting or unsafe code, and each escape is a place where the guarantee no longer holds. And the guarantees stop at memory: no information-flow label, no integrity label, no statement about what a value means. For those, the system needs the machinery of attenuation and revocation, which operates on capabilities at runtime, and information-flow considerations that no ownership rule addresses.