论文:arXiv:2609.30254v1 ↗ — Forte: A sensitivity type system for imperative Rust, Chiké Abuah, 2026-09-24 代码:artifact 包含 forte-rs 库、Flux spec、Verus 机械化(leaves.rs / calculus.rs)、OpenDP 证明义务调查、notebook

一个差分隐私机制,怎么悄悄地说谎#

如果你在差分隐私(DP)领域做过哪怕一点工程,都会对 sensitivity 这个词保持敬畏。它是整个噪声校准的基石:一个机制输出的最大变化幅度,在邻近数据集之间。机制加 Laplace 噪声,加多少,完全由 sensitivity 决定。

差一个常数,出大事。

少估 1,噪声就少加一点,声称的 ε 就比真实的小,机制的”保护”就会比承诺的弱一档。而且这件事没有任何运行时症状:机制照样跑、输出照样合理、单元测试照样通过——它就是静默地少保护了一个用户。

Casacuberta 等人 2022 年那篇 CCS 论文《Widespread Underestimation of Sensitivity in Differentially Private Libraries and How to Fix It》对部署中的差分隐私库做了一次系统性扫描,结论是:很多库在自己都不知道的情况下低估了 sensitivity。原因五花八门——off-by-one 的直径、把 Lipschitz clamp 错读成 1-sensitivity、metric convention 切换时漏掉 ×2、把累加和的 d 当成元素数而实际是替换数——但共性只有一条:这些常数写在 review 文档里,不在编译器里。

OpenDP 的应对是手写证明文档。109 份,8433 行,38297 词。但它们覆盖了 14 / 68 个可信稳定性闭包;剩下的 54 个,包括所有有界求和变体,全靠代码注释和文献引用撑场。

这并不是”人手不够”的问题,而是结构性的问题:能写出这些常数的类型系统,表达不了部署它们的代码。

纯演算系的天然隔阂#

Fuzz、DFuzz、Duet、Jazz、Solo——这一脉的 sensitivity 类型系统全建在纯 λ 演算上。它们给敏感值挂一个 grade(graded linear types、contextual linear types、environment index 等等),然后证明”一个值带 grade 走过整个程序都不会变”。

这条路漂亮,但有一个隐含前提:值的 grade 是不可变的。

它成立,因为纯演算里值走的是 substitution。值的 grade 跟着值走,值不动 grade 不动。frame 永远成立:你读一个 grade s 的 x,后面读到的还是 x,还是 s,没毛病。

但部署里的 Rust 不这么干。OpenDP 里一个累加器长这样:

let mut acc: Histogram = zero();
for row in rows {
    acc.increment(row.bucket());  // 原地加
}
let noisy = laplace_release(acc, budget);

acc 的 sensitivity 一边跑一边长:从零,到每加一行涨一个 grade,到 loop 结束变成一个非常大的数。纯演算连这个模式都写不出来,因为它根本没有”原地修改”这个动作。

命令式系的那点进步,差了一口气#

LightDP、Fuzzi、CheckDP——把 sensitivity 抬到一阶命令式语言上,变量可赋值(T-Assign 直接 retype),但不允许引用。两个名字永远不会指向同一个 location,所以 frame 还是不需要推论——它来自”没引用”这个事实。

但 Rust 的程序里,helper(&mut acc, &mut data) 这种调用满天飞。借给 callee 的 &mut acc,本质上是 caller 那块 location 的另一个名字。callee 在 callee 的世界里写它,然后 callee 退出,这块 location 又回到 caller。写之前它带一个 sensitivity,写之后带另一个——这就是 frame 该推论的真正内容。

而这些命令式系没法表达这个动作,更别说证明它了。

Forte 的洞察:一个事实就够#

Abuah 写的 Forte 找到的那个点,是 Rust 类型系统里早就摆在那儿的一个事实:&mut 是排他的。

只要你相信”在 &mut x 还活着的时候,没有别的 &mut x 存在”,你就同时拿到了两件事:

