log in  |  register  |  feedback?  |  help  |  web accessibility
A Probabilistic Separation Logic
Michael Hicks
Monday, February 10, 2020, 12:00-1:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)

Probabilistic independence is a fundamental tool for reasoning about randomized programs. Independence describes the result of drawing a fresh random sample—a basic operation in all probabilistic languages—and greatly simplifies formal reasoning about collections of random samples. Nevertheless, existing verification methods handle independence poorly, if at all.

In this paper, we propose a probabilistic separation logic where separation models probabilistic independence. We first give a new, probabilistic model of the logic of bunched implications (BI), the logic of assertions in separation logic. Then, we introduce a program logic based on these assertions and prove soundness of the proof system. We demonstrate our logic by verifying security properties of several cryptographic constructions, including simple ORAM, secure multi-party addition, oblivious transfer, and private information retrieval. Our logic is able to state and verify two different forms of the standard cryptographic security property, while proofs work in terms of high-level properties like independence and uniformity.

Paper available at: https://dl.acm.org/doi/10.1145/3371123

This talk is organized by Sankha Narayan Guria