CAREER: FormalDP: Formally Verified, Private, Accurate and Efficient Data Analysis

职业：FormalDP：经过正式验证、私密、准确、高效的数据分析

基本信息

批准号：
2040249
负责人：
Marco Gaboardi
金额：
$ 48.83万
依托单位：
Trustees of Boston University
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-01-01 至 2025-04-30
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2040249&HistoricalAwards=false
关键词：
CAREER FormalDP Formally Verified Private

项目摘要

Data-driven technology is having an impressive impact on society but privacy concerns restrict the way data can be used and released. Differential privacy has emerged as a leading notion supporting efficient and accurate data analyses that respect privacy. But designing and implementing efficient differentially private data analyses with high utility can be challenging and error prone. Even privacy experts have released code with bugs or designed incorrect algorithms. Programming platforms and formal verification tools can assist data analysts in designing differentially private data analyses without bugs. However, the current approaches have two limitations: first, they support reasoning about privacy but not about accuracy and efficiency which are two other important aspects of data analyses; second, they support reasoning about idealized data analyses but not about their implementations on finite computers. The goal of this project is to overcome these two limitations by developing novel formal verification techniques and tools supporting formal reasoning combining privacy, accuracy, and efficiency guarantees for both data analyses, and their implementations. The results of this project will contribute to develop foundational methods for privacy-preserving technology which can benefit society by improving and promoting safer practices in handling private or sensitive data. Moreover, the project will support educational activities aimed at training students with a global view on data privacy and its practices, and outreach activities aimed at investigating ways in which privacy policies and standards can be impacted by the results of this research.The technical goal of this proposal is the theoretical and technological development of verification techniques and tools that can enable the design of data analyses that are private, accurate, efficient, and with verified implementations. To achieve this goal the project will focus on three concrete directions: first, it will develop formal verification techniques to reason in a formal way about the accuracy of differentially private data analyses; second, it will develop resource analysis techniques to reason about the efficiency of a data analysis in terms of computing time and space, and in terms of the number of needed data samples; third, it will develop reasoning techniques to verify the privacy, accuracy and efficiency of implementations of differentially private algorithms on finite computers. These techniques will be implement as a type-based verification framework, named FormalDP, which will thus support type-based formal reasoning combining privacy, accuracy and efficiency for data analyses and their implementations. The effectiveness of this approach will be assessed through experimental studies about the level of accuracy and efficiency that verified differentially private implementations can achieve.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.

数据驱动的技术对社会产生了令人印象深刻的影响，但隐私问题限制了可以使用和发布数据的方式。差异隐私已成为支持尊重隐私的高效和准确数据分析的主要概念。但是，使用高实用程序设计和实施有效的差异私人数据分析可能是具有挑战性的，并且容易出错。甚至隐私专家也已经发布了使用错误或设计不正确算法的代码。编程平台和正式验证工具可以帮助数据分析师设计差异化私人数据分析而无需错误。但是，当前的方法有两个局限性：首先，它们支持有关隐私的推理，而不是准确性和效率，这是数据分析的其他两个重要方面。其次，他们支持有关理想化数据分析的推理，而不是在有限计算机上实现的。该项目的目的是通过开发新颖的正式验证技术和工具来克服这两个局限性，这些技术和工具支持正式推理，以结合两个数据分析及其实施的隐私，准确性和效率保证。该项目的结果将有助于开发隐私保护技术的基础方法，这些方法可以通过改善和促进处理私人或敏感数据来使社会受益。此外，该项目将支持旨在培训学生对数据隐私及其实践的全球观点的教育活动，以及旨在调查这项研究结果可能影响隐私政策和标准的活动。该提案的技术目标是该验证技术和工具的理论和技术开发，这些技术和工具能够实现私人的设计，并有效地实现了私人的设计，并有效地，并有效地，精确地，精确地。为了实现这一目标，该项目将重点放在三个具体方向上：首先，它将开发出正式的验证技术，以正式的方式推理差异私人数据分析的准确性；其次，它将开发资源分析技术，以根据计算时间和空间以及所需数据样本的数量来推理数据分析的效率；第三，它将开发推理技术，以验证有限计算机上差异私有算法实施的隐私，准确性和效率。这些技术将作为一种基于类型的验证框架实现，该验证框架名为FormalDP，因此将支持基于类型的正式推理，结合了隐私，准确性和效率，以供数据分析及其实现。该方法的有效性将通过实验研究来评估有关验证差异私人实施的准确性和效率水平。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的智力优点和更广泛影响的评估标准来评估值得支持的。