Proving Differential Privacy via Probabilistic Couplings

TL;DR

This paper introduces compositional verification methods for differential privacy using probabilistic couplings, enabling proofs beyond standard composition theorems, demonstrated on key algorithms with an extended relational logic.

Contribution

It develops a novel verification framework based on probabilistic couplings, extending the apRHL logic to handle more complex privacy proofs for important algorithms.

Findings

Verified privacy of the Exponential mechanism and Above Threshold algorithm

Extended the apRHL logic with new rules for Laplace mechanisms

Provided a coupling-based approach for proofs beyond composition theorems

Abstract

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.