Formalization of Differential Privacy in Isabelle/HOL

TL;DR

This paper presents a formal Isabelle/HOL library for verifying differential privacy, including continuous distributions, the Laplace mechanism, and report noisy max, enhancing formal verification methods in privacy-preserving data analysis.

Contribution

It introduces the first formalization of differential privacy in Isabelle/HOL supporting continuous distributions and formalizes key mechanisms like Laplace and report noisy max.

Findings

Formalization of differential privacy in Isabelle/HOL

Support for continuous probability distributions

Verification of Laplace and report noisy max mechanisms

Abstract

Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differential privacy of databases is complicated to determine. One of the reasons for this is that small changes in database programs can break their differential privacy. Therefore, formal verification of differential privacy has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing differential privacy in a general setting. To our knowledge, it is the first formalization of differential privacy that supports continuous probability distributions. First, we formalize the standard definition of differential privacy and its basic properties. Second, we formalize the Laplace mechanism and its differential privacy. Finally, we formalize the differential privacy of the report noisy max mechanism.