Document Open Access Logo

A Program Logic for Union Bounds

Authors Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.107.pdf
  • Filesize: 499 kB
  • 15 pages

Document Identifiers

Author Details

Gilles Barthe
Marco Gaboardi
Benjamin Grégoire
Justin Hsu
Pierre-Yves Strub

Cite As Get BibTex

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. A Program Logic for Union Bounds. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 107:1-107:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.107

Abstract

We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analyzing randomized algorithms. In formal verification terms, the union bound allows flexible and compositional reasoning over possible ways an algorithm may go wrong. It also enables a clean separation between reasoning about probabilities and reasoning about events, which are expressed as standard first-order formulas in our logic. Notably, assertions in our logic are non-probabilistic, even though we can conclude probabilistic facts from the judgments.

Our logic can also prove accuracy properties for interactive programs, where the program must produce intermediate outputs as soon as pieces of the input arrive, rather than accessing the entire input at once. This setting also enables adaptivity, where later inputs may depend on earlier intermediate outputs. We show how to prove accuracy for several examples from the differential privacy literature, both interactive and non-interactive.

Subject Classification

Keywords
  • Probabilistic Algorithms
  • Accuracy
  • Formal Verification
  • Hoare Logic
  • Union Bound

Metrics

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

References

  1. Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568-589, 2009. URL: https://www.lri.fr/~paulin/ALEA/random-scp.pdf.
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Formal certification of randomized algorithms. 2015. URL: http://justinh.su/files/docs/BEGGHS15paper.pdf.
  4. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. Relational reasoning via probabilistic coupling. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Suva, Fiji, volume 9450, pages 387-401, 2015. URL: http://arxiv.org/abs/1509.03476.
  5. Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub. Proving differential privacy in Hoare logic. In IEEE Computer Security Foundations Symposium (CSF), Vienna, Austria, 2014. URL: http://arxiv.org/abs/1407.2988, URL: http://arxiv.org/abs/Yes.
  6. Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proving differential privacy via probabilistic couplings. In IEEE Symposium on Logic in Computer Science (LICS), New York, New York, 2016. To appear. URL: http://arxiv.org/abs/1601.05047, URL: http://arxiv.org/abs/Yes.
  7. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. Formal certification of code-based cryptographic proofs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Savannah, Georgia, pages 90-101, New York, 2009. URL: http://research.microsoft.com/pubs/185309/Zanella.2009.POPL.pdf.
  8. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. Probabilistic relational reasoning for differential privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania, pages 97-110, 2012. URL: http://certicrypt.gforge.inria.fr/2012.POPL.pdf.
  9. Sooraj Bhat, Ashish Agarwal, Richard Vuduc, and Alexander Gray. A type theory for probability density functions. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania, pages 545-556, 2012. URL: http://dx.doi.org/10.1145/2103656.2103721.
  10. Johannes Borgström, Andrew D. Gordon, Michael Greenberg, James Margetson, and Jurgen Van Gael. Measure transformer semantics for Bayesian machine learning. Logical Methods in Computer Science, 9(3), 2013. URL: https://doi.org/10.2168/LMCS-9(3:11)2013.
  11. Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia, pages 511-526, 2013. URL: https://www.cs.colorado.edu/~srirams/papers/cav2013-martingales.pdf.
  12. Aleksandar Chakarov and Sriram Sankaranarayanan. Expectation invariants as fixed points of probabilistic programs. In International Symposium on Static Analysis (SAS), Munich, Germany, volume 8723 of Lecture Notes in Computer Science, pages 85-100. Springer-Verlag, 2014. URL: https://www.cs.colorado.edu/~srirams/papers/sas14-expectations.pdf.
  13. Patrick Cousot and Michael Monerau. Probabilistic abstract interpretation. In Helmut Seidl, editor, European Symposium on Programming (ESOP), Tallinn, Estonia, volume 7211 of Lecture Notes in Computer Science, pages 169-193. Springer, 2012. URL: http://www.di.ens.fr/~cousot/publications.www/Cousot-Monerau-ESOP2012-extended.pdf.
  14. Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. Calibrating noise to sensitivity in private data analysis. In IACR Theory of Cryptography Conference (TCC), New York, New York, pages 265-284, 2006. URL: http://dx.doi.org/10.1007/11681878_14.
  15. Cynthia Dwork and Aaron Roth. The algorithmic foundations of differential privacy. Foundations and Trends in Theoretical Computer Science, 9(3-4):211-407, 2014. URL: http://dx.doi.org/10.1561/0400000042.
  16. Luis María Ferrer Fioriti and Holger Hermanns. Probabilistic termination: Soundness, completeness, and compositionality. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, pages 489-501. ACM, 2015. URL: http://www.ae-info.org/attach/User/Hermanns_Holger/Publications/FH-POPL15.pdf.
  17. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In European Symposium on Programming (ESOP), Eindhoven, The Netherlands, Lecture Notes in Computer Science, 2016. Google Scholar
  18. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C Pierce. Linear dependent types for differential privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 357-370, 2013. URL: http://dl.acm.org/citation.cfm?id=2429113.
  19. Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. Prinsys - on a quest for probabilistic loop invariants. In International Conference on Quantitative Evaluation of Systems (QEST), pages 193-208, 2013. Google Scholar
  20. Anupam Gupta, Aaron Roth, and Jonathan Ullman. Iterative constructions and private data release. In IACR Theory of Cryptography Conference (TCC), Taormina, Italy, pages 339-356, 2012. URL: http://arxiv.org/abs/1107.3731.
  21. Moritz Hardt and Guy N Rothblum. A multiplicative weights mechanism for privacy-preserving data analysis. In IEEE Symposium on Foundations of Computer Science (FOCS), Las Vegas, Nevada, pages 61-70, 2010. URL: http://www.mit.edu/~rothblum/papers/pmw.pdf.
  22. Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent programs. In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, pages 1-6, 1982. URL: http://dx.doi.org/10.1145/582153.582154.
  23. Joe Hurd, Annabelle McIver, and Carroll Morgan. Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science, 346(1):96-112, 2005. Google Scholar
  24. C. Jones and Gordon D. Plotkin. A probabilistic powerdomain of evaluations. In IEEE Symposium on Logic in Computer Science (LICS), Asilomar, California, pages 186-195, 1989. URL: http://dx.doi.org/10.1109/LICS.1989.39173.
  25. Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs. In European Symposium on Programming (ESOP), Eindhoven, The Netherlands, Lecture Notes in Computer Science, 2016. Google Scholar
  26. Joost-Pieter Katoen. Perspectives in probabilistic verification. In IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 3-10, 2008. Google Scholar
  27. Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll Morgan. Linear-invariant generation for probabilistic programs. In Radhia Cousot and Matthieu Martel, editors, International Symposium on Static Analysis (SAS), Perpignan, France, volume 6337 of Lecture Notes in Computer Science, pages 390-406. Springer, 2010. Google Scholar
  28. Dexter Kozen. Semantics of probabilistic programs. In IEEE Symposium on Foundations of Computer Science (FOCS), San Juan, Puerto Rico, pages 101-114, 1979. Google Scholar
  29. Dexter Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, 1985. Google Scholar
  30. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Tallinn, Estonia, pages 52-66, 2002. Google Scholar
  31. A. McIver and C. Morgan. Abstraction, Refinement, and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. Google Scholar
  32. Frank McSherry and Kunal Talwar. Mechanism design via differential privacy. In IEEE Symposium on Foundations of Computer Science (FOCS), Providence, Rhode Island, pages 94-103, 2007. URL: http://dx.doi.org/10.1109/FOCS.2007.41.
  33. David Monniaux. Abstract interpretation of probabilistic semantics. In Jens Palsberg, editor, International Symposium on Static Analysis (SAS), Santa Barbara, California, volume 1824 of Lecture Notes in Computer Science, pages 322-339. Springer, 2000. Google Scholar
  34. Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325-353, 1996. Google Scholar
  35. Lyle Harold Ramshaw. Formalizing the Analysis of Algorithms. PhD thesis, Stanford University, 1979. Google Scholar
  36. Robert Rand and Steve Zdancewic. VPHL: A verified partial-correctness logic for probabilistic programs. In Mathematical Foundations of Program Semantics (MFPS), 2015. Google Scholar
  37. Jason Reed and Benjamin C Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, 2010. URL: http://dl.acm.org/citation.cfm?id=1863568.
  38. Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S McKinley, Dan Grossman, and Luis Ceze. Expressing and verifying probabilistic assertions. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Edinburgh, Scotland, page 14, 2014. URL: http://research.microsoft.com/pubs/211410/passert-pldi2014.pdf.
  39. Micha Sharir, Amir Pnueli, and Sergiu Hart. Verification of probabilistic programs. SIAM Journal on Computing, 13(2):292-314, 1984. URL: http://dx.doi.org/10.1137/0213021.
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