Ownership and Borrowing as a Static Lifetime Proof

Every other mechanism discussed here detects a lifetime violation after the fact. A quarantine widens the window in which a stale access is visible; a shadow stack compares a return address at the moment it is used; a capability faults at the offending instruction. All of them answer the same question at run time: is this access legal right now. A borrow checker answers a different question at compile time: can any execution of this program make this access illegal. If the answer is no, the program is accepted and needs no check. If the answer is yes, the program does not compile.

The mechanism is a set of rules about who may hold a reference to what, enforced by an analysis that tracks every reference’s lifetime through the control-flow graph. It is the only approach in this cluster that removes the bug class rather than mitigating it, and it is also the one with the most visible cost to the programmer.

Moves make ownership unique

The foundation is that a value has exactly one owner at a time, and that transferring ownership invalidates the previous holder.

let s = String::from("buffer");
let t = s;              // ownership moves to t
println!("{}", s);      // rejected: s is no longer valid

An assignment of a non-copyable value is a move, not a copy: the bytes may or may not be duplicated in the generated code, but the source binding is marked uninitialised and any later use is a compile error. The consequence is that the double-free problem disappears at the source level. There is no point in the program at which two variables own the same allocation, so there is no second owner to release it. The allocator’s integrity checks still exist for the unsafe code underneath, but the safe surface cannot produce the second release.

Moves also fix the aliasing that makes use-after-free hard to reason about. A function that takes ownership of a value can free it, and the caller cannot retain a pointer to it because the caller no longer has the value. The lifetime of the allocation is tied to the lifetime of exactly one binding, and the compiler tracks the binding through every branch of the control flow.

Copy types are the exception, and the exception is principled. A type whose value is a plain sequence of bits with no owned resource can be duplicated freely, because the duplicate owns nothing. The distinction is expressed by a trait that the compiler treats specially: implementing it declares that a bitwise copy is semantically a full copy. Getting that declaration wrong for a type that does own a resource is the one way to reintroduce a double free in safe code, and it requires deliberately implementing the trait for a type containing a pointer.

Borrows are loans with scopes

Most code does not want to move a value; it wants to look at it. A reference is a loan, and the rules of the loan are what the borrow checker enforces: any number of shared references, or exactly one mutable reference, and never both at once.

The exclusivity rule is what makes the analysis tractable and what makes the safety argument work. A shared reference may not be used to mutate, so no other reference can observe a change through it. A mutable reference is exclusive, so no other reference exists while it is live, which means a mutation through it cannot invalidate any other reference. Together the two rules give the compiler a property it can check locally: at any program point, the set of live references to a value is either a non-empty set of shared references or a single mutable one.

fn extend(v: &mut Vec<u8>, extra: &[u8]) {
    // Both borrows are live here; the compiler verifies they are disjoint.
    v.extend_from_slice(extra);
}

fn bad(v: &mut Vec<u8>) {
    let first = &v[0];          // shared borrow of v's contents
    v.push(1);                  // mutable borrow: rejected while first is live
    println!("{}", first);
}

The second function is the canonical rejection, and the reason is concrete: push may reallocate the vector’s buffer, which would leave first pointing at freed memory. The check is not a heuristic about what push does; it is a consequence of the exclusivity rule, which says a mutable borrow cannot coexist with a shared one. The compiler does not need to know that push can reallocate, and it would reject the same code even if it could prove the capacity was sufficient, because the rule is structural rather than semantic.

The cost of that structural rule is real. Code that would be safe because the reallocation does not happen, or because the shared reference is not used after the mutation, is rejected. The programmer’s options are to restructure (copy the value out, split the borrow, use an index instead of a reference) or to reach for a runtime-checked container, which moves the check from compile time to run time and reintroduces the possibility of a panic.

Lifetimes are the analysis, not an annotation language

A lifetime parameter is the compiler’s name for a region of the program, and the annotations exist because the compiler needs to know how the lifetimes of inputs and outputs relate when a function’s body is not visible to its callers.

