Approximate Relational Hoare Logic for Continuous Random Samplings

TL;DR

This paper extends approximate relational Hoare logic (apRHL) to handle continuous random samplings by defining a graded relational lifting of the Giry monad, enabling formal verification of differential privacy in continuous settings.

Contribution

It introduces a graded relational lifting of the Giry monad and extends apRHL to verify differential privacy with continuous random samplings.

Findings

Extended apRHL to continuous samplings.

Provided proof rules for continuous random samplings.

Enhanced formal verification capabilities for privacy analysis.

Abstract

Approximate relational Hoare logic (apRHL) is a logic for formal verification of the differential privacy of databases written in the programming language pWHILE. Strictly speaking, however, this logic deals only with discrete random samplings. In this paper, we define the graded relational lifting of the subprobabilistic variant of Giry monad, which described differential privacy. We extend the logic apRHL with this graded lifting to deal with continuous random samplings. We give a generic method to give proof rules of apRHL for continuous random samplings.