差分隐私的验证性基础
密码学与安全
2025-04-30 v3
摘要
差分隐私 (DP) 已成为隐私保留数据分析的金标准，但正确实现它方面面临诸多挑战。以往工作侧重于高层次验证 DP，假设基础正确且存在完美的随机源。然而，差分隐私的底层理论相当复杂且微妙。基本机制和随机数生成中的缺陷是实际 DP 系统中的关键漏洞来源。本文提出了 SampCert，第一个为差分隐私提供全面、机械化基础的系统。SampCert 使用 Lean 编写，包含超过 12,000 行证明。它提供一种可泛化且可扩展的 DP 概念，构建和组合 DP 机制的框架，以及形式化验证的拉普拉斯和高斯抽样算法。SampCert 为 (1) 为开发下一代差分隐私算法提供机械化基础，以及 (2) 可部署于生产系统中的机械验证原语提供了可能性。事实上，SampCert 的验证算法正 powers Amazon Web Services (AWS) 的差分隐私产品，展示了其实际影响。SampCert 的关键创新包括：(1) 可针对各种 DP 定义（如纯粹 DP、集中 DP、R\`enyi DP）进行实例化的通用 DP 基础；(2) 避免浮点实现陷阱的离散拉普拉斯和高斯抽样算法的形式化验证；(3) 简洁的概率单子和新颖的证明技术，使形式化更加高效。为实现对 DP 和随机数生成的复杂正确性属性的证明，SampCert 大量依赖 Lean 的广泛 Mathlib 库，利用傅里叶分析、测度论和概率论、数论以及拓扑学中的定理。
引用
@article{arxiv.2412.01671,
title = {Verified Foundations for Differential Privacy},
author = {Markus de Medeiros and Muhammad Naveed and Tancrède Lepoint and Temesghen Kahsai and Tristan Ravitch and Stefan Zetzsche and Anjali Joshi and Joseph Tassarotti and Aws Albarghouthi and Jean-Baptiste Tristan},
journal= {arXiv preprint arXiv:2412.01671},
year = {2025}
}