What this work contributes
Introduces DipApprox for verifying differential privacy of loop-free probabilistic programs that use Gaussian and other discrete or continuous distributions. It combines numerical integration and tail bounds to approximate probabilities to arbitrary precision, with an almost-decidability result for (ε, δ)-privacy: all but a finite set of δ values are decidable under the paper's assumptions.
When to read this work
Read this when a privacy mechanism uses Gaussian noise or requires reasoning about both discrete and continuous random choices. The Sparse Vector and Noisy Max evaluations provide concrete verification examples.
Topics: Differential privacy · Formal verification · Gaussian mechanisms · Numerical integration · DipApprox
Abstract
The verification of differential privacy algorithms that employ Gaussian distributions is little understood. This paper tackles the challenge of verifying such programs by introducing a novel approach to approximating probability distributions of loop-free programs that sample from both discrete and continuous distributions with computable probability density functions, including Gaussian and Laplace. We establish that verifying (epsilon, delta)-differential privacy for these programs is almost decidable, meaning the problem is decidable for all values of delta except those in a finite set. Our verification algorithm is based on computing probabilities to any desired precision by combining integral approximations, and tail probability bounds. The proposed methods are implemented in the tool, DipApprox, using the FLINT library for high-precision integral computations, and incorporate optimizations to enhance scalability. We validate DipApprox on fundamental privacy-preserving algorithms, such as Gaussian variants of the Sparse Vector Technique and Noisy Max, demonstrating its effectiveness in both confirming privacy guarantees and detecting violations.
Tutorials and reading guides
- DipApprox: verifying differential privacy with Gaussian noise — Inside our CCS 2025 paper: how DipApprox uses certified integration, Gaussian tail bounds, and probability intervals to prove or refute differential privacy.
Cite this work
Download BibTeX · Download RIS
@inproceedings{bhusal2025ccs,
title = {Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions},
author = {Bhusal, Bishnu and Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh},
booktitle = {Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security},
series = {CCS '25},
pages = {1439--1453},
year = {2025},
month = oct,
publisher = {Association for Computing Machinery},
doi = {10.1145/3719027.3765043},
url = {https://doi.org/10.1145/3719027.3765043},
eprint = {2509.08804},
archiveprefix = {arXiv},
keywords = {Differential Privacy, Verification, Gaussian Distribution, Tail Bounds, Approximation Algorithms}
}