AI 中文总结
Forte 是一个基于所有权机制的 Rust 敏感性类型系统，通过独占借用强更新敏感性环境，实现差分隐私程序的度量保持，并已通过 Verus 验证和 Flux 集成，在 OpenDP 机制内核上成功应用。
AI 中文摘要
我们介绍了 Forte，一个针对 Rust 的敏感性类型系统，其可靠性建立在所有权机制之上。从 Fuzz 的线性分级到 Solo 的环境索引，这些分级敏感性类型系统都是纯演算：对某个值的声明在其整个生命周期内都成立，因为没有任何操作可以修改它。命令式敏感性分析允许对一阶变量进行赋值，但不允许引用，因此在这些分析中不会出现别名问题。实际部署中计算差分隐私统计的程序是用 Rust 编写的，它们通过借用进行修改。Forte 弥补了这一差距。其核心规则通过独占借用、在原始调用处以及跨经过检查的函数边界，强更新敏感性环境；其可靠性定理是在带有存储的操作语义上的度量保持，其中仅凭 &mut 的独占性就允许跨修改调用进行框架化，而两个别名借用足以在没有该独占性的情况下反驳该定理。Verus 对该定理、函数规则及反驳进行了机械化验证。Flux 将 Forte 作为普通库进行检查，无需分叉编译器；每个确定性原始签名背后都有机器检查的定理支持，一个对应定理将度量保持性传递到检查器所接受的程序。我们在来自 OpenDP 的机制内核上评估了 Forte，这些内核具有真正的原地修改，用检查过的常量匹配库的可信稳定性映射，覆盖了没有证明文档的构造函数，拒绝了差一错误（off-by-one）的直径、收紧的界限、校准错误的发布以及超支的预算，并推导出一个可信常量作为推断出的循环不变量。
英文摘要
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.
Comments29 pages. Submitted to the Journal of Functional Programming
