2026-08-06T22:56:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12536 2024-03-12T11:57:07Z ddc:004 open_access

The Complexity of Verifying Loop-Free Programs as Differentially Private Gaboardi, Marco Nissim, Kobbi Purser, David differential privacy program verification probabilistic programs We study the problem of verifying differential privacy for loop-free programs with probabilistic choice. Programs in this class can be seen as randomized Boolean circuits, which we will use as a formal model to answer two different questions: first, deciding whether a program satisfies a prescribed level of privacy; second, approximating the privacy parameters a program realizes. We show that the problem of deciding whether a program satisfies ε-differential privacy is coNP^#P-complete. In fact, this is the case when either the input domain or the output range of the program is large. Further, we show that deciding whether a program is (ε,δ)-differentially private is coNP^#P-hard, and in coNP^#P for small output domains, but always in coNP^{#P^#P}. Finally, we show that the problem of approximating the level of differential privacy is both NP-hard and coNP-hard. These results complement previous results by Murtagh and Vadhan [Jack Murtagh and Salil P. Vadhan, 2016] showing that deciding the optimal composition of differentially private components is #P-complete, and that approximating the optimal composition of differentially private components is in P. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Marco Gaboardi and Kobbi Nissim and David Purser 2020 Is Part Of LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2020.129 urn:nbn:de:0030-drops-125362 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.129 eng https://creativecommons.org/licenses/by/3.0/legalcode