This program is tentative and subject to change.

Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of $\epsilon$-DP. Our method refutes $\epsilon$-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for $\epsilon$-DP refutation. To the best of our knowledge, our method is the first method for $\epsilon$-DP refutation to offer the following four desirable features: (1)~it is fully automated, (2)~it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3)~it provides soundness guarantees, and (4)~it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute $\epsilon$-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.

This program is tentative and subject to change.

Thu 18 Jun

Displayed time zone: Mountain Time (US & Canada) change

13:40 - 15:00
Formal Verification of Probabilistic ProgramsPLDI Research Papers at Flatirons 3
13:40
20m
Talk
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
PLDI Research Papers
Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
DOI
14:00
20m
Talk
Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
PLDI Research Papers
Satoshi Kura Waseda University, Hiroshi Unno Tohoku University, Takeshi Tsukada Chiba University
DOI
14:20
20m
Talk
SuperDP: Differential Privacy Refutation via Supermartingales
PLDI Research Papers
Krishnendu Chatterjee IST Austria, Ehsan Kafshdar Goharshady IST Austria, Đorđe Žikelić Singapore Management University
DOI
14:40
20m
Talk
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
PLDI Research Papers
Philipp G. Haselwarter Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen CISPA Helmholtz Center for Information Security, Kwing Hei Li Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
Link to publication DOI Pre-print