PrivInfer - Programming Languages for Differential Privacy: Conditioning and Inference

点击翻译按钮获取中文摘要

An enormous amount of individuals' data is collected every day. Thesedata could potentially be very valuable for scientific and medicalresearch or for targeting business. Unfortunately, privacy concernsrestrict the way this huge amount of information can be used andreleased. Several techniques have been proposed with the aim ofmaking the data anonymous. These techniques however lose theireffectiveness when attackers can exploit additional knowledge.Differential privacy is a promising approach to the privacy-preservingrelease of data: it offers a strong guaranteed bound on the increasein harm that a user I incurs as a result of participating in adifferentially private data analysis, even under worst-caseassumptions.A standard way to ensure differential privacy is by adding somestatistical noise to the result of a data analysis. Differentiallyprivate mechanisms have been proposed for a wide range of interestingproblems like statistical analysis, combinatorial optimization,machine learning, distributed computations, etc. Moreover, severalprogramming language verification tools have been proposed with thegoal of assisting a programmer in checking whether a given program isdifferentially private or not.These tools have been proved successful in checking differentiallyprivate programs that uses standard mechanisms. They offer however only alimited support for reasoning about differential privacy when this isobtained using non-standard mechanisms. One limitation comes from thesimplified probabilistic models that are built-in to those tools. Inparticular, these simplified models provide no support (or only verylimited support) for reasoning about explicit conditionaldistributions and probabilistic inference. From the verificationpoint of view, dealing with explicit conditional distributions isdifficult because it requires finding a manageable representation, inthe internal logic of the verification tool, of events and probabilitymeasures. Moreover, it requires a set of primitives to handle themefficiently.In this project we aim at overcoming these limitations by extendingthe scope of verification tools for differential privacy to supportexplicit reasoning about conditional distributions and probabilisticinference. Support for conditional distributions and probabilisticinference is crucial for reasoning about machine learningalgorithms. Those are essential tools for achieving efficient andaccurate data analysis for massive collection of data. So, the goal ofthe project is to provide a novel programming language technologyuseful for enhancing privacy-preserving data analysis based on machine learning.