Forte adds sensitivity tracking to mutable Rust code for privacy
Forte: A sensitivity type system for imperative Rust
Programming Languages
Summary
Programs that handle sensitive data often need to ensure privacy by keeping track of how much information is used or changed. Previous tools worked well only with code that doesn’t change data, but many real-world programs written in Rust do change data through a feature called borrowing. The authors introduce Forte, a system that tracks sensitivity in Rust programs even when data changes, by using Rust’s ownership rules. They prove that Forte reliably detects changes and applies it to existing privacy software to catch bugs and verify privacy guarantees.
What this means in practice
- •For privacy software developers: Check and verify that privacy-preserving Rust programs correctly manage data sensitivity even with mutable state and borrows.
- •For secure software engineers: Use Forte to find and fix bugs involving incorrect data sensitivity assumptions in Rust code with in-place mutation.
Authors
Chiké Abuah
Abstract
We introduce Forte, a sensitivity type system for Rust whose soundness rests on ownership. The graded sensitivity type systems, from Fuzz's linear grading to Solo's environment indices, are pure calculi: a claim about a value holds for the value's whole lifetime because nothing can mutate it. The imperative sensitivity analyses admit assignment to first-order variables and no references, so no question of aliasing arises in them. The programs that compute differentially private statistics in deployment are Rust, and they mutate through borrows. Forte closes this gap. Its central rules strongly update a sensitivity environment through an exclusive borrow, at a primitive call and across a checked function boundary; its soundness theorem is metric preservation over an operational semantics with a store, in which the exclusivity of &mut alone licenses framing across a mutating call, and two aliased borrows suffice to refute the theorem without it. Verus mechanizes the theorem, the function rule, and the refutation. Flux checks Forte as an ordinary library, with no fork of the compiler; a machine-checked theorem backs every deterministic primitive signature, and a correspondence theorem transports metric preservation to the programs the checker accepts. We evaluate Forte on mechanism kernels from OpenDP with genuine in-place mutation, matching the library's trusted stability maps with checked constants, covering the constructors that have no proof document, rejecting off-by-one diameters, tightened bounds, miscalibrated releases, and overspent budgets, and deriving one trusted constant as an inferred loop invariant.