Fri 12 Jan 2018 14:05 - 14:30 at Watercourt - Probability Chair(s): Lars Birkedal

In this paper, we present a push-button, automated technique for verifying $\epsilon$-differential privacy of sophisticated randomized algorithms. We make a range of conceptual, algorithmic,and practical contributions: (1) 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. (2) 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 kind of constraints combining first-order Horn clauses with probabilistic constraints. (3) We present a technique for solving HMC constraints by transforming probabilistic constraints into logical constraints with uninterpreted functions. (4) Finally, we implement our technique and provide the first automated proofs of a number of algorithms from the differential privacy literature, including Report Noisy Max, the Exponential Mechanism, and the Sparse Vector Mechanism.

Fri 12 Jan

 13:40 - 15:20: Research Papers - Probability at Watercourt Chair(s): Lars Birkedal 13:40 - 14:05Talk Proving expected sensitivity of probabilistic programs 14:05 - 14:30Talk Synthesizing Coupling Proofs of Differential Privacy 14:30 - 14:55Talk Measurable cones and stable, measurable functions 14:55 - 15:20Talk Denotational validation of higher-order Bayesian inference