权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

SHF：媒介：协作研究：差分隐私机制的验证

基本信息

批准号：
1901069
负责人：
Aravinda Sistla
金额：
$ 80万
依托单位：
University of Illinois at Chicago
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2019
资助国家：
美国
起止时间：
2019-10-01 至 2024-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1901069&HistoricalAwards=false
关键词：
SHF Medium Collaborative Research Verification

项目摘要

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.

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

项目成果

期刊论文数量（18）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs

DOI：
10.1109/lics52264.2021.9470708
发表时间：
2021-04
期刊：
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
影响因子：
0
作者：
Rohit Chadha;A. Sistla;Mahesh Viswanathan
通讯作者：
Rohit Chadha;A. Sistla;Mahesh Viswanathan

Optimal prediction of synchronization-preserving races

同步保持竞争的最佳预测

DOI：
10.1145/3434317
发表时间：
2021
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Mathur, Umang;Pavlogiannis, Andreas;Viswanathan, Mahesh
通讯作者：
Viswanathan, Mahesh

Decidable Synthesis of Programs with Uninterpreted Functions

DOI：
10.1007/978-3-030-53291-8_32
发表时间：
2020-06-16
期刊：
Computer Aided Verification
影响因子：
0
作者：
Krogmeier P;Mathur U;Murali A;Madhusudan P;Viswanathan M
通讯作者：
Viswanathan M

Checking LTL[F,G,X] on compressed traces in polynomial time

在多项式时间内检查压缩迹线上的 LTL[F,G,X]

DOI：
10.1145/3468264.3468557
发表时间：
2021
期刊：
ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
影响因子：
0
作者：
Zhang, Minjian;Mathur, Umang;Viswanathan, Mahesh
通讯作者：
Viswanathan, Mahesh

Controller Synthesis for Linear System With Reach-Avoid Specifications