PaperlayerView exact revision on arXiv

Source-linked AI summary

Forte: A sensitivity type system for imperative Rust

Chiké Abuah

arXiv:2609.30254v1cs.PL

TL;DR

Differential privacy depends on correctly calibrated sensitivity, but deployed Rust programs mutate through borrows, a setting not addressed by prior sensitivity systems. Forte uses exclusive borrows to support sensitivity updates, and its checker rejects several miscalibrated bounds and releases in an OpenDP pipeline.

  • Problem

    Differential privacy mechanisms calibrate noise to sensitivity, but underestimating sensitivity silently invalidates the claimed privacy guarantee.

    Source: §1 · p. 1

  • Method

    Forte strongly updates sensitivity environments through exclusive borrows and checks the system as a Rust library, with Verus-backed primitive signatures and a correspondence theorem for accepted programs.

    Source: §1 · pp. 2–3

  • Results

    Forte rejects a 1-sensitivity claim for the pipeline and rejects the sum without its clamp, for which the unbounded vector type has no sum rule.

    Source: §2 · p. 4

  • Takeaways & Limitations

    Forte’s OpenDP case studies match trusted stability maps with checked constants, including for kernels that mutate in place.

    Source: §9 · p. 24

    The guarantee idealizes integers as unbounded and reals as exact, leaving overflow and floating-point rounding outside its scope.

    Source: §1 · p. 2

Abstract

from arXiv · show

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.

1 Introduction

Existing sensitivity type systems cannot express deployed Rust programs that mutate through references, leaving sensitivity claims in privacy mechanisms difficult to check statically. Forte uses Rust ownership to support checked sensitivity updates through exclusive borrows and applies this approach to OpenDP kernels.

1 Introduction

  • Deployed Rust mutates through references, while pure sensitivity calculi cannot model mutation and imperative analyses exclude references and aliasing.OpenDP attaches trusted stability maps to transformations, but proof documents cover only 14 of its 68 trusted stability closures.Source: §1 · pp. 1–2
  • Forte strongly updates sensitivity environments through exclusive borrows; without exclusivity, aliased borrows can invalidate the frame and produce a false claim.The soundness proof consumes ownership at this point, while sensitivity arithmetic itself permits weakening, contraction, and exchange.Source: §1 · p. 2
  • Flux checks Forte as an ordinary library without a compiler fork, while Verus mechanizes metric preservation and deterministic primitive-signature obligations.A correspondence theorem relates programs accepted by Flux to Forte derivations.Source: §1 · p. 2
  • The threat model excludes malicious authors and probabilistic release steps, while the arithmetic guarantee idealizes integers and reals, excluding overflow and floating-point rounding.OpenDP’s handling of overflow and floating-point error can compose as a trusted additive layer.Source: §1 · p. 2
  • OpenDP kernel case studies check trusted stability constants, cover 54 constructors without proof documents, reject several deployed-library errors, and infer one trusted constant as a loop invariant.The rejected errors include off-by-one diameters, tightened bounds, Lipschitz readings of clamps, under-calibrated releases, and overspent budgets.Source: §1 · p. 3

2 Overview of Forte

The overview illustrates Forte with a bounded-sum pipeline and mutating Rust helpers. Exclusive borrows support strong updates across calls and loops, while the checker rejects incorrect sensitivity claims and supports updates at public vector indices.

Overview of Forte

  • OpenDP has 109 hand-written proof documents, but they cover only 14 of 68 trusted stability closures; the illustrated constructor has no proof document despite its correct constant.The paper notes that the ecosystem has a record of widespread sensitivity underestimation.Source: §2 · pp. 3–4
  • For sized, bounded data, clamping establishes a bounds invariant and the sum rule scales each source’s sensitivity by the interval diameter hi−lo.Sized data has public, fixed length, so neighboring datasets substitute rows without adding or removing them.Source: §2 · p. 4
  • The checker rejects 1-sensitivity for the clamped sum and rejects the sum without clamping, where the unbounded vector has no sum rule.OpenDP’s symmetric input-distance convention counts 2 per substitution on sized data, making floor(d_in/2)·(U−L) correspond to the per-row diameter hi−lo.Source: §2 · p. 4

Sensitivity under mutation

  • A helper’s ensures clause describes the accumulator’s updated environment, allowing callers to reuse the helper instead of inlining mutation at each call.Repeated calls strongly update the accumulator’s environment from (0, 0, 0) through successive source contributions.Source: §2 · pp. 4–5