fn longest<'a>(x: &'a str, y: &'a str) -> &'a str {
    if x.len() > y.len() { x } else { y }
}

The signature says the returned reference is valid for no longer than the shorter of the two inputs. Without the annotation the compiler would have to assume the output could outlive either input, which it cannot verify, so it rejects the function. The annotation is a claim the compiler checks against the body: the returned reference must be derived from one of the inputs, and its uses must fall within the region the caller supplies.

The key point is that lifetimes are not a runtime concept and do not exist in the generated code. They are constraints on the analysis, and the analysis is a data-flow problem over the control-flow graph. The original formulation tied each reference’s lifetime to its lexical scope, which rejected programs that were obviously safe: a reference taken inside a loop and dropped before the next iteration has a scope longer than its actual use. Non-lexical lifetimes replaced the lexical scope with a liveness analysis: a borrow ends at its last use, computed from the control-flow graph, which accepts a much larger class of programs without weakening the guarantee.

let mut v = vec![1, 2, 3];
let r = &v[0];
println!("{}", r);       // last use of r
v.push(4);               // accepted: the borrow has ended

Under the lexical rule the borrow would extend to the end of the enclosing block and the push would be rejected. Under the liveness rule the borrow ends at the println, and the mutation is accepted because no shared reference is live across it. The safety argument is unchanged: at the point of the push, no reference exists that the reallocation could invalidate.

Where the proof cannot reach

The borrow checker is sound for the safe subset, and the safe subset is not the whole language. Three boundaries matter.

The first is unsafe code. Operations that the analysis cannot model, such as dereferencing a raw pointer or calling into foreign code, are permitted inside an unsafe block, and the safety argument for that block is the programmer’s obligation. The compiler’s guarantee is conditional: safe code cannot violate memory safety provided every unsafe block upholds its stated contract. A bug in a collection’s internals is a bug in an unsafe block, and it is exactly the class of bug the shadow-memory tools are built to find, which is why they remain in use in projects written in memory-safe languages.

The second is interior mutability. A type that permits mutation through a shared reference, such as a cell that tracks borrows at run time or an atomic, steps outside the exclusivity rule and enforces it by other means. The compiler’s static guarantee becomes a runtime one: a RefCell keeps a borrow counter that is checked when a borrow is taken, so a conflicting borrow is a panic rather than a compile error. An atomic removes the exclusivity question from the checker entirely by making each operation indivisible. Memory safety survives in both cases because a check or an atomicity guarantee stands where the static rule did, but for the cell the failure mode moves from “does not compile” to “terminates at run time”.

The third is the boundary with code the compiler did not analyse. A foreign function that retains a pointer after the call returns, or that frees memory the caller still owns, is outside the model. The interface must encode the contract in its type, whether by taking ownership, borrowing for a stated lifetime, or returning a value the caller owns, and the encoding is a human judgement about what the foreign code does. When the judgement is wrong, the compiler’s proof is about a program that does not match the one being run.

What the trade actually is

The trade is not safety against speed. Safe Rust compiles to code with no bounds checks at the borrow level, because the borrows are gone by then; the checks that remain are the slice bounds checks that the language keeps for indexing, and those are the same ones any checked language pays. The trade is safety against expressiveness: programs whose aliasing patterns the analysis cannot describe must be restructured or moved into unsafe code, and the restructuring is a real cost paid by the programmer rather than by the machine.

The compensating benefit is that the cost is paid once, at compile time, and the resulting program has no runtime mechanism to disable, no instrumentation to remove for production, and no coverage question about which libraries were built with the checks. That is the property none of the runtime mitigations described here can offer: the canary can be compiled out, the sanitizer only checks instrumented code, and the capability machine protects only the code compiled for it. A static proof is either present in the program or the program does not exist, which is why the approach has spread from one language’s design into the type systems of several others and into the C and C++ proposals that aim to give existing code a checkable subset.