1. 强更新:location 走完 callee 之后,新的 grade 就是 callee 写在签名 ensures 里的 grade,旧 grade 在 caller context 里被覆盖。
2. Frame:这个 location 是独有的,callee 写的就只是这个 location,不会写到 caller 还活着的别的视图里去。

这两个加在一起,就足以支撑所有”在 mutating 上下文里证明 sensitivity 不会崩”的工作。其余的所有结构性约束——纯净、线性、别名敏感——在 sensitivity 层全部不需要。weakening、contraction、exchange,三条结构规则全部成立。

而 &mut 的排他性是 Rust 的 borrow checker 在编译期就保证的。Forte 直接把”distinctness of borrowed actuals”这条前提外包给 rustc,自己的类型系统反而少干活。

一句话:Forte 收紧的不是”在 sensitivity 上加什么”,而是”在 sensitivity 上最少需要什么”。

这张图把这条主线画清楚了。每一列往右,都是把一类结构性假设甩掉;Forte 这列只剩一个事实。

一个反例:双重读为什么安全,双重写为什么崩#

“aliasing 对 soundness 无害”这种直觉其实只对了一半。

读 alias 是无害的。考虑下面这段,x 被读了两次,结果 environment 是 2·α,刚好把”读了两遍”这件事计进结果里:

// sound
fn add_assign(acc: &mut SInt[@α], x: SInt[@α]) {
    *acc = *acc + x;  // read x once, plus read *acc, write *acc
}

写 alias 是灾难。考虑这段:

// unsound
fn double_into(p: &mut SInt[@α], q: &mut SInt[@β])
    ensures p : SInt[@(α+β)],
              q : SInt[@β]   // ← q 没动,所以保留 β
{
    *p = *p + *q;
}

如果你拿同一个 x 同时当 p 和 q 调它——double_into(&mut x, &mut x)——会发生什么?

• p := p + q 在 p 和 q 是同一个 location 时,变成 x := x + x = 2·x。
• 但 type checker 的 output context 里有 q : SInt[@β],也就是 x : SInt[@β]。
• 真实情况是两次 run 之间 x 最多差 2α;如果 β < 2α(比如 α=β=1,声明”x 最多差 1”,实际”x 最多差 2”),frame 破裂,声明错。

Forte 没有靠”运行时检测”或”运行时不变性”来挡这一类。它把这一类外包给 rustc——&mut x 同时活两次,这是借用检查器的错误,根本到不了 type checker。

唯一区别:左边的两个名字是”读视角”,右边的两个名字是”写视角”。索引算术会把前者计进结果(contraction 的合法计价),但计不了后者的写能力碰撞——两个 ensures 撞同一 location,而 environment 是关于 location 的声明,不是关于名字的声明。

这一条边界,把 Forte 和 Fuzz 系/Solo 系区分开:Forte 知道什么叫”写”。

𝜆-Forte:把这一切形式化#

Abuah 在 §3 给出了一个一阶的、带 store 的核心演算 𝜆-Forte。它只有这些构造:

• pub B:公开基类型,base types 不带 sensitivity
• S[®s]:标量敏感类型,environment 是个 k 维向量
• Vec L1[®s]、Vec Sub[lo, hi, ®s]、Vec L∞[®s]:三种向量类型,对应元素 L1 距离、替换行计数、L∞ 距离
• &x / &mut x:共享/排他借用
• 函数可以收 &mut 参数,签名带 ensures 子句描述借用参数出来时的新 environment

类型规则里最关键的两条是 T-CallMut 和 T-CallFn:

T-CallMut  (primitive call through &mut):
  Σ(p) = ∀α. (&mut τ1..τn, τ'1..τ'm) → τ ensures xj : τout_j
  σ instantiates α
  Γ(zj) = στj   (j ≤ n)
  z1..zn pairwise distinct    ← 排他性前提
  Γ ⊢ ai : στ'i ⊣ Γ          (i ≤ m)
  ─────────────────────────────────────
  Γ ⊢ p(&mut z1, .., &mut zn, a1, .., am) : στ ⊣ Γ[zj ↦→ στout_j]

