一句话：针对有限输入输出程序，研究差分隐私判定的可判定性，填补逻辑与统计方法回避的基础问题。
差分隐私是含私有数据数据库统计计算的事实标准，其优势在于同时保障个体隐私与提供准确统计结果。由于其数学定义，差分隐私也适合形式分析：已有大量工作用逻辑方法证明隐私，近期又有统计方法发现隐私违反，但这些方法虽实用，却回避了根本的可判定性问题。本文聚焦输入和输出均有限的程序，研究其差分隐私判定问题的可判定性。论文旨在从判定角度弥补现有逻辑证明与统计检测之间的理论空白，为有限输入输出程序上的隐私验证提供可判定性基础。
Differential privacy is a de facto standard for statistical computations over databases that contain private data. Its main and rather surprising strength is to guarantee individual privacy and yet allow for accurate statistical results. Thanks to its mathematical definition, differential privacy is also a natural target for formal analysis. A broad line of work develops and uses logical methods for proving privacy. A more recent and complementary line of work uses statistical methods for finding privacy violations. Although both lines of work are practically successful, they elide the fundamental question of decidability.
DOI 原文 ·
@inproceedings{paperbot5545,
title = {Deciding Differential Privacy for Programs with Finite Inputs and Outputs},
author = {Gilles Barthe and Rohit Chadha and Vishal Jagannath and A. Prasad Sistla and Mahesh Viswanathan},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394796}
}