SuperDP: Differential Privacy Refutation via Supermartingales

TL;DR

SuperDP introduces an automated, sound, and semi-complete method for refuting differential privacy by leveraging supermartingales, applicable to complex stochastic mechanisms, and demonstrates superior performance over existing techniques.

Contribution

The paper presents the first fully automated, sound, semi-complete method for refuting epsilon-DP using supermartingales, applicable to both discrete and continuous distributions.

Findings

SuperDP outperforms previous methods on challenging examples.

It successfully refutes epsilon-DP in cases previously out of reach.

The method is applicable to stochastic mechanisms with sampling from various distributions.

Abstract

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.