[pl-seminar] Synthesizing Proofs of Differential Privacy

Monday, October 9, 2017 -
12:00pm to 1:00pm
CS 4310

Speaker Name: 

Aws Albarghouthi

Speaker Institution: 

University of Wisconsin - Madison




Differential privacy has emerged as a promising probabilistic formulation of privacy, generating intense interest within academia and industry. We present a push-button, automated technique for verifying ϵ-differential privacy of sophisticated randomized algorithms. We make several conceptual, algorithmic, and practical contributions: (i) Inspired by the recent advances on approximate couplings and randomness alignment, we
present a new proof technique called coupling strategies, which casts differential privacy proofs as discovering a strategy in a game where we have finite privacy resources to expend. (ii) To discover a winning strategy, we present a constraint-based formulation of the problem as solving a set of Horn modulo couplings (hmc) constraints, a novel combination of first-order Horn clauses and probabilistic constraints. (iii) We present a
technique for solving hmc constraints by transforming probabilistic constraints into logical constraints with uninterpreted functions. (iv) Finally, we implement our technique and provide the first automated privacy proofs for a number of challenging algorithms from the differential privacy literature, including Report Noisy Max, the Exponential Mechanism, and the Sparse Vector Mechanism.