Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SuperDP: Differential Privacy Refutation via Supermartingales

Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Đorđe Žikelić

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 $ε$-DP. Our method refutes $ε$-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 $ε$-DP refutation. To the best of our knowledge, our method is the first method for $ε$-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 $ε$-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.

SuperDP: Differential Privacy Refutation via Supermartingales

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 -DP. Our method refutes -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 -DP refutation. To the best of our knowledge, our method is the first method for -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 -DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.

Paper Structure

This paper contains 23 sections, 4 theorems, 15 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Overview
  3. Preliminaries
  4. Probabilistic Programs
  5. Differential Privacy
  6. Sound and Complete Proof Rule for Differential Privacy Refutation
  7. Background: Expectation Supermartingales and Submartingales
  8. Proof Rule for Differential Privacy Refutation
  9. Automated Algorithm for Differential Privacy Refutation
  10. Experimental Evaluation
  11. Experimental Setup
  12. Benchmarks and Setup
  13. Results
  14. Related Work
  15. Conclusion
  16. ...and 8 more sections

Key Result

theorem 1

Let $\pCFG = (\locs,\pvars,\Vout,\locinit,\thetainit,\transitions,\guards,\updates)$ be an a.s. terminating pCFG, $I$ be an invariant in $\pCFG$, $f\colon \R^{\pvars_\out} \to \R$ be a Borel-measurable function over the outputs in $\pCFG$, $U_f$ be an UESM for $f$ and $L_f$ be an LESM for $f$. If th

Figures (3)

  • Figure 1: Our two running examples for illustrating our approach to refuting $\epsilon$-DP. In both cases, we use Input to denote the predicate that defines possible program inputs, Sim to denote the similarity relation over inputs, and $\textsc{Out}$ to denote output program variables.
  • Figure 2: Details of RR-2 and PrivBernoulli benchmarks of Section \ref{['sec:experiments']}
  • Figure 3: Details of lowprob and geometric benchmarks of Section \ref{['sec:experiments']}

Theorems & Definitions (21)

  • Example 1: Running example: Randomized response mechanism
  • Example 2: Running example: Histogram mechanism
  • Example 3
  • Example 4
  • definition 1: Differential privacy Dwork06DworkR14
  • Remark 1
  • definition 2: Upper expectation supermartingale ChatterjeeGNZ24
  • definition 3: Lower expectation submartingale ChatterjeeGNZ24
  • definition 4: OST-soundness ChatterjeeGNZ24
  • theorem 1: Soundness of U/LESMs ChatterjeeGNZ24
  • ...and 11 more