The role of exclusivity

  • Exclusive borrows let the soundness argument frame distinct locations; aliased exclusive borrows can leave a stale environment and support an unsound later read.The aliased call double_into(&mut acc, &mut acc) is rejected by Rust’s borrow checker before refinement checking.Source: §2 · p. 5

Loops and exact bounds

  • Flux infers a loop invariant coupling the accumulator’s sensitivity to the trip count for repeated clamped daily releases.The exact bound is available because the environment index and n share an integer sort; one case-study loop requires a hint.Source: §2 · pp. 5–6

Element writes at public indices

  • With a public write index, adding daily totals to a report updates one L1 coordinate, and Flux infers the loop invariant without hints.A data-dependent index would put the loop outside the checked fragment.Source: §2 · p. 6

3 Formal description of Forte

λ-Forte is a first-order, store-based core calculus for checked composition, with flow-sensitive sensitivity types that track mutation through exclusive borrows. Its rules update borrowed locals at primitive calls and checked function boundaries, with loops restricted to public guards.

3 Formal description of Forte

  • The checked core has mutable locals, exclusive call-site borrows, borrowed function parameters, public-counter loops, and trusted primitives; it excludes escaping references, sensitive closures, and sensitive control flow.The fragment keeps the ownership question live while deferring borrows that outlive calls and references stored in data structures.Source: §3 · p. 6
  • Each source has a metric, and a sensitivity environment assigns coefficients bounding how far a value can move as sources move; types track scalars and vectors under several metrics.The vector metrics are elementwise L1, substituted-row count, and L∞; bounded Sub types record a domain invariant that licenses the diameter sum rule.Source: §3 · pp. 6–7
  • Typing is flow-sensitive: output contexts record types after evaluation, while subtyping weakens environments pointwise and leaves public types unchanged.A well-typed program has well-formed declarations and a main expression typed in the empty context.Source: §3 · p. 7, Figure 2 · p. 8
  • Assignment retypes its local, while borrowed calls strongly update each borrowed local from its instantiated output type and require borrowed locals to be distinct.Repeated value arguments remain sound in the by-value fragment because the value is read before the write and the output environment prices the double read.Source: §3 · p. 7
  • A function is checked under its signature with borrowed parameters representing distinct locations; call-site distinctness lets its typing derivation transport to the caller.Rust’s borrow checker discharges this obligation at every call, preventing an ensures entry from describing a location another parameter has updated.Source: §3 · pp. 7–8
  • Loops use an existentially quantified invariant context that the implementation infers, and their guards must be public.Sensitive branching is out of scope for the core, and the case studies do not require it at the checked layer.Source: §3 · p. 9
  • The trusted signature set covers scalar, vector, metric-conversion, and structural primitives, with each entry backed by a mechanized semantic-validity obligation.The set includes diameter-scaling sum only for bounded Sub vectors and no sum rule for the unbounded form.Source: §3 · p. 9

4 Metatheory

Forte proves metric preservation over a store-based semantics: related source stores and typed programs produce related values and post-stores. The proof identifies borrow distinctness as necessary for strong updates and framing.

4 Metatheory

  • For well-formed declarations, metric preservation relates the runs’ output values and post-stores whenever the inputs and initial stores are related.The theorem also establishes termination of the second run; related runs follow equal public guards.Source: §4 · pp. 9–10
  • Every primitive signature is semantically valid, and a machine-checked theorem discharges every non-definitional case.The diameter-sum rule bounds clamped-sum differences by substituted-row count times the interval width.Source: §4 · p. 10
  • A mutating call preserves relatedness at every context variable outside its borrowed arguments and, for functions, fresh locals.Fresh callee locals scope out after the call.Source: §4 · p. 10
  • Strong updates preserve relatedness at borrowed locations when the borrowed locals are pairwise distinct.Distinctness ensures each location receives one post-value, matching the value described by the proof.Source: §4 · p. 10
  • Function-call soundness uses distinct actuals to make parameter substitution injective, then applies the body induction hypothesis and frames other caller variables.The callee’s post-stores relate at its output context and weaken into the ensures types.Source: §4 · p. 10
  • Aliasing two borrows of one sensitivity-1 local leaves a false sensitivity-1 claim after the call, although the stored value can differ by 2.The failure is a frame violation: the ensures entries were treated as claims about distinct locations.Source: §4 · pp. 10–11
  • The sensitivity layer admits weakening, contraction, and exchange; only the separate budget layer is affine.Environment addition prices duplicated claims at use sites.Source: §4 · p. 11
  • Verus mechanizes the scalar fragment’s metric-preservation theorem and function rule, as well as a refutation using an aliased call.The mechanized fragment includes assignment, public conditionals and loops, source reads, scalar primitives, and declared procedures with exclusive-borrow parameters.Source: §4 · p. 11

