Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918138874953728 |
|---|---|
| author | Bhusal, Bishnu Chadha, Rohit Sistla, A. Prasad Viswanathan, Mahesh |
| author_facet | Bhusal, Bishnu Chadha, Rohit Sistla, A. Prasad Viswanathan, Mahesh |
| contents | 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 $(ε,δ)$-differential privacy for these programs is \emph{almost decidable}, meaning the problem is decidable for all values of $δ$ 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 {\ourtool} 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_08804 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions Bhusal, Bishnu Chadha, Rohit Sistla, A. Prasad Viswanathan, Mahesh Cryptography and Security Programming Languages D.2.5; F.4.1 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 $(ε,δ)$-differential privacy for these programs is \emph{almost decidable}, meaning the problem is decidable for all values of $δ$ 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 {\ourtool} 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. |
| title | Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions |
| topic | Cryptography and Security Programming Languages D.2.5; F.4.1 |
| url | https://arxiv.org/abs/2509.08804 |