Deciding Differential Privacy for Programs with Finite Inputs and Outputs
Gilles Barthe, Rohit Chadha, Vishal Jagannath, Aravinda Prasad Sistla, Mahesh Viswanathan · 2020
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.