一句话：提出概率高阶分离逻辑，将隐私预算作为分离逻辑资源，模块化验证通用语言中的差分隐私实现。
差分隐私是隐私保护数据分析的标准方法，但现代差分隐私库使用的设计模式与语言特性，以及库设计者希望建立的保证，常超出既有验证方法的范围。本文提出一种程序逻辑，用于验证以复杂通用语言编写的差分隐私实现，其核心创新是将隐私预算作为一等的分离逻辑资源，从而支持对原语、高阶组合子与交互式算法的模块化推理。该逻辑可处理隐私过滤器、缓存等常见库实现模式。作者在 Rocq 证明助手中机器验证了一个差分隐私机制库，包括在线 Sparse Vector Technique 和受 OpenDP 启发的隐私过滤器，并将规约实例化以验证库客户端，表明规约具有通用性与可复用性。
Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially private algorithms is widely recognized and has sparked fruitful research on formal methods. However, the design patterns and language features used in modern DP libraries as well as the classes of guarantees that the library designers wish to establish often fall outside of the scope of previous verification approaches. We introduce a program logic suitable for verifying differentially private implementations written in complex, general-purpose programming languages. Our logic has first-class support for reasoning about privacy budgets as a separation logic resource. The expressiveness of the logic and the target language allow our approach to handle common programming patterns used in the implementation of libraries for differential privacy, such as privacy filters and caching. While previous work has focused on developing guarantees for programs written in domain-specific languages or for privacy mechanisms in isolation, our logic can reason modularly about primitives, higher-order combinators, and interactive algorithms. We demonstrate the applicability of our approach by implementing a verified library of differential privacy mechanisms, including an online version of the Sparse Vector Technique, as well as a privacy filter inspired by the popular Python library OpenDP, which crucially relies on our ability to handle the combination of randomization, local state, and higher-order functions. We demonstrate that our specifications are general and reusable by instantiating them to verify clients of our library. All of our results have been foundationally verified in the Rocq Prover.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{HaselwarterAGLT26,
title = {Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic},
author = {Philipp G. Haselwarter and Alejandro Aguirre and Simon Oddershede Gregersen and Kwing Hei Li and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808311}
}