A Probabilistic Separation Logic
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 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
Semantics of Probabilistic & Quantum ProgrammingResearch Papers at Ile de France II (IDF II)
Chair(s): Alexandra Silva University College London
|Full Abstraction for the Quantum Lambda-Calculus|
Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS LyonLink to publication DOI Media Attached File Attached
|Relational Proofs for Quantum Programs|
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Mingsheng Ying University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun Yu University of Technology Sydney, Australia, Li Zhou Max Planck Institute for Security and Privacy/Tsinghua UniversityLink to publication DOI Pre-print Media Attached File Attached
|A Probabilistic Separation Logic|
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Kevin Liao Max Planck Institute for Security and PrivacyLink to publication DOI Media Attached