SHF: Medium: Collaborative Research: Verification of Differential Privacy Mechanisms

从数据中提取信息是公共政策、科学和商业决策不可或缺的一部分。负责任的信息提取要求尊重个人数据的隐私。差分隐私是一个精确而流行的概念，它在确保数据隐私的同时保证其分析的有用性。保护数据隐私的方案很难设计。即使是善意的机制也可能无法尊重隐私，因为关于分析隐私的推理是微妙的。该项目开发自动化方法，以确定数据分析方法是否根据差异隐私的概念保护数据隐私。这些技术要么证明给定的数据分析方法是差异私有的，要么在分析不足时向分析人员提供反馈。该项目包括教育活动，如指导/培训研究生，为研究生、本科生、初中生和高中生编写课程材料，以及参与针对本科生、初中生和高中生代表性不足的少数民族的外联活动。该项目采用基于模型检查的方法来验证差异隐私。主要研究重点包括(a)通过考虑不同复杂性的项目来确定可决定和不可决定的案例；(b)开发可决性案例的模型检查技术，使用抽象、对称约简和符号方法来对抗状态空间爆炸；(c)制订反例方案和产生反例的方法；(d)开发实现算法的工具，并在示例程序上对其进行实验评估。该项目的研究成功将推动安全性和差异隐私验证的最新技术。该项目为初高中学生开发游戏和特殊的离线编码练习，向他们介绍安全和隐私方面的一些挑战和想法。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Information extraction from data is integral to decision making in public policy, science, and business. Responsible information extraction demands respecting privacy of individual data. Differential privacy is a precise, and popular notion that ensures data privacy while guaranteeing its usefulness for analysis. Schemes to preserve data privacy are difficult to design. Even well intentioned mechanisms may fail to respect privacy, because reasoning about privacy of an analysis is subtle. This project develops automated methods that determine if a data analysis method, preserves data privacy with respect to the notion of differential privacy. These techniques either certify that the given data analysis method is differentially private, or provide feedback to analyst when it falls short. The project includes educational activities like mentoring/training of graduate students, development of curricular materials for graduate, undergraduate, middle and high school students, and participation in outreach activities targeting under represented minorities at the undergraduate, middle and high school levels. The project takes a model checking based approach to verifying differential privacy. Principal research thrusts include (a) identification of decidable and undecidable cases by considering programs of varying complexity; (b) development of model checking techniques, for decidability cases, that combat state space explosion using abstraction, symmetry reduction, and symbolic approaches; (c) development of counterexample schemes and methods to generate them; and (d) development of tools implementing the algorithms and evaluating them experimentally on example programs. Research successes in the project will advance state of the art in verification of security and differential privacy. The project develops games and special off-line coding exercises for middle and high school students to introduce them to some of the challenges and ideas in security and privacy.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.