Gilles Barthe
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Probabilistic independence is a useful concept for describing the result of random sampling—a basic operation in all probabilistic languages—and for reasoning about groups of random variables. Nevertheless, existing verification methods handle independence poorly, if at all. We propose a probabili stic separation logic PSL, where separation models probabilistic independence. We first give a new, probabilistic model of the logic of bunched implications (BI). We then build a program logic based on these assertions, and prove soundness of the proof system. We demonstrate our logic by verifying information-theoretic security of cryptographic constructions for several well-known tasks, including private information retrieval, oblivious transfer, secure multi-party addition, and simple oblivious RAM. Our proofs reason purely in terms of high-level properties, like independence and uniformity.
Supplemental Material
- Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, and Jason M. Rute. 2019. On the computability of graphons. In IEEE Symposium on Logic in Computer Science (LICS), Vancouver, British Columbia.Google Scholar
- Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, and Pierre-Yves Strub. 2015. Verified Proofs of Higher-Order Masking. In IACR International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT), Sofia, Bulgaria (Lecture Notes in Computer Science) , Vol. 9056. Springer-Verlag, 457–485. Google Scholar
- Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. An AssertionBased Program Logic for Probabilistic Programs. In European Symposium on Programming (ESOP), Thessaloniki, Greece. arXiv: cs.LO/1803.05535 https://arxiv.org/abs/1803.05535Google Scholar
- Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017. Proving uniformity and independence by self-composition and coupling. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Maun, Botswana (EPiC Series in Computing) , Vol. 46. 385–403. http://www.easychair.org/ publications/paper/340344Google Scholar
- Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. A Program Logic for Union Bounds. In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy (Leibniz International Proceedings in Informatics) , Vol. 55. Schloss Dagstuhl–Leibniz Center for Informatics, 107:1–107:15. Google Scholar
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Savannah, Georgia. 90–101. Google Scholar
- Gilles Barthe, Justin Hsu, and Kevin Liao. 2020. A Probabilistic Separation Logic. Proceedings of the ACM on Programming Languages 4, POPL (Jan. 2020). arXiv: cs.PL/1907.10708 https://arxiv.org/abs/1907.10708Google Scholar
- Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proceedings of the ACM on Programming Languages 3, POPL (2019), 34:1–34:29. Google Scholar
- Stephen Brookes. 2007. A semantics for concurrent separation logic. Theoretical Computer Science 375, 1–3 (2007), 227–270. Google Scholar
- T.-H. Hubert Chan, Jonathan Katz, Kartik Nayak, Antigoni Polychroniadou, and Elaine Shi. 2018. More is Less: Perfectly Secure Oblivious Algorithms in the Multi-server Setting. In International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT), Brisbane, Australia (Lecture Notes in Computer Science) , Thomas Peyrin and Steven D. Galbraith (Eds.), Vol. 11274. Springer-Verlag, 158–188. Google Scholar
- Benny Chor, Oded Goldreich, Eyal Kushilevitz, and Madhu Sudan. 1995. Private information retrieval. In IEEE Symposium on Foundations of Computer Science (FOCS), Milwaukee, Wisconsin . 41–50.Google Scholar
- Kai-Min Chung and Rafael Pass. 2013. A Simple ORAM. IACR Cryptology ePrint Archive 2013 (2013), 243. http://eprint.iacr. org/2013/243Google Scholar
- Ronald Cramer, Ivan Bjerre Damgård, and Jesper Buus Nielsen. 2015. Secure Multiparty Computation. Cambridge University Press.Google Scholar
- David Darais, Chang Liu, Ian Sweet, and Michael Hicks. 2020. A Language for Probabilistically Oblivious Computation. Proceedings of the ACM on Programming Languages 4, POPL (Jan. 2020). http://arxiv.org/abs/1711.09305Google Scholar
- Simon Docherty. 2019. Bunched Logics: A Uniform Approach. Ph.D. Dissertation. University College London.Google Scholar
- Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2018. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Proceedings of the ACM on Programming Languages 2, POPL (2018), 59:1–59:28. Google Scholar
- Didier Galmiche, Daniel Méry, and David J. Pym. 2005. The semantics of BI and resource tableaux. Mathematical Structures in Computer Science 15, 6 (2005), 1033–1088. Google Scholar
- Craig Gentry, Kenny A. Goldman, Shai Halevi, Charanjit S. Jutla, Mariana Raykova, and Daniel Wichs. 2013. Optimizing ORAM and Using It Efficiently for Secure Computation. In International Symposium on Privacy Enhancing Technologies (PETS), Bloomington, Indiana (Lecture Notes in Computer Science) , Vol. 7981. Springer-Verlag, 1–18. Google Scholar
- Michèle Giry. 1982. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis. Springer Berlin Heidelberg, Berlin, Heidelberg, 68–85.Google Scholar
- Oded Goldreich. 1987. Towards a Theory of Software Protection and Simulation by Oblivious RAMs. In ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York , Alfred V. Aho (Ed.). 182–194. Google Scholar
- Oded Goldreich, Silvio Micali, and Avi Wigderson. 1987. How to play any mental game. In ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York . 218–229.Google Scholar
- Oded Goldreich and Rafail Ostrovsky. 1996. Software Protection and Simulation on Oblivious RAMs. Journal of the ACM 43, 3 (1996), 431–473. Google Scholar
- Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff. 2015. Automated Analysis and Synthesis of Authenticated Encryption Schemes. IACR Cryptology ePrint Archive 2015 (2015), 624. http://eprint.iacr.org/2015/624Google Scholar
- Russell Impagliazzo and Steven Rudich. 1988. Limits on the Provable Consequences of One-way Permutations. In IACR International Cryptology Conference (CRYPTO), Santa Barbara, California (Lecture Notes in Computer Science) , Vol. 403. Springer, 8–26. Google Scholar
- Samin S. Ishtiaq and Peter W. O’Hearn. 2001. BI as an assertion language for mutable data structures. In ACM SIGPLAN– SIGACT Symposium on Principles of Programming Languages (POPL), London, England . 14–26. https://dl.acm.org/citation. cfm?id=375719Google Scholar
- Jonathan Katz and Yehuda Lindell. 2014. Introduction to Modern Cryptography. Chapman and Hall/CRC.Google Scholar
- Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. System Sci. 22, 3 (1981), 328–350. Google Scholar
- Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. System Sci. 30, 2 (1985). Google Scholar
- Yehuda Lindell. 2017. How to simulate it–a tutorial on the simulation proof technique. In Tutorials on the Foundations of Cryptography . Springer-Verlag, 277–346.Google Scholar
- Daniele Micciancio. 1997. Oblivious Data Structures: Applications to Cryptography. In ACM SIGACT Symposium on Theory of Computing (STOC), El Paso, Texas . 456–464. Google Scholar
- Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Transactions on Programming Languages and Systems 18, 3 (1996), 325–353. Google Scholar
- Moni Naor and Vanessa Teague. 2001. Anti-presistence: history independent data structures. In Proceedings on 33rd Annual ACM Symposium on Theory of Computing, July 6-8, 2001, Heraklion, Crete, Greece . ACM, 492–501. Google Scholar
- Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theoretical Computer Science 375, 1–3 (2007), 271–307. Google Scholar
- Peter W. O’Hearn and David J. Pym. 1999. The logic of bunched implications. Bulletin of Symbolic Logic 5, 2 (1999), 215–244. http://www.math.ucla.edu/%7Easl/bsl/0502/0502-003.psGoogle Scholar
- Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In International Workshop on Computer Science Logic (CSL), Paris, France (Lecture Notes in Computer Science), Vol. 2142. Springer-Verlag, 1–19. Google Scholar
- David J. Pym. 1999. On Bunched Predicate Logic. In IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy. 183–192. Google Scholar
- D. J. Pym. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, Vol. 26. Kluwer Academic Publishers. Errata and Remarks maintained at: http://www.cantab.net/users/david.pym/BI-monographerrata.pdf .Google Scholar
- David J. Pym, Peter W. O’Hearn, and Hongseok Yang. 2004. Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315, 1 (2004), 257–305. Google Scholar
- Michael O. Rabin. 2005. How To Exchange Secrets with Oblivious Transfer. IACR Cryptology ePrint Archive 2005 (2005), 187.Google Scholar
- John C. Reynolds. 2008. An Introduction to Separation Logic (Preliminary Draft). Technical Report. ITU University, Copenhagen. https://www.cs.cmu.edu/~jcr/copenhagen08.pdfGoogle Scholar
- Ronald Rivest. 1999. Unconditionally secure commitment and oblivious transfer schemes using private channels and a trusted initializer. (1999).Google Scholar
- N. Saheb-Djahromi. 1980. CPO’s of Measures for Nondeterminism. Theoretical Computer Science 12 (1980), 19–37. Google Scholar
- Elaine Shi, T.-H. Hubert Chan, Emil Stefanov, and Mingfei Li. 2011. Oblivious RAM with 𝑂 ( (log 𝑁 ) 3 ) Worst-Case Cost. In International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT), Seoul, South Korea (Lecture Notes in Computer Science) , Vol. 7073. Springer, 197–214. Google Scholar
- Alex Simpson. 2018. Category-theoretic Structure for Independence and Conditional Independence. Electronic Notes in Theoretical Computer Science 336 (2018), 281–297. Google Scholar
- Geoffrey Smith. 2003. Probabilistic Noninterference through Weak Probabilistic Bisimulation. In IEEE Computer Security Foundations Workshop (CSFW), Pacific Grove, California . 3–13. Google Scholar
- Sam Staton, Dario Stein, Hongseok Yang, Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. 2018. The BetaBernoulli process and algebraic effects. In International Colloquium on Automata, Languages and Programming (ICALP), Prague, Czech Republic (Leibniz International Proceedings in Informatics) , Vol. 107. Schloss Dagstuhl–Leibniz Center for Informatics, 141:1–141:15. Google Scholar
- Emil Stefanov, Marten van Dijk, Elaine Shi, Christopher W. Fletcher, Ling Ren, Xiangyao Yu, and Srinivas Devadas. 2013. Path ORAM: an extremely simple oblivious RAM protocol. In ACM SIGSAC Conference on Computer and Communications Security (CCS), Berlin, Germany . 299–310. Google Scholar
- Joseph Tassarotti and Robert Harper. 2019. A separation logic for concurrent randomized programs. Proceedings of the ACM on Programming Languages 3, POPL (2019), 64:1–64:30. Google Scholar
- Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3, POPL (2019), 36:1–36:29. https://dl.acm.org/citation.cfm?id=3290349Google Scholar
- Xiao Shaun Wang, Kartik Nayak, Chang Liu, T.-H. Hubert Chan, Elaine Shi, Emil Stefanov, and Yan Huang. 2014. Oblivious Data Structures. In ACM SIGSAC Conference on Computer and Communications Security (CCS), Scottsdale, Arizona. 215–226. Google Scholar
- Hongseok Yang. 2001. Local Reasoning for Stateful Programs. Ph.D. Dissertation. Champaign, IL, USA. AAI3023240.Google Scholar
- Andrew Chi-Chih Yao. 1986. How to generate and exchange secrets. In IEEE Symposium on Foundations of Computer Science (FOCS), Toronto, Ontario . 162–167.Google Scholar
Index Terms
- A probabilistic separation logic
Recommendations
Higher-Order Separation Logic in Isabelle/HOLCF
We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a way that one may use any theory defined in Isabelle/HOLCF to construct ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Comments