Isabelle library formalizes Rényi differential privacy for secure data analysis
Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)
Cryptography and SecurityLogic in Computer Science
Summary
Calculating privacy guarantees for databases can be very complex, especially when small changes can affect the results. The paper presents a new software library created in Isabelle/HOL that precisely defines and checks a specific kind of privacy measure called Rényi differential privacy. This library also covers related mathematical tools and privacy methods used in machine learning, like adding Gaussian noise. The work helps make privacy guarantees more reliable by formally proving properties instead of relying on informal reasoning.
What this means in practice
- •For database engineers: Implement and verify privacy guarantees in data-management systems using formal proofs of Rényi differential privacy properties.
- •For machine learning engineers: Ensure trustworthy privacy analysis for training models with Gaussian noise by leveraging formally verified privacy computations.
Authors
Tetsuya Sato
Abstract
Differential privacy (DP) is a gold-standard definition of privacy designed to evaluate the privacy guarantee of databases. Rényi differential privacy (RDP) is an important variant of DP that gives tight evaluations of machine learning algorithms. These formulations are easy to understand, but evaluating privacy for actual databases is complicated. Even a small change in the database can break its privacy, and evaluations of DP and RDP themselves are complicated. In particular, RDP evaluations in recent studies have become much harder. Therefore, formal verification of them has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing Rényi differential privacy in a general setting. We first formalize RDP for continuous distributions. As a technical basis, we formalize several properties of convex functions and $f$-divergences for nonnegative convex functions. We formalize basic properties of RDP, conversion laws from RDP to DP, the moment accountants in DP, and the Gaussian mechanism and its RDP. Finally, we discuss the stochastic gradient descent mechanism with Gaussian noise and formalize a rough evaluation of its RDP and DP.