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.
Fri 24 Jan
|14:00 - 14:21|
|Link to publication DOI Media Attached File Attached|
|14:21 - 14:43|
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun YuUniversity of Technology Sydney, Australia, Li ZhouMax Planck Institute for Security and Privacy/Tsinghua UniversityLink to publication DOI Pre-print Media Attached File Attached
|14:43 - 15:05|
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Kevin LiaoMax Planck Institute for Security and PrivacyLink to publication DOI Media Attached