Verified Foundations for Differential Privacy

• URL: http://arxiv.org/abs/2412.01671v2
• Date: Tue, 03 Dec 2024 18:53:16 GMT
• Title: Verified Foundations for Differential Privacy
• Authors: Markus de Medeiros, Muhammad Naveed, Tancrede Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan,
• Abstract summary: We present SampCert, the first comprehensive, mechanized foundation for differential privacy. It offers a generic notion of DP, a framework for constructing and composing DP mechanisms, and formally verified implementations of Laplace and Gaussian sampling algorithms. Indeed, SampCert's verified algorithms power the DP offerings of Amazon Web Services (AWS)
• Score: 7.790536155623866
• License:
• Abstract: Differential privacy (DP) has become the gold standard for privacy-preserving data analysis, but implementing it correctly has proven challenging. Prior work has focused on verifying DP at a high level, assuming the foundations are correct and a perfect source of randomness is available. However, the underlying theory of differential privacy can be very complex and subtle. Flaws in basic mechanisms and random number generation have been a critical source of vulnerabilities in real-world DP systems. In this paper, we present SampCert, the first comprehensive, mechanized foundation for differential privacy. SampCert is written in Lean with over 12,000 lines of proof. It offers a generic and extensible notion of DP, a framework for constructing and composing DP mechanisms, and formally verified implementations of Laplace and Gaussian sampling algorithms. SampCert provides (1) a mechanized foundation for developing the next generation of differentially private algorithms, and (2) mechanically verified primitives that can be deployed in production systems. Indeed, SampCert's verified algorithms power the DP offerings of Amazon Web Services (AWS), demonstrating its real-world impact. SampCert's key innovations include: (1) A generic DP foundation that can be instantiated for various DP definitions (e.g., pure, concentrated, R\'enyi DP); (2) formally verified discrete Laplace and Gaussian sampling algorithms that avoid the pitfalls of floating-point implementations; and (3) a simple probability monad and novel proof techniques that streamline the formalization. To enable proving complex correctness properties of DP and random number generation, SampCert makes heavy use of Lean's extensive Mathlib library, leveraging theorems in Fourier analysis, measure and probability theory, number theory, and topology.

Related papers

• Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting [5.552645730505715]
  Two core challenges are finding expressive, compact, and efficient encodings of distributions of DP algorithms. We address the first challenge by developing a method for tight privacy and accuracy bound synthesis. We develop a framework for leveraging inherent symmetries in DP algorithms.
  arXiv  Detail & Related papers  (2024-02-26T19:29:46Z)
• Closed-Form Bounds for DP-SGD against Record-level Inference [18.85865832127335]
  We focus on the popular DP-SGD algorithm, and derive simple closed-form bounds. We obtain bounds for membership inference that match state-of-the-art techniques. We present a novel data-dependent bound against attribute inference.
  arXiv  Detail & Related papers  (2024-02-22T09:26:16Z)
• Privacy Amplification for Matrix Mechanisms [18.13715687378337]
  "MMCC" is the first algorithm to analyze privacy amplification via sampling for any generic matrix mechanism. We show it leads to significant improvement in the privacy-utility trade-offs for DP-FTRL algorithms on standard benchmarks.
  arXiv  Detail & Related papers  (2023-10-24T05:16:52Z)
• The Normal Distributions Indistinguishability Spectrum and its Application to Privacy-Preserving Machine Learning [7.61316504036937]
  Differential Privacy is the most common method for machine learning (ML) on privacy-sensitive data. In big data analytics, one often uses randomized sketching/aggregation algorithms to make processing high-dimensional data tractable.
  arXiv  Detail & Related papers  (2023-09-03T19:07:31Z)
• Differentially-Private Bayes Consistency [70.92545332158217]
  We construct a Bayes consistent learning rule that satisfies differential privacy (DP) We prove that any VC class can be privately learned in a semi-supervised setting with a near-optimal sample complexity.
  arXiv  Detail & Related papers  (2022-12-08T11:57:30Z)
• Normalized/Clipped SGD with Perturbation for Differentially Private Non-Convex Optimization [94.06564567766475]
  DP-SGD and DP-NSGD mitigate the risk of large models memorizing sensitive training data. We show that these two algorithms achieve similar best accuracy while DP-NSGD is comparatively easier to tune than DP-SGD.
  arXiv  Detail & Related papers  (2022-06-27T03:45:02Z)
• Smoothed Differential Privacy [55.415581832037084]
  Differential privacy (DP) is a widely-accepted and widely-applied notion of privacy based on worst-case analysis. In this paper, we propose a natural extension of DP following the worst average-case idea behind the celebrated smoothed analysis. We prove that any discrete mechanism with sampling procedures is more private than what DP predicts, while many continuous mechanisms with sampling procedures are still non-private under smoothed DP.
  arXiv  Detail & Related papers  (2021-07-04T06:55:45Z)
• Improved, Deterministic Smoothing for L1 Certified Robustness [119.86676998327864]
  We propose a non-additive and deterministic smoothing method, Deterministic Smoothing with Splitting Noise (DSSN) In contrast to uniform additive smoothing, the SSN certification does not require the random noise components used to be independent. This is the first work to provide deterministic "randomized smoothing" for a norm-based adversarial threat model.
  arXiv  Detail & Related papers  (2021-03-17T21:49:53Z)
• On the Practicality of Differential Privacy in Federated Learning by Tuning Iteration Times [51.61278695776151]
  Federated Learning (FL) is well known for its privacy protection when training machine learning models among distributed clients collaboratively. Recent studies have pointed out that the naive FL is susceptible to gradient leakage attacks. Differential Privacy (DP) emerges as a promising countermeasure to defend against gradient leakage attacks.
  arXiv  Detail & Related papers  (2021-01-11T19:43:12Z)
• Improving Generative Adversarial Networks with Local Coordinate Coding [150.24880482480455]
  Generative adversarial networks (GANs) have shown remarkable success in generating realistic data from some predefined prior distribution. In practice, semantic information might be represented by some latent distribution learned from data. We propose an LCCGAN model with local coordinate coding (LCC) to improve the performance of generating data.
  arXiv  Detail & Related papers  (2020-07-28T09:17:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.