T-CallFn   (declared function through &mut):
  和 T-CallMut 形状一致,只是 Σ 换成 Φ,callee 的 body 已被 WF-Fn 一次过 type-check

两条规则的形状完全一样——这就是 Forte 的关键洞察:primitive 上的强更新和函数上的强更新,在类型规则层面是同一种东西,只是签名层来源不同。一个来自 trusted 库,一个来自 checked 函数。

soundness 定理 (Theorem 4.2,Metric Preservation)说的是:如果 Γ ⊢ e : τ ⊣ Γ',且两次 run 的输入 stores 是 “related at Γ”(每对变量满足 sensitivity 上界),那么两次 run 的输出 stores 也 “related at Γ’”。

证明分三个核心引理:

• Lemma 4.4 (Frame):一次调用只写它声明要写的 location,别的 location 一字不动
• Lemma 4.5 (Strong update):排他性保证了 distinctness 的 location 收到的就是 Lemma 4.3 给出的 post-value
• Lemma 4.7 (Function call):把 callee 的 typing derivation 通过 substitution 运到 caller 这里;只有当 substitution 在借用参数上是 injective 的时候才合法——这恰恰是 T-CallFn 的 pairwise distinctness 前提

整篇证明消耗 distinctness 前提的次数,只有两次:Lemma 4.5 和 Lemma 4.7,没有第三处。

这张图把 caller → T-CallFn → callee body → store → output context 的链路画出来了,红色标的就是 distinctness 关键前提——它穿过 Lemma 4.6(renaming 需要 injectivity)、Lemma 4.5(强更新需要 distinctness)、Lemma 4.4(frame 需要知道哪些 location 没被碰)三个地方,撑住了整条链。

反证也写在 Verus 里#

Lemma 4.5 / 4.7 真的需要 distinctness 吗?拿掉它,定理就不成立。作者在 Verus 里把这个反证机械化:aliased_call_refutation 声明 double_into,证明其签名是 well-formed,然后展示同一份代码在 alias 调用下,输出 stores 不再 related at output context——也就是 Theorem 4.2 的结论破了。

这个反证的存在,反过来确认:distinctness 是 soundness 的最小前提,而不是一个工程上够用的强假设。

forte-rs:不开 fork 的实现#

𝜆-Forte 是纸上的演算;forte-rs 是跑在 flux 上的 Rust 库。

关键约束:Forte 不能改 flux。flux 是 LLVM-Rust 项目,2019 年起就在做 refinement type for Rust,有自己的论文(Lehmann et al. PLDI’23、Lehmann et al. POPL’25),有自己的 release cadence 和 fixpoint engine。Forte 之所以叫 Forte,是因为它把所有 sensitivity 逻辑都装进一个库,forte-rs 是一个普通 Cargo crate,编译走 rustc,验证走 flux。

编码表#

最有意思的是 #[opaque] + 3-tuple refinement index 这个组合:

#[opaque]
#[refined_by(sa: int, sb: int, sc: int)]
pub struct SInt { v: i64 }  // v 对 checker 不可见

// 签名里的 ensures
#[spec(fn(acc: &mut SInt[@av], data: &SVec[@s], lo: i64, hi: i64{lo <= hi})
       ensures acc: SInt[av.a + (hi-lo)*s.sa,
                          av.b + (hi-lo)*s.sb,
                          av.c + (hi-lo)*s.sc])]
pub fn add_clamped_sum(acc: &mut SInt, data: &SVec, lo: i64, hi: i64) { ... }

3-tuple 这个选择看着武断,但有两个强约束:

1. SMT-friendly:整个 environment 的算术是线性、可判定,flux 能推断 loop invariant
2. 解耦:不同源的 metric 各自独立 — 第一个源是 age,第二个是 income,第三个是性别 — 三个坐标,不必绑死

