research-article

Open access

A probabilistic separation logic

Authors:

Kevin LiaoAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue POPL

Article No.: 55, Pages 1 - 30

https://doi.org/10.1145/3371123

Published: 20 December 2019 Publication History

Abstract

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.

Supplementary Material

WEBM File (a55-barthe.webm)

Download
72.29 MB

References

[1]

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.

[2]

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.

[3]

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.05535

[4]

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/340344

[5]

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.

[6]

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.

[7]

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.10708

[8]

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.

[9]

Stephen Brookes. 2007. A semantics for concurrent separation logic. Theoretical Computer Science 375, 1–3 (2007), 227–270.

[10]

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.

[11]

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.

[12]

Kai-Min Chung and Rafael Pass. 2013. A Simple ORAM. IACR Cryptology ePrint Archive 2013 (2013), 243. http://eprint.iacr. org/2013/243

[13]

Ronald Cramer, Ivan Bjerre Damgård, and Jesper Buus Nielsen. 2015. Secure Multiparty Computation. Cambridge University Press.

[14]

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.09305

[15]

Simon Docherty. 2019. Bunched Logics: A Uniform Approach. Ph.D. Dissertation. University College London.

[16]

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.

[17]

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.

[18]

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.

[19]

Michèle Giry. 1982. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis. Springer Berlin Heidelberg, Berlin, Heidelberg, 68–85.

[20]

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.

[21]

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.

[22]

Oded Goldreich and Rafail Ostrovsky. 1996. Software Protection and Simulation on Oblivious RAMs. Journal of the ACM 43, 3 (1996), 431–473.

[23]

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/624

[24]

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.

[25]

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=375719

[26]

Jonathan Katz and Yehuda Lindell. 2014. Introduction to Modern Cryptography. Chapman and Hall/CRC.

[27]

Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. System Sci. 22, 3 (1981), 328–350.

[28]

Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. System Sci. 30, 2 (1985).

[29]

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.

[30]

Daniele Micciancio. 1997. Oblivious Data Structures: Applications to Cryptography. In ACM SIGACT Symposium on Theory of Computing (STOC), El Paso, Texas . 456–464.

[31]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Transactions on Programming Languages and Systems 18, 3 (1996), 325–353.

[32]

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.

[33]

Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theoretical Computer Science 375, 1–3 (2007), 271–307.

[34]

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.ps

[35]

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.

[36]

David J. Pym. 1999. On Bunched Predicate Logic. In IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy. 183–192.

[37]

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 .

[38]

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.

[39]

Michael O. Rabin. 2005. How To Exchange Secrets with Oblivious Transfer. IACR Cryptology ePrint Archive 2005 (2005), 187.

[40]

John C. Reynolds. 2008. An Introduction to Separation Logic (Preliminary Draft). Technical Report. ITU University, Copenhagen. https://www.cs.cmu.edu/~jcr/copenhagen08.pdf

[41]

Ronald Rivest. 1999. Unconditionally secure commitment and oblivious transfer schemes using private channels and a trusted initializer. (1999).

[42]

N. Saheb-Djahromi. 1980. CPO’s of Measures for Nondeterminism. Theoretical Computer Science 12 (1980), 19–37.

[43]

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.

[44]

Alex Simpson. 2018. Category-theoretic Structure for Independence and Conditional Independence. Electronic Notes in Theoretical Computer Science 336 (2018), 281–297.

[45]

Geoffrey Smith. 2003. Probabilistic Noninterference through Weak Probabilistic Bisimulation. In IEEE Computer Security Foundations Workshop (CSFW), Pacific Grove, California . 3–13.

[46]

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.

[47]

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.

[48]

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.

[49]

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=3290349

[50]

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.

[51]

Hongseok Yang. 2001. Local Reasoning for Stateful Programs. Ph.D. Dissertation. Champaign, IL, USA. AAI3023240.

[52]

Andrew Chi-Chih Yao. 1986. How to generate and exchange secrets. In IEEE Symposium on Foundations of Computer Science (FOCS), Toronto, Ontario . 162–167.

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Skalka CNear J(2024)Language-Based Security for Low-Level MPCProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678246(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678246
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Show More Cited By

Index Terms

A probabilistic separation logic
1. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification
2. Theory of computation
  1. Logic
    1. 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 Languages

When 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 '17

When 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

University of Wisconsin--Madison
ONR
NSF
Facebook

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
1,315
Total Downloads

Downloads (Last 12 months)282
Downloads (Last 6 weeks)65

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Skalka CNear J(2024)Language-Based Security for Low-Level MPCProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678246(1-14)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678246
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Simpson ASobocinski PLago UEsparza J(2024)Equivalence and Conditional Independence in Atomic Sheaf LogicProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662132(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662132
Li JWang EZhang Y(2024)Compiling Probabilistic Programs for Variable Elimination with Information FlowProceedings of the ACM on Programming Languages10.1145/36564488:PLDI(1755-1780)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656448
Dardinier TMüller P(2024)Hyper Hoare Logic: (Dis-)Proving Program HyperpropertiesProceedings of the ACM on Programming Languages10.1145/36564378:PLDI(1485-1509)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656437
Zilberstein NSaliling ASilva A(2024)Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational EffectsProceedings of the ACM on Programming Languages10.1145/36498218:OOPSLA1(276-304)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649821
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Asynchronous Probabilistic Couplings in Higher-Order Separation LogicProceedings of the ACM on Programming Languages10.1145/36328688:POPL(753-784)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632868
Yan PMurray TOhrimenko OPham VSison R(2024)Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious AlgorithmsFormal Methods10.1007/978-3-031-71162-6_10(188-205)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_10
Li JAhmed AHoltzen S(2023)Lilac: A Modal Separation Logic for Conditional ProbabilityProceedings of the ACM on Programming Languages10.1145/35912267:PLDI(148-171)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591226
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents