Rust's Borrow Checker Meets Differential Privacy: A Type System That Works in the Real World
Differential privacy is the gold standard for privacy-preserving data analysis, and every differentially private mechanism calibrates its noise to a sensitivity: a bound on how far a query's output can move when one individual's data changes. Get the sensitivity wrong, and the privacy guarantee evaporates -- silently, with no visible symptom. The program runs, the output looks plausible, and the guarantee no longer holds.
This is not a hypothetical risk. Casacuberta et al. documented widespread sensitivity underestimation across deployed differential privacy libraries, much of it traceable to subtleties that a type system should police: metric conventions, neighboring definitions, and constants conflated between them. Yet the type systems designed to catch these errors cannot host the code that actually runs in production. The flagship open-source library OpenDP attaches a "stability map" to each transformation -- a trusted runtime closure from input distance to output distance -- but 109 hand-written proof documents accompany the codebase and reach only 14 of the 68 trusted stability closures in its transformation constructors. Every variant of the bounded sum is among the constructors without a proof document.
A new paper from Chiké Abuah introduces Forte, a sensitivity type system for Rust whose soundness rests on ownership. The key insight is that Rust's exclusive mutable borrow alone licenses framing across a mutating call, which means the type system can strongly update a sensitivity environment in place -- where prior systems required either purity or linearity. The paper delivers a mechanized, machine-checked system that plugs directly into Rust's existing tooling, requiring no compiler fork.
Why Existing Sensitivity Type Systems Cannot Host Production Code
The sensitivity type system literature spans two families, and neither can express deployed differential privacy programs.
Pure calculi, from Fuzz's linear grading to DFuzz, Duet, Jazz, and Solo's environment indices, treat values as flowing by substitution. A claim attached to a value holds for the value's entire lifetime because nothing can mutate what it describes. These systems are elegant and sound, but they assume a world without in-place mutation.
Imperative sensitivity analyses, including Fuzzi and the LightDP line, admit assignment to first-order variables but exclude references entirely. In these systems, two names never denote one location, so aliasing never arises. The programs that compute differentially private statistics in deployment, however, are written in imperative Rust and mutate through borrows.
OpenDP's mechanism kernels accumulate totals through mutable borrows, build histograms by in-place increment, and grow tree layers in place. Consider a helper function that clamps and sums one dataset and adds the result into an accumulator borrowed from its caller. The function signature declares an environment update: the accumulator's sensitivity environment after the call differs from what it was before, computed from the environment it arrived with plus the sum's sensitivity. Inside the function, the trusted add_assign primitive performs the same kind of update.
In a pure calculus, this pattern is inexpressible. In an imperative calculus without references, it is expressible only by inlining the helper at every call site, because a function that mutates an argument needs a name for the caller's location. The soundness argument for the call needs one fact: while the mutable borrow of the accumulator is live, no other view of that accumulator exists. Rust's borrow checker supplies that fact.
The Core Insight: Exclusivity Enables Framing
Forte's central claim is that the exclusivity of a Rust mutable borrow alone licenses framing across a mutating call. When a caller borrows &mut acc to a helper, the type system can reason that while the borrow is live, no other reference to acc exists. This means a claim attached to acc -- its sensitivity environment -- can be updated in place without conflicting with the caller's view.
The update arithmetic is alias-tolerant by design. A call that reads one location twice computes x+x, and the environment 2s the rules assign is a correct bound, because environment-indexed sensitivity charges contraction by addition. But aliasing breaks the frame, the treatment of distinct claims as claims about distinct locations. If two exclusive borrows of the same local exist, the type system retains the second parameter's stale environment for a location whose contents the first parameter updated, and a later read at that stale environment is unsound.
Forte makes this premise explicit and formal. Two aliased exclusive borrows suffice to derive a false claim, which means exclusivity is not merely convenient but necessary for the soundness theorem. The paper proves this through a counterexample mechanized in Verus, showing that without borrow exclusivity, the framing argument collapses.
How Forte Works
Forte is built as λ-Forte, a first-order, store-based core calculus with mutable locals, exclusive borrows at call sites, functions whose parameters are exclusive borrows, loops over public counters, and a trusted signature set standing for the primitive library. The fragment is deliberately narrow so that the ownership question remains live: the proof must establish a frame across a mutating call and across a checked function boundary, while remaining an induction on evaluation.
Sensitivity environments are the core abstraction. A program declares a finite set of sources, the units of protection. Each source has a metric on its input space. A sensitivity environment assigns one coefficient per source, and the environment attached to a value bounds how far that value can move when a source changes. Types are public base types, sensitive scalars annotated with an environment vector, and sensitive vectors under three metrics: elementwise L1 distance, substituted-row count, and L-infinity distance.
The typing judgment is flow-sensitive, with an output context recording types after evaluation. Assignment retypes the assigned local, so ordinary mutation of locals is already a strong update. The novel rules govern calls that mutate through borrows, both at a primitive and across a function boundary, and loops over public counters.
At a primitive call, the signature declares input and output types with environments. The call rule checks that each argument matches its expected type, and the result replaces each borrowed parameter's type with its output type, updated according to the ensures clause. Across a function boundary, the well-formedness rule requires that the function body types correctly under a context where each parameter's environment has been replaced by its declared output type, and the caller's actual environments are subtypes of the formal ones.
Loops deserve special attention. Accumulation under a loop couples the environment to the trip count. Forte relies on Flux, the checking tool, to infer loop invariants that bind the environment to the counter. In practice, this works naturally when the environment shares a sort with the loop counter, enabling exact bounds of the form "after n iterations, the total sensitivity is at most n times the per-iteration sensitivity."
Implementation: No Compiler Fork, No Trusted Base
Forte is realized as forte-rs, an ordinary Rust library checked by Flux, with no fork of the compiler. This is a significant practical achievement. Sensitivity environments are refinement indices on opaque structs. Strong updates are Flux's existing &mut ensures clauses. Flux infers loop invariants. The entire system plugs into Rust's existing toolchain.
There is, however, a subtlety. Flux's own soundness theorem is unary, a statement about one run of a program. A sensitivity claim relates two runs: the run with the original data and the run with one individual substituted. Metric preservation -- the property that a function's output distance is bounded by the sensitivity environment times the input distance -- is the theorem Flux cannot supply on its own. Forte addresses this with a correspondence theorem that transports metric preservation from λ-Forte derivations to every program the checker accepts in the fragment.
The trusted base is where Verus comes in. Every deterministic primitive signature obligation is a Verus theorem. Verus mechanizes the soundness core of the calculus, including the function rule and the refutation of its aliased form. The development comprises 43 verified theorems and lemmas, covering diameter rules, metric-conversion rules, and the arithmetic that Casacuberta et al. show to be error-prone in deployed libraries.
Case Studies: Finding Real Bugs in Real Libraries
The paper evaluates Forte on verified re-implementations of OpenDP mechanism kernels chosen specifically for their in-place mutation. The evaluation serves multiple purposes simultaneously: it validates the type system against known results, catches errors in deployed code, and demonstrates practical utility.
First, Forte matches the library's trusted stability maps with checked constants. OpenDP's make_sized_bounded_int_checked_sum constructor attaches a stability map that computes floor(d_in / 2) times the range. OpenDP trusts this closure based on a comment and a citation, with no proof document. Forte checks it mechanically, confirming that the diameter sum rule produces the same constant under the symmetric distance convention that OpenDP uses.
Second, Forte covers the 54 constructors in OpenDP that have no proof document at all. This is a substantial fraction of the trusted base and represents a gap in the library's verification infrastructure that Forte fills without requiring the library authors to write new proof documents.
Third, Forte rejects several categories of errors that Casacuberta et al. documented as recurring in deployed differential privacy libraries. Off-by-one diameters, tightened bounds that silently reduce the privacy guarantee, the Lipschitz reading of a clamp that treats bounded clamping as having sensitivity 1, under-calibrated releases that produce plausible-looking output with insufficient noise, and overspent budgets that accumulate beyond declared limits -- all are caught by the type checker, often before a single line of code compiles.
Fourth, Forte derives one trusted constant as an inferred loop invariant. In a function accumulating daily releases over n iterations, Flux discovers the invariant coupling the environment to the counter, certifying the total sensitivity as a function of both the per-iteration bound and the number of iterations. This is the first time a type system has derived a loop-dependent sensitivity constant as an invariant rather than having it asserted by a human author.
The Broader Significance
The paper closes a structural gap that has existed since sensitivity type systems were first proposed. The Fuzz-to-Solo lineage proved core calculi sound over substitution-based semantics. Forte restates and proves the same property over a store-based operational semantics, where the ownership of exclusive borrows -- not the absence of mutation -- is the fact that soundness consumes. The soundness proof asks nothing substructural of data: weakening, contraction, and exchange are all admissible in the sensitivity layer.
This distinction matters because it means Forte can be adopted by any Rust project that already uses the borrow checker. No new language, no new type system, no new syntax. The sensitivity environment is a refinement index on an opaque struct. The strong updates are ensured clauses that Flux already supports. The correspondence theorem connects the refinement-level checking to the calculus-level guarantee.
The paper also raises an important question about the future of privacy verification in systems programming. The gap between pure calculi and imperative deployment code is not unique to differential privacy. Any system that tracks resource usage, information flow, or security properties through mutation faces the same structural challenge. Forte's approach -- using ownership to license framing at mutable boundaries -- may generalize beyond sensitivity to other graded tracking problems that must survive real-world code.
Limitations and Open Directions
The paper acknowledges several constraints. The arithmetic model assumes unbounded integers and exact reals, so overflow and floating-point rounding fall outside the guarantee. OpenDP's own treatment of overflow and floating-point error composes with the checked constant as a trusted additive layer, but the floating-point half of the failures documented by Casacuberta et al. is out of scope.
The fragment excludes borrows that outlive a call, references stored in data structures, closures over sensitive data, and sensitive control flow. Each of these exclusions defers a harder problem. A borrow that outlives a call requires reasoning about the lifetime of the sensitivity claim beyond the call site. References stored in data structures introduce aliasing through data, not through the function call stack. Closures over sensitive data capture the same aliasing problem with more structure. Sensitive control flow adds the challenge of data-dependent branching on privacy properties.
The evaluation is limited to OpenDP's mechanism kernels and the AI2-THOR navigation task family for the core calculus. Broader evaluation across different application domains, different metrics, and different Rust codebases would strengthen the case for general applicability.
Nevertheless, the paper delivers something rare in the type systems literature: a soundness theorem that is both formally proven and practically deployed, checked by the same toolchain that programmers already use, catching real bugs in real libraries, without requiring any changes to the language itself. Forte does not ask the Rust community to adopt a new programming model. It asks them to add refinement types to their structs and ensures clauses to their functions, and the borrow checker -- already there -- does the rest.