库实例化了三个源,每个 kernel 都装得下。要更多源就重新生成类型。作者明确说:“map-sorted index 在原则上能 lift 这个限制,但需要 quantify 整个 SMT 数组 — 线性可判定这条命根子就丢了”。

两层 index sort 的取舍#

flux 的 refinement sort 不统一:real 和 int 各自封闭,中间没有 cast。

这强迫做了一个实际选择:所有涉及运行时值(loop count, runtime-int)的 bound 必须用 int sort,把所有常量化合(纯字面量,没有循环)留给 real sort。前者用 scaled rational 表示,i64 自动 lift。后者直接做线性算术。

副作用:L2 类的 bound(需要 sqrt)进不来 — refinement grammar 没 sqrt,sum-of-squares 那条规则就只能做”半径式过估”,而不是真实 L2 norm。这个限制 §5 第二段明确说出来了。

Theorem 5.1:把 flux 接回 𝜆-Forte#

flux 的 soundness 是一元的:被接受的程序在单次 run 上满足 refinement。sensitivity 是关系的:两次 run 之间的差。没有任何一元 statement 能推出关系性。

Abuah 没试图让 flux 提供 metric preservation — 他写了一个 Theorem 5.1,叫 Correspondence,把 flux 接受的程序对应回 𝜆-Forte 的 ok 程序。

定义上需要固定一个 fragment F:refinement 是 per-coordinate atom 的合取(v.i ≤ e / v.i ≥ e / v.i = e,e 是 public 表达式),每个坐标至少有一个上界。每个 case-study kernel 都在 F 里。

elaborate 一个 refinement φ 到 𝜆-Forte 的方式很自然:把每个坐标的上界取最小值,组成一个 environment tuple。

Lemma B.1 (Maximum):  satisfiable 的 φ 在每个坐标上 satisfy 自己的上界
Lemma B.2 (Implication elaborates):  φ ⇒ ψ valid ⟹ ub(φ) ≤ ub(ψ) pointwise
Lemma B.3 (Semantic agreement):  两个值 related at any env satisfying φ ⟺ related at ub(φ)

Theorem 5.1 的证明是对 flux 的 model derivation 做归纳,每条规则映射到 𝜆-Forte 的同名规则:唯一的非平凡引理是 B.2——SMT 的 implication 翻译成 λ-Forte 的 pointwise environment 不等式。

四个 flux 公开特性是这个定理的全部前提:

1. opacity:只有签名和 subtyping 约束 opaque type 的 refinement
2. solver implication:subtyping 是 implication,solver 决定
3. &mut ensures:flux 更新 &mut 参数到 ensures 类型(这直接复用,T-CallMut/T-CallFn 不需要扩展 flux)
4. inferred loop invariant:loop 在推断的 invariant 下检查,branch 用公共 weakening join

作者坦白:“这是 flux 公开特性的总结,不是 flux 完整语义的证明”——把 flux 全文重证明一遍是未来工作。

信任根基,从一层变两层#

之前的 sensitivity 类型系,信任根基是一层:库自己。Fuzz/Solo 信任自己的 primitive 库;Duet/Jazz 把库切两半。Forte 是两层的:

• 外层(flux-checked layer):mechanism 作者写代码的层 — kernel / composer / 强更新 / loop invariant — 131 行 kernel、0 个 #[trusted]
• 内层(Verus-mechanized layer):每次 change 都要重新过定理检查的层 — 43 个 leaf 定理 + 46 个 calculus item + Theorem 4.2 + 反证——452 行 leaf 实现,313 行 trusted primitive body,每个 #[trusted] 签名 cite 一个 Verus 定理

中间是 Theorem 5.1 (Correspondence)——一个金桥,把外层的 flux 接受映射回内层的 𝜆-Forte ok。

举几个 leaf 家族为例:

这就是论文最关键的一招:leaf 层的每一个 primitive 签名,背后都背一个 Verus 机械化定理——库不再是”信任 primitive”,而是”每个 primitive 都对应一个可重新验证的证明”。

