Papers for

secure software engineers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Forte adds sensitivity tracking to mutable Rust code for privacy

Forte: A sensitivity type system for imperative Rust

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.

Thu 24 SeptProgramming Languages
The gist
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.
Open → 2609.30254v1