The Complexity of Verifying Boolean Programs as Differentially Private
arXiv:2309.04642 · doi:10.1109/CSF54842.2022.9919653
Abstract
We study the complexity of the problem of verifying differential privacy for while-like programs working over boolean values and making probabilistic choices. Programs in this class can be interpreted into finite-state discrete-time Markov Chains (DTMC). We show that the problem of deciding whether a program is differentially private for specific values of the privacy parameters is PSPACE-complete. To show that this problem is in PSPACE, we adapt classical results about computing hitting probabilities for DTMC. To show PSPACE-hardness we use a reduction from the problem of checking whether a program almost surely terminates or not. We also show that the problem of approximating the privacy parameters that a program provides is PSPACE-hard. Moreover, we investigate the complexity of similar problems also for several relaxations of differential privacy: Rényi differential privacy, concentrated differential privacy, and truncated concentrated differential privacy. For these notions, we consider gap-versions of the problem of deciding whether a program is private or not and we show that all of them are PSPACE-complete.
arXiv commentAppeared in CSF 2022
References in corpus (11)
- Renyi Differential Privacy
- Detecting Violations of Differential Privacy
- Proving Differential Privacy via Probabilistic Couplings
- LightDP: Towards Automating Differential Privacy Proofs
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
- Proving differential privacy in Hoare logic
- Synthesizing Coupling Proofs of Differential Privacy
- CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
- Guidelines for Implementing and Auditing Differentially Private Systems
- Bisimilarity Distances for Approximate Differential Privacy
- The Sparse Vector Technique, Revisited