OpenDP 那个 109 份手写证明文档、8433 行的体量,Forte 用 131 行 kernel + 452 行 leaf + 2 个 loop hint 替代了。比 OpenDP 的 stability map 那一半(文档共 769 行手算)少一个数量级,而且是 checked obligation 不是经验。

OpenDP 实战:从 109 篇文档到 131 行 checked kernel#

§6 是 case studies——把 OpenDP 的 transformation kernel 重新实现成 forte-rs 代码,然后让 flux 检查。

7 个 kernel 全在 F fragment 里,0 个 #[trusted]:

两个有意思的细节:

细节 1:fused vs composed 差一倍

quantile prefix counts 同一个向量可以走两条路 — 一条 fused,直接对每个候选数 ”≤ candidate” 的行数;一条 composed,先做 histogram 再 prefix sum。Forte 两条都接受,fused 出 1 per row,composed 出 2 per row。OpenDP 自己用的是 fused,但其稳定性闭包用 compositional 推导会付出一倍的常数。

这个 2x 漂移正是 Casacuberta et al. 报告里反复出现的”偶发敏感性低估”模式。Forte 把两条路都做成 theorem-backed signature,任你用,常数不会糊弄。

细节 2:b-ary tree 的 trusted constant 变 inferred invariant

OpenDP 的 b_ary_tree 把 num_layers 作为 stability constant,代码注释里写着”每个输入元素贡献到每一层的一个节点”,靠 review 推理,没有 proof document。

Forte 写这个 kernel 时,loop 一层层构造 tree,每层做一次 chunked sum(partition 保持 L1 环境),每次 append 通过 &mut 强更新累加一层环境。flux 自己推断出 loop invariant:累积的 environment 上界 ≤ loop counter。

就这两个 qualifier hint(a ≤ i 和 a ≤ 1,作者 ablation 验证过最小),flux 解出 invariant。这就是 §1 摘要里那句”derives one trusted constant as an inferred loop invariant”——OpenDP 文档里靠人脑保证的常数,在 Forte 这边是 type checker 推出来的。

负面控制:type checker 抓的 bug 类型#

每个 kernel 都做了”故意改坏”的实验,Forte 全部拒绝:

• clamp ∘ sum 写成 1-sensitivity(Lipschitz 误读)
• fused quantile 写成 0-sensitivity
• loop bound 从 100n 收到 99n
• b-ary 写成 layers − 1
• sum-of-squares 直径 15625 写成 15624(off-by-one)
• count by categories 写成 1 per row
• helper 的 ensures 漏一个 diameter
• release noise scale 124 写成 125 用的 124(校准不足)
• budget split 1,999,999 micro-ε 写成 2·10⁶(预算不够)
• weekday bound 收到 n − 1

两个根本到不了 refinement checker 的程序:double_into(&mut x, &mut x) 被 rustc 直接拒(&mut 借用错误);无界向量的求和没有规则可调 — bug class 直接无表达,不可表达即不可引入。

一份完整的程序:从数据到噪声输出#

§7 把这一切装进一个 end-to-end 例子。一张两人口表,两列(ages / incomes)都来自 source a,所以一个替换的个体改这两列的各一行。程序释放行数、年龄总和、收入总和,总预算 ε=2。

#[spec(fn(ages: &SVec[@(1,0,0)], incomes: &SVec[@(1,0,0)],
            budget: {Budget[@bv] | bv.eps >= 2_000_000}, seed: u64)
        -> (i64, i64, i64))]
pub fn census_release(ages: &SVec, incomes: &SVec,
                      budget: Budget, seed: u64) -> (i64, i64, i64) {
    let n = SVec::count(ages);                          // SInt[(0,0,0)]
    let n_public = release_insensitive(n);              // 精确释放
    let (b_ages, b_incomes) = Budget::split(budget, 1_000_000);
    let age_sum = sized_bounded_sum(ages, 0, 125);      // SInt[(125,0,0)]
    let noisy_age_sum =
          laplace_release_a(age_sum, b_ages, 125, seed); // SInt[(2·10^5,0,0)]
    let income_sum = sized_bounded_sum(incomes, 0, 200_000);
    let noisy_income_sum =
          laplace_release_a(income_sum, b_incomes, 200_000, seed + 1);
    (n_public, noisy_age_sum, noisy_income_sum)
}

