用于差分隐私的关系式 $\star$-提升
计算机科学中的逻辑
2023-06-22 v9 编程语言
摘要
形式化验证的最新进展已将近似提升(也称为近似耦合)确定为证明差分隐私的一种简洁、可组合的抽象。该构造可用两种风格定义。早期定义要求存在一个或多个见证分布，而Sato近期的定义对所有样本集使用全称量化。这些概念各有优势：全称版本比存在性版本更通用，而已知存在性提升满足更精确的组合原理。我们提出了一种新颖的存在性近似提升版本，称为-提升，并证明对于离散概率测度它等价于Sato的构造。我们的工作统一了所有已知的近似提升概念，为两种风格的提升带来了更清晰的性质、更通用的构造和更精确的组合定理，从而实现更丰富的差分隐私证明。我们还澄清了现有近似提升定义之间的关系，并考虑了基于-散度的更通用近似提升。
引用
@article{arxiv.1705.00133,
title = {Relational $\star$-Liftings for Differential Privacy},
author = {Gilles Barthe and Thomas Espitau and Justin Hsu and Tetsuya Sato and Pierre-Yves Strub},
journal= {arXiv preprint arXiv:1705.00133},
year = {2023}
}