Document Open Access Logo

The Complexity of Verifying Loop-Free Programs as Differentially Private

Authors Marco Gaboardi, Kobbi Nissim , David Purser

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.129.pdf
  • Filesize: 0.68 MB
  • 17 pages

Document Identifiers

Author Details

Marco Gaboardi
  • Boston University, MA, USA
Kobbi Nissim
  • Georgetown University, Washington, DC, USA
David Purser
  • University of Warwick, Coventry, UK
  • Max Planck Institute for Software Systems, Saarbrücken, Germany

Funding

M. G. and K. N. were supported by NSF grant No. 1565387 TWC: Large: Collaborative: Computing Over Distributed Sensitive Data. D. P. was supported by the UK EPSRC Centre for Doctoral Training in Urban Science (EP/L016400/1).

Acknowledgements

Research partially done while M.G. and K.N. participated in the "Data Privacy: Foundations and Applications" program held at the Simons Institute, UC Berkeley in spring 2019.

Cite As Get BibTex

Marco Gaboardi, Kobbi Nissim, and David Purser. The Complexity of Verifying Loop-Free Programs as Differentially Private. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 129:1-129:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ICALP.2020.129

Abstract

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.

Subject Classification

ACM Subject Classification
  • Security and privacy
  • Theory of computation → Probabilistic computation