这个 signature 就是隐私合约。 把它一行行读:

• &SVec[@(1,0,0)]:一列在 row-substitution metric 下的向量,index 是 sensitivity environment,一坐标一源。index 写明一个替换行最多改这一列一行,源 b / c 不能动它。
• 两列 index 相同,因为我只有 from_source_a 一种方式产出这个类型的值 — 这是程序对”它保护什么”的声明。
• Budget[@bv] 把 token 的大小绑进类型,bv.eps ≥ 2·10⁶ — 小于这个的 token 编译不过。
• Budget 不是 Copy,所以 token 是 move-only 进函数,caller 不能复用。
• seed 是 public,epsilon-calibration 内部用。
• 返回类型是三个没有 index 的 i64 — 输出离开了 sensitivity 域。从 sensitive 到 i64 只有两条路:laplace_release_a(必须有 token 且 scale 校准)或 release_insensitive(环境必须是 0)。

这张图画了六种节点:输入数据 → 两个 SVec → 两个 bounded sum → budget split → 两个 laplace release → 输出。每条边的箭头颜色对应数据流类型(绿 sensitive / 金 release / 红 i64 输出)。最关键的对比在右下角:count 走的是 release_insensitive,因为它的环境是 (0,0,0)——count 对 sized data 是不敏感的。

flux 拒绝四种编辑:

1. 𝜀 = 1.5 的 contract,导致第二个 release 预算不够
2. ages 的 scale = 124(scale 必须 ≥ sensitivity)
3. 一个 token 给两个 release(Budget 不 Copy,move 后失效)
4. 把 age_sum 传给精确 release — release_insensitive 的参数类型只接受 (0,0,0) 环境

全部是 compile-time error,没有任何运行时检测。

Verus 那一层:release 背后的隐私证明#

laplace release 的 side condition 不是一句空话。release 之所以真的能 release,靠的是 14 个 Verus verified item 的算术:

Laplace 在 scale b 下的密度正比于 exp(-|k|/b),所以在任一输出 y 处两次 run 密度的比是 exp((|y−f₂|−|y−f₁|)/b)。对数是隐私损失,等于 (|y−f₂|−|y−f₁|)/b。在 side condition (ε ≥ Δ/b) 下,损失处处 ≤ ε,反向三角不等式即可;两次独立 release 损失相加;一个权重上的 pointwise ratio bound 是它们在任何输出集合上求和的 ratio bound;census 程序两次 release 总损失 ≤ ε = 2。

这些是 Verus 一行行过完的。“我们仍然信任 sampler 从那个密度采样,exp 单调,把损失 bound 转成密度比 bound” — 这条尾巴上还是有人脑推理,但已经是 DP 定义本身的事实,不是库的实现细节。

还剩什么#

§9 的 Limitations 列得很坦白:

• 演算只接受调用期间活的借用,不接受跨调用的 long-lived borrow、不接受存进数据结构的引用、不接受闭包捕获敏感数据、不接受敏感数据驱动的控制流。
• case study 不需要前三,第四个就是为什么 data-dependent 索引的 element 写入必须是 leaf,不是用户级 checked 代码。
• 算术被理想化,整数 unbounded,实数 exact,overflow 和浮点 rounding 在保证之外。OpenDP 自己的 checked / saturating sum 变体是”信任的 additive 层”。
• source 集合是固定的 — 库实例化在 3,其它宽度要重新生成类型。
• 涉及 loop count 的 bound 必须用 int sort,√ 进不来,L2 类 bound 只能做过估。
• 机械化只覆盖 scalar fragment,procedures 必须参数全是 borrow,body 只引用自己的参数。vector / by-value / 多态 scheme 还是纸面证明。
• Theorem 5.1 依赖 flux 的4 条公开特性,不重新证明 flux 全文。
• 概率层 — sampler 和 exp 单调 — 还信,SampCert(PLDI’25)是自然的替代。
• Polars 那 31 / 68 个 stability map 需要 Polars 引擎的 model。

