Advanced Probabilistic Couplings for Differential Privacy
Gilles Barthe Noémie Fong Marco Gaboardi IMDEA Software Institute Madrid, Spain ENS Paris, France University at Buffalo, SUNY Buffalo, USA Benjamin Grégoire Justin Hsu Pierre-Yves Strub Inria Sophia-Antipolis, France University of Pennsylvania Philadelphia, USA IMDEA Software Institute Madrid, Spain
Abstract
Differential privacy is a promising formal approach to data privacy, which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information. Several tools have been developed for the formal verification of differentially private algorithms, including program logics and type systems. However, these tools do not capture fundamental techniques that have emerged in recent years, and cannot be used for reasoning about cutting-edge differentially private algorithms. Existing techniques fail to handle three broad classes of algorithms: 1) algorithms where privacy depends on accuracy guarantees, 2) algorithms that are analyzed with the advanced composition theorem, which shows slower growth in the privacy cost, 3) algorithms that interactively accept adaptive inputs.
中文速览
差分隐私（differential privacy）的形式化验证工具长期无法处理三类重要算法：隐私保证依赖精度的算法、需要用"高级组合定理"（advanced composition theorem）分析的算法、以及能交互式接收自适应输入的算法。本文扩展了关系程序逻辑 apRHL，引入新的证明规则，将精度逻辑 aHL 整合进来以支持精度依赖型隐私推理，并将高级组合定理推广到近似耦合（approximate coupling）框架以处理循环体的隐私分析，同时增加了对手规则来建模自适应交互输入；此外还提出了一种名为"最优子集耦合"（optimal subset coupling）的新耦合构造，给出拉普拉斯分布的最优区间耦合规则。以融合了上述全部三类难点的 Sparse Vector 变体算法"Between Thresholds 自适应稀疏向量"为贯穿示例，作者在 EasyCrypt 中完成了机器可验证的差分隐私形式化证明，证明过程无需繁琐的概率计算，展示出近似耦合方法在差分隐私形式化验证中的强大表达能力。
原文 arXiv:1606.07143;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1606.07143v2