Proving Differential Privacy via Probabilistic Couplings
This provides a new verification approach for the differential privacy community, addressing a specific bottleneck in proving privacy for complex algorithms.
The paper tackles the problem of formally verifying differential privacy for algorithms that cannot be analyzed using standard composition theorems, by developing compositional methods based on probabilistic couplings, and demonstrates this on the Exponential mechanism and Above Threshold algorithm, verifying them in an extended relational program logic apRHL+.
In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based on the observation that differential privacy has deep connections with a generalization of probabilistic couplings, an established mathematical tool for reasoning about stochastic processes. Even when the composition theorem is not helpful, we can often prove privacy by a coupling argument. We demonstrate our methods on two algorithms: the Exponential mechanism and the Above Threshold algorithm, the critical component of the famous Sparse Vector algorithm. We verify these examples in a relational program logic apRHL+, which can construct approximate couplings. This logic extends the existing apRHL logic with more general rules for the Laplace mechanism and the one-sided Laplace mechanism, and new structural rules enabling pointwise reasoning about privacy; all the rules are inspired by the connection with coupling. While our paper is presented from a formal verification perspective, we believe that its main insight is of independent interest for the differential privacy community.