从”sensitivity 是经验”到”sensitivity 是类型”#

Abuah 在 Conclusion 那段话我反复读了三遍:

We have presented Forte, a sensitivity type system for Rust whose soundness rests on ownership: sensitivity environments are refinement indices, strong updates flow through exclusive borrows at primitive calls and across checked function boundaries, and the soundness proof consumes one ownership fact, borrow exclusivity.

把这件事说回 OpenDP 那 109 份手写证明文档、8433 行、38297 词 — Forte 用两个数量级少的代码(131 kernel + 452 leaf + 2 hint)替代 stability-map 这一半的证明,做到的不是”自动化 review”,而是把 sensitivity 这个性质从经验事实变成编译期类型。

机制作者不再需要记住:

• OpenDP 的 d 是 symmetric distance,sized data 上 ×2 per substituted row
• 替换和 add/remove 的 metric 切换在哪一步
• clamp 直径和 Lipschitz 1-sensitivity 的区别
• sum-of-squares 的半径式过估怎么放进 stability map
• histogram 一进一出 bucket +2 的 2x 漂移
• budget split 必须 move-only,scale 必须 ≥ sensitivity

这些全在类型里。

我读完这篇论文最深的感受不是技术细节,而是一种研究姿态的判断:在已有类型系统上面加 sensitivity 看似顺理成章,但真正难的是承认”我需要的最少假设是什么”。Forte 给出的答案是 &mut 排他性,加上 rustc 的借用检查器,加上 flux 的 &mut ensures 子句,加上一个 correspondence 定理把这个组合接回形式化语义——其余的全是副产品。

回到 §1 那个让人后背发凉的现实:差分隐私机制悄悄说谎,不是因为作者不在乎,是因为没有人能在 review 时枚举所有错误。类型系统不会漏掉 off-by-one,因为它根本不接受这类声明存在。

参考资料#

• Abuah (2026). Forte: A sensitivity type system for imperative Rust. arXiv:2609.30254v1
• Casacuberta, Shoemate, Vadhan, Wagaman (2022). Widespread Underestimation of Sensitivity in Differentially Private Libraries and How to Fix It. ACM CCS
• Reed & Pierce (2010). Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy. ICFP — Fuzz 的起点
• Near, Darais, Abuah, et al. (2019). Duet: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy. OOPSLA
• Toro, Darais, Abuah, Near, et al. (2023). Contextual Linear Types for Differential Privacy. TOPLAS — Jazz
• Abuah, Darais, Near (2022). Solo: A Lightweight Static Analysis for Differential Privacy. OOPSLA
• Lehmann, Geller, Vazou, Jhala (2023). Flux: Liquid Types for Rust. PLDI
• Lehmann, Kurashige, Akiti, Krishnakumar, Jhala (2025). Generic Refinement Types. POPL
• Lattuada, Hance, Cho, et al. (2023). Verus: Verifying Rust Programs using Linear Ghost Types. OOPSLA
• Zhang, Roth, Haeberlen, Pierce, Roth (2019). Fuzzi: A Three-Level Logic for Differential Privacy. ICFP
• de Medeiros, Naveed, Lepoint, et al. (2025). Verified Foundations for Differential Privacy. PLDI — SampCert
• The OpenDP Team (2026). The OpenDP Library. https://github.com/opendp/opendp ↗

如果你读完想动手,Forte 的 artifact 在 arXiv 页面挂着 — forte-rs 库、Flux spec、Verus 发展(leaves.rs / calculus.rs)、OpenDP 证明义务调查,以及一个 notebook 跑 §7 全部例子。最快 5 分钟把 census_release 跑起来看 flux 怎么拒掉你那 4 类坏编辑。