Keywords
  • differential privacy
  • program verification
  • probabilistic programs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. John M. Abowd. The U.S. census bureau adopts differential privacy. In Yike Guo and Faisal Farooq, editors, Proceedings of the 24th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, KDD 2018, London, UK, August 19-23, 2018, page 2867. ACM, 2018. URL: https://doi.org/10.1145/3219819.3226070.
  2. Aws Albarghouthi and Justin Hsu. Synthesizing coupling proofs of differential privacy. Proc. ACM Program. Lang., 2(POPL):58:1-58:30, 2018. URL: https://doi.org/10.1145/3158146.
  3. Mário S. Alvim, Miguel E. Andrés, Konstantinos Chatzikokolakis, and Catuscia Palamidessi. On the relation between differential privacy and quantitative information flow. In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 60-76. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_4.
  4. Apple. Apple differential privacy technical overview. URL: https://www.apple.com/privacy/docs/Differential_Privacy_Overview.pdf.
  5. Gilles Barthe, Rohit Chadha, Vishal bibsource = self, Jagannath, A Prasad Sistla, and Mahesh Viswanathan. Deciding differential privacy for programs with finite inputs and outputs. In LICS 2020 (to appear), 2020. arXiv preprint: URL: https://arxiv.org/abs/1910.04137.
  6. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. Higher-order approximate relational refinement types for mechanism design and differential privacy. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 55-68. ACM, 2015. URL: https://doi.org/10.1145/2676726.2677000.
  7. Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving differential privacy via probabilistic couplings. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 749-758. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934554.
  8. Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. Programming language techniques for differential privacy. SIGLOG News, 3(1):34-53, 2016. URL: https://dl.acm.org/citation.cfm?id=2893591.
  9. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 97-110. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103670.
  10. Benjamin Bichsel, Timon Gehr, Dana Drachsler-Cohen, Petar Tsankov, and Martin T. Vechev. Dp-finder: Finding differential privacy violations by sampling and optimization. In David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang, editors, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 508-524. ACM, 2018. URL: https://doi.org/10.1145/3243734.3243863.
  11. Rohit Chadha, Dileep Kini, and Mahesh Viswanathan. Quantitative information flow in boolean programs. In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8414 of Lecture Notes in Computer Science, pages 103-119. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_6.
  12. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, volume 8704 of Lecture Notes in Computer Science, pages 32-46. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_4.
  13. Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate counting in SMT and value estimation for probabilistic programs. Acta Inf., 54(8):729-764, 2017. URL: https://doi.org/10.1007/s00236-017-0297-2.
  14. Dmitry Chistikov, Andrzej S. Murawski, and David Purser. Bisimilarity distances for approximate differential privacy. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 194-210. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_12.
  15. Dmitry Chistikov, Andrzej S. Murawski, and David Purser. Asymmetric distances for approximate differential privacy. In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 10:1-10:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.10.
  16. Loris D'Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, and Benjamin C. Pierce. Sensitivity analysis using type-based constraints. In Richard Lazarus, Assaf J. Kfoury, and Jacob Beal, editors, Proceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages, FPCDSL@ICFP 2013, Boston, Massachusetts, USA, September 22, 2013, pages 43-50. ACM, 2013. URL: https://doi.org/10.1145/2505351.2505353.
  17. Dorothy E. Denning. Cryptography and Data Security. Addison-Wesley, 1982. Google Scholar
  18. Differential Privacy Team, Apple. Learning with privacy at scale, 2017. URL: https://machinelearning.apple.com/docs/learning-with-privacy-at-scale/appledifferentialprivacysystem.pdf.
  19. Zeyu Ding, Yuxin Wang, Guanhong Wang, Danfeng Zhang, and Daniel Kifer. Detecting violations of differential privacy. In David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang, editors, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 475-489. ACM, 2018. URL: https://doi.org/10.1145/3243734.3243818.
  20. Kashyap Dixit, Madhav Jha, Sofya Raskhodnikova, and Abhradeep Thakurta. Testing the lipschitz property over product distributions with applications to data privacy. In Amit Sahai, editor, Theory of Cryptography - 10th Theory of Cryptography Conference, TCC 2013, Tokyo, Japan, March 3-6, 2013. Proceedings, volume 7785 of Lecture Notes in Computer Science, pages 418-436. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36594-2_24.
  21. Cynthia Dwork, Krishnaram Kenthapadi, Frank McSherry, Ilya Mironov, and Moni Naor. Our data, ourselves: Privacy via distributed noise generation. In Serge Vaudenay, editor, Advances in Cryptology - EUROCRYPT 2006, 25th Annual International Conference on the Theory and Applications of Cryptographic Techniques, St. Petersburg, Russia, May 28 - June 1, 2006, Proceedings, volume 4004 of Lecture Notes in Computer Science, pages 486-503. Springer, 2006. URL: https://doi.org/10.1007/11761679_29.
  22. Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam D. Smith. Calibrating noise to sensitivity in private data analysis. In Shai Halevi and Tal Rabin, editors, Theory of Cryptography, Third Theory of Cryptography Conference, TCC 2006, New York, NY, USA, March 4-7, 2006, Proceedings, volume 3876 of Lecture Notes in Computer Science, pages 265-284. Springer, 2006. URL: https://doi.org/10.1007/11681878_14.
  23. Cynthia Dwork, Guy N. Rothblum, and Salil P. Vadhan. Boosting and differential privacy. In 51th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2010, October 23-26, 2010, Las Vegas, Nevada, USA, pages 51-60. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/FOCS.2010.12.
  24. Úlfar Erlingsson, Vasyl Pihur, and Aleksandra Korolova. RAPPOR: randomized aggregatable privacy-preserving ordinal response. In Gail-Joon Ahn, Moti Yung, and Ninghui Li, editors, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014, pages 1054-1067. ACM, 2014. URL: https://doi.org/10.1145/2660267.2660348.
  25. Matthew Fredrikson and Somesh Jha. Satisfiability modulo counting: a new approach for analyzing privacy properties. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 42:1-42:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603097.
  26. Anna C. Gilbert and Audra McMillan. Property testing for differential privacy. In 56th Annual Allerton Conference on Communication, Control, and Computing, Allerton 2018, Monticello, IL, USA, October 2-5, 2018, pages 249-258. IEEE, 2018. URL: https://doi.org/10.1109/ALLERTON.2018.8636068.
  27. J. W. Gray. Probabilistic interference. In Proceedings. 1990 IEEE Computer Society Symposium on Research in Security and Privacy, pages 170-179, May 1990. URL: https://doi.org/10.1109/RISP.1990.63848.
  28. Charlie Jacomme, Steve Kremer, and Gilles Barthe. Universal equivalence and majority on probabilistic programs over finite fields. In LICS 2020 (to appear), 2020. Google Scholar
  29. Madhav Jha and Sofya Raskhodnikova. Testing and reconstruction of lipschitz functions with applications to data privacy. SIAM J. Comput., 42(2):700-731, 2013. URL: https://doi.org/10.1137/110840741.
  30. Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, 1981. URL: https://doi.org/10.1016/0022-0000(81)90036-2.
  31. Michael L. Littman, Judy Goldsmith, and Martin Mundhenk. The computational complexity of probabilistic planning. J. Artif. Intell. Res., 9:1-36, 1998. URL: https://doi.org/10.1613/jair.505.
  32. Min Lyu, Dong Su, and Ninghui Li. Understanding the sparse vector technique for differential privacy. Proc. VLDB Endow., 10(6):637-648, 2017. URL: https://doi.org/10.14778/3055330.3055331.
  33. Frank McSherry. Privacy integrated queries: an extensible platform for privacy-preserving data analysis. In Ugur Çetintemel, Stanley B. Zdonik, Donald Kossmann, and Nesime Tatbul, editors, Proceedings of the ACM SIGMOD International Conference on Management of Data, SIGMOD 2009, Providence, Rhode Island, USA, June 29 - July 2, 2009, pages 19-30. ACM, 2009. URL: https://doi.org/10.1145/1559845.1559850.
  34. Ilya Mironov. On significance of the least significant bits for differential privacy. In Ting Yu, George Danezis, and Virgil D. Gligor, editors, the ACM Conference on Computer and Communications Security, CCS'12, Raleigh, NC, USA, October 16-18, 2012, pages 650-661. ACM, 2012. URL: https://doi.org/10.1145/2382196.2382264.
  35. Jack Murtagh and Salil P. Vadhan. The complexity of computing the optimal composition of differential privacy. In Eyal Kushilevitz and Tal Malkin, editors, Theory of Cryptography - 13th International Conference, TCC 2016-A, Tel Aviv, Israel, January 10-13, 2016, Proceedings, Part I, volume 9562 of Lecture Notes in Computer Science, pages 157-175. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49096-9_7.
  36. Nicolas Papernot, Martín Abadi, Úlfar Erlingsson, Ian J. Goodfellow, and Kunal Talwar. Semi-supervised knowledge transfer for deep learning from private training data. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview.net, 2017. URL: https://openreview.net/forum?id=HkwoSDPgg.
  37. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157-168. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863568.
  38. Indrajit Roy, Srinath T. V. Setty, Ann Kilzer, Vitaly Shmatikov, and Emmett Witchel. Airavat: Security and privacy for mapreduce. In Proceedings of the 7th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2010, April 28-30, 2010, San Jose, CA, USA, pages 297-312. USENIX Association, 2010. URL: http://www.usenix.org/events/nsdi10/tech/full_papers/roy.pdf.
  39. Seinosuke Toda. PP is as hard as the polynomial-time hierarchy. SIAM J. Comput., 20(5):865-877, 1991. URL: https://doi.org/10.1137/0220053.
  40. Michael Carl Tschantz, Dilsun Kirli Kaynar, and Anupam Datta. Formal verification of differential privacy for interactive systems (extended abstract). In Michael W. Mislove and Joël Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 of Electronic Notes in Theoretical Computer Science, pages 61-79. Elsevier, 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.015.
  41. Stanley L Warner. Randomized response: A survey technique for eliminating evasive answer bias. Journal of the American Statistical Association, 60(309):63-69, 1965. Google Scholar
  42. Hirotoshi Yasuoka and Tachio Terauchi. On bounding problems of quantitative information flow. In Dimitris Gritzalis, Bart Preneel, and Marianthi Theoharidou, editors, Computer Security - ESORICS 2010, 15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010. Proceedings, volume 6345 of Lecture Notes in Computer Science, pages 357-372. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15497-3_22.
  43. Hirotoshi Yasuoka and Tachio Terauchi. Quantitative information flow - verification hardness and possibilities. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pages 15-27. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/CSF.2010.9.
  44. Danfeng Zhang and Daniel Kifer. Lightdp: towards automating differential privacy proofs. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 888-901. ACM, 2017. URL: http://dl.acm.org/citation.cfm?id=3009884.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact