A Probabilistic Separation Logic

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

References in corpus (2)

• A Probabilistic Separation Logic
• A Language for Probabilistically Oblivious Computation

Cited by in corpus (16)

• Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
• A Probabilistic Separation Logic
• Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
• Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
• A Separation Logic for Negative Dependence
• Conditional independence by typing
• Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
• Approximate Relational Reasoning for Higher-Order Probabilistic Programs
• A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
• On Algebraic Abstractions for Concurrent Separation Logics
• Tachis: Higher-Order Separation Logic with Credits for Expected Costs
• Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
• Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
• Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects