A Probabilistic Separation Logic

TL;DR

This paper introduces PSL, a probabilistic separation logic that models independence, enabling high-level reasoning about probabilistic programs and verifying cryptographic security properties.

Contribution

It presents a new probabilistic model of BI and develops a sound program logic for reasoning about independence in probabilistic programs.

Findings

Verified cryptographic protocols using PSL

Reasoned about independence and uniformity in proofs

Demonstrated applicability to security properties

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.