5 Implementation

Forte is implemented as a Flux-checked Rust library whose refinement-indexed environments support strong updates through mutable borrows. A correspondence theorem connects accepted programs in a defined fragment to the store-based calculus, while Verus proves the trusted primitive obligations.

Encoding

  • Sensitivity-bearing values use opaque structs indexed by fixed-width environment tuples; the library uses width three, and linear SMT arithmetic lets Flux infer loop invariants.Changing the environment width requires regenerating the types; Flux's existing &mut ensures clauses provide strong updates at primitive signatures and checked functions.Source: §5 · p. 11

Correspondence

  • The correspondence theorem transports metric preservation to checker-accepted programs in fragment F by elaborating their refinements and signatures into λ-Forte types.The theorem relies on a documented model of Flux checks; deriving that model's four properties from Flux's core calculus is left for future work.Source: §5 · p. 12

Trusted signatures

  • Each trusted Flux signature with a two-run obligation cites a Verus theorem proving its validity, and the calculus consumes those obligations by name.The one-to-one correspondence is recorded in signature documentation.Source: §5 · p. 13, Table 2 · p. 13

Budgets and release

  • Privacy budgets are non-Copy affine tokens consumed by moves, and release signatures reject under-budgeted or under-calibrated Laplace releases.The release side condition requires eps · scale ≥ 10^6 · sensitivity in micro-epsilons.Source: §5 · pp. 13–14

Trusted base

  • The trusted base includes inspected Rust primitive bodies, Flux and its solver, and user assertions about sources, metrics, and raw-data injection.The checker does not enforce the protocol that each program run mints only one budget token.Source: §5 · p. 14

6 Case studies

The case studies re-implement five OpenDP transformation families selected for genuine in-place mutation. Their certified constants agree with OpenDP after unit conversion, while checked derivations and negative controls expose both supported scope and boundaries.

Constants and conventions

  • Every certified constant agrees with OpenDP after one unit conversion, with OpenDP's symmetric distance counting two per substituted row on sized data.The evaluation re-implements kernels from five OpenDP transformation families selected for genuine in-place mutation.Source: §6 · pp. 14–15

Across a function boundary

  • A clamp-and-sum helper is checked across a function boundary and called from an accumulator and loop, whose invariant Flux infers without hints.The weekday kernel also mutates elements at public indices and releases with calibrated ε = 1 after splitting one token across two releases.Source: §6 · pp. 15, 17

From trusted constant to inferred invariant

  • For the b-ary tree, Forte derives OpenDP's layer-based bound through chunked sums and strong updates, with Flux inferring the loop invariant from two minimal hints.The hints provide qualifier shapes a ≤ i and a ≤ 1; the solver finds the invariant itself.Source: §6 · p. 15

Fused versus compositional accounting

  • For quantiles, the fused rule certifies 1 per row, while histogram-plus-prefix-sums composition certifies 2 per row; both derivations are sound.Only the fused derivation matches OpenDP's map, and no weakening rule lowers the compositional result below 2.Source: §6 · pp. 15–16

The count under two metrics

  • The same count is insensitive under sized substitution metrics but has stability d under add/remove distance on unsized data.A histogram over public categories moves two buckets per substituted row and receives certified constant 2.Source: §6 · p. 16

Manual proof obligation

  • For the covered kernels, seven corresponding proof documents contain 769 lines of manual proof, while the checked stability-map obligations use 131 lines of kernel code.Forte does not discharge the documents' functional-correctness arguments; the claimed saving concerns only the stability-map half.Source: §6 · p. 16

Negative controls

  • All listed negative controls fail, including tightened sensitivity and loop bounds, off-by-one constants, under-calibrated releases, and under-provisioned budgets.Rust also rejects aliased exclusive borrows, while the unclamped substitution-metric sum has no rule to invoke.Source: §6 · p. 16

Scope

  • Data-dependent-index writes remain in trusted leaf primitives, while the checked layer handles composition, loops, strong updates, function boundaries, and public-index writes.The checked core rejects loops over sensitive indices because they would branch on secrets.Source: §6 · p. 17

7 Forte by example: OpenDP’s own primitives

The case studies verify OpenDP-style primitive bodies and stability maps in the shapes the library uses, while Polars-based transformations stand apart.

Case-study scope

  • The case studies cover primitive bodies and stability maps, not floating-point relaxation terms or Polars-based transformations.The latter need a model of the query-plan engine.Source: §7 · p. 17

Example 1: the body of the checked sum

  • 7 verified, 0 errors; checked_sum’s overflow precondition discharges the in-range obligation for acc + v[i].The constructor rejects bounds under which the sum could overflow.Source: §7 · pp. 17–18

Example 2: clamp, then sum, run twice

  • 21 verified, 0 errors; self-composition proves the two-run clamp-then-sum outputs differ by at most substituted rows × (hi − lo).The wrapper calls the leaf theorems as its proof.Source: §7 · pp. 18–19

Example 3: a fused body

  • 9 verified, 0 errors; the fused prefix-count constant is 1 per substituted row in L∞ because one substituted row changes one indicator.The two-run claim is per coordinate.Source: §7 · p. 19

Example 4: stability maps as indices

  • A chain’s sensitivity constant is the product of its indices, while OpenDP’s symmetric distance enters once through integer division by 2.The two-run justification composes the parts’ claims.Source: §7 · pp. 19–20

Example 5: constructors and their chain

  • 10 functions processed: 7 checked and 3 trusted; the checker rejects clamp-then-sum’s hi - lo - 1 refinement.The claimed hi − lo constant depends on the two-run theorem for the chain.Source: §7 · p. 20

Example 6: a complete program, from the data to the noisy output

  • The census contract requires ε≥2 and rejects ε=1.5, an age scale of 124, token reuse, and exact release of the age sum.Its two sensitive sums use separate budget tokens; the count has zero sensitivity.Source: §7 · pp. 20–21

Limitations

  • The guarantee excludes stored references, sensitive control flow, overflow, and floating-point rounding, among other stated boundaries.The calculus permits borrows only for a call’s duration; the case studies did not need stored references, closures over sensitive data, or sensitive control flow at the checked layer.Source: §7 · p. 22

8 Related work

Prior systems address sensitivity in pure calculi or imperative programs without references; Forte extends ownership-based reasoning to mutation through Rust borrows.

Sensitivity type systems and imperative analyses

  • Fuzz, DFuzz, Duet, Jazz, and Solo use pure calculi, while imperative analyses update first-order variables without references or aliasing.Forte inherits Solo’s environment-indexed design and moves it to a mutable host.Source: §8 · pp. 22–23

Imperative sensitivity analyses

  • Forte’s related-work distinction is that its theorem handles a second name for a caller’s location at primitive and checked-function boundaries.The theorem identifies borrow ownership as the fact that preserves the frame.Source: §8 · p. 23

Dynamic and hybrid enforcement

  • DDuo and DPella are library-hosted designs; Forte makes sensitivity claims static and checked at calls, while SampCert verifies probabilistic samplers and composition.SampCert is described as a natural replacement for Forte’s trusted sampler.Source: §8 · p. 23

Verification in and of Rust

  • Forte combines Flux refinement inference for mechanism code with Verus proofs, using ownership for a relational quantitative property rather than unary verification.Unlike lattice-valued labels, sensitivity environments require real-valued arithmetic, scaling, and metric-conversion rules.Source: §8 · p. 23

Sensitivity failures in deployed systems

  • OpenDP’s hand-written proof documents address deployed sensitivity claims; Forte checks kernel obligations, including a factor-2 fused/compositional gap.The passage connects that gap to constant drift warned of in Casacuberta et al. [5].Source: §8 · p. 23

9 Conclusion

Forte uses ownership to support sensitivity tracking through Rust mutation, formalizes and mechanizes its soundness argument, and checks OpenDP-style kernels.

Conclusion

  • Forte uses sensitivity environments as refinement indices and strongly updates them through exclusive borrows at primitive calls and checked function boundaries.Borrow exclusivity is the ownership fact consumed by the soundness proof.Source: §9 · p. 24
  • Metric preservation is proved over a store-based semantics; Verus mechanizes the scalar core, function rule, aliased-form refutation, and deterministic primitive obligations.A correspondence theorem transports the guarantee to programs accepted by the checker.Source: §9 · p. 24
  • The case studies match OpenDP stability maps with checked constants, reject several sensitivity and privacy-budget errors, and infer one trusted constant as a loop invariant.Future work includes longer-lived borrows, source polymorphism, and a mechanized privacy layer above affine budget tokens.Source: §9 · p. 24

Data availability statement

The submission provides the library, case-study kernels, specifications, mechanized proofs, survey output, and runnable examples with pinned tool versions.

Data availability statement

  • The artifact includes forte-rs, Flux specifications, Verus developments, an OpenDP proof-obligation survey, and runnable checker examples with expected outputs.Pinned tool versions accompany the materials.Source: Data availability statement · p. 24

A Proofs

The proof establishes metric preservation by induction over evaluation, using relatedness lemmas for primitive operations and a frame argument for calls. Its distinctness premise is necessary: aliased exclusive borrows can leave a stale sensitivity bound that the output store violates.

A Proofs

  • Leaf validity reduces primitive cases to their named theorems; addition combines operand sensitivities, scaling multiplies them, and clamping uses 1-Lipschitzness.The diameter-sum cases bound the result using the number of differing coordinates and the interval width.Source: A Proofs · p. 25
  • The frame lemma preserves relatedness for every location outside a call’s borrowed write set, for both primitive and function calls.For function calls, the body writes only through actual borrowed locations or fresh and renamed locals, which are removed afterward.Source: A Proofs · p. 26
  • Metric preservation follows by induction on the first run’s evaluation, with public data ensuring both runs follow the same rule skeleton and the second run terminates.The mechanized theorem includes termination of the second run in each case.Source: A Proofs · p. 26
  • Variables, assignment, sequencing, conditionals, and loops preserve the relation through store updates, weakening, and lockstep execution under public guards.For loops, induction on the first run’s iteration count uses the invariant context to keep both runs synchronized.Source: A Proofs · p. 26
  • Function-call preservation uses distinct borrowed locations to rename callee locals injectively, apply the body induction hypothesis, and frame all other caller variables.Primitive calls likewise use pairwise distinct borrowed locations so each updated location receives its corresponding post-value.Source: A Proofs · pp. 26–27
  • Aliasing two mutable borrows lets a function double a source value while its output context retains sensitivity 1, although the store distance can reach 2.Thus the output store is not related at the claimed bound, refuting metric preservation without distinctness.Source: A Proofs · p. 27

B The correspondence theorem

The correspondence theorem connects Flux’s refinement-based checking rules to elaborated λ-Forte judgments. Elaboration and semantic agreement let metric preservation for the core calculus transfer to programs accepted by the checker, subject to stated assumptions.

B The correspondence theorem

  • The model assigns sensitive values refined types and uses a flow-sensitive environment; its stated rules govern the checked fragment.The model specifies signature calls, assignments, branches, loops, and function-body checking, including updates to mutable-borrow actuals.Source: B The correspondence theorem · pp. 27–28
  • The signature rule updates each mutable-borrow actual to its ensures refinement, while requiring pairwise-distinct locals and no other live reference during the call.The account identifies Rust’s borrow checker as enforcing these exclusivity conditions.Source: B The correspondence theorem · p. 27
  • The transfer assumes sound solver answers, sound Rust borrow checking, opacity for sensitive values, and unary public refinements shared across related runs.Semantic agreement connects the checker’s refined types to the elaborated metric-related types.Source: B The correspondence theorem · p. 28
  • A refinement’s upper-bound vector becomes the λ-Forte environment, and valid refinement implications yield the pointwise inequalities required by subsumption.For satisfiable refinements, the upper bound satisfies the refinement and bounds every vector satisfying it.Source: B The correspondence theorem · p. 28
  • The correspondence proof elaborates each checker derivation into a λ-Forte derivation, then applies metric preservation to the elaborated program.It handles unsatisfiable refinements only on paths with contradictory public facts, which neither related run takes.Source: B The correspondence theorem · pp. 28–29

C The trusted-base seam, in full

The trusted-signature account pairs library signature families with mechanized obligations and identifies cases whose claims follow directly from relatedness.

C The trusted-base seam, in full

  • Definitional rows require no theorem because their two-run claims follow immediately from relatedness.Examples given are equal constants, source reads, and duplication.Source: C The trusted-base seam, in full · p. 29
  • Table 6 covers every trusted signature family and its mechanized obligation, with 43 verified theorems and supporting lemmas in total.The caption establishes the table’s scope and total.Source: Table 6 · p. 29
  • The table’s stated organization makes the mechanized obligation for each trusted signature family visible alongside the family it covers.The passage identifies the table as listing every family against its obligation.Source: Table 6 · p. 29, C The trusted-base seam, in full · p. 29
Loading 2609.30254v1…