Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)

TL;DR

This paper presents a modular program logic for verifying differential privacy in complex, general-purpose programming languages, enabling formal guarantees for privacy-preserving algorithms with practical implementations.

Contribution

It introduces a new logic with first-class privacy budget reasoning, supporting modular verification of complex DP algorithms and libraries in real-world programming languages.

Findings

Verified a library of differential privacy mechanisms including Sparse Vector Technique

Developed a privacy filter inspired by OpenDP that handles randomization and higher-order functions

All results are formally verified in the Rocq Prover.

Abstract

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.