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.

翻译：差分隐私是保护隐私的数据分析的标准方法。确保差分隐私算法实现的可靠性具有重要保障，这一共识已催生出形式化方法领域的丰硕研究。然而，现代差分隐私库所采用的设计模式与语言特性，以及库设计者希望建立的保证类别，往往超出了现有验证方法的适用范围。我们提出了一种适用于验证用复杂通用编程语言编写的差分隐私实现的程序逻辑。该逻辑将隐私预算作为分离逻辑资源进行一等支持。该逻辑与目标语言的表现力使我们能够处理差分隐私库实现中常用的编程模式，例如隐私过滤器和缓存。先前的研究主要集中于为领域特定语言编写的程序或孤立的隐私机制提供保证，而我们的逻辑能够模块化地推理原语、高阶组合子以及交互式算法。我们通过实现一个经过验证的差分隐私机制库来展示该方法的实用性，该库包含在线版本的稀疏向量技术，以及受流行Python库OpenDP启发的隐私过滤器——这一实现关键依赖于我们处理随机化、局部状态与高阶函数组合的能力。我们还通过实例化规范来验证库的客户端程序，证明这些规范具有通用性和可复用性。所有结果均在Rocq证明助手中完成了基础性验证。