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

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

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.