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

数据驱动的技术正在对社会产生令人印象深刻的影响，但隐私问题限制了数据的使用和发布方式。差分隐私已成为支持尊重隐私的有效和准确的数据分析的领先概念。但是，设计和实现高效的、具有高实用性的、不同的私有数据分析可能具有挑战性，而且容易出错。甚至隐私专家也发布了带有错误或设计错误算法的代码。编程平台和形式化验证工具可以帮助数据分析人员设计不存在错误的不同私有数据分析。然而，目前的方法有两个局限性：首先，它们支持关于隐私的推理，但不支持准确性和效率，这是数据分析的另外两个重要方面；其次，它们支持关于理想化数据分析的推理，但不支持它们在有限计算机上的实现。该项目的目标是通过开发新的形式验证技术和工具来克服这两个限制，这些技术和工具支持形式推理，将隐私、准确性和数据分析及其实现的效率保证结合起来。该项目的成果将有助于开发隐私保护技术的基本方法，通过改进和促进处理私人或敏感数据的更安全做法，使社会受益。此外，该项目将支持旨在培养学生对数据隐私及其实践具有全球视野的教育活动，以及旨在调查隐私政策和标准可能受到本研究结果影响的方式的外展活动。该提案的技术目标是验证技术和工具的理论和技术发展，这些技术和工具可以使数据分析的设计成为私有的、准确的、有效的，并且具有经过验证的实现。为了实现这一目标，该项目将侧重于三个具体方向：首先，它将开发正式的验证技术，以正式的方式推理差异私有数据分析的准确性；其次，它将发展资源分析技术，从计算时间和空间以及所需数据样本的数量方面来推断数据分析的效率；第三，它将开发推理技术来验证有限计算机上差分私有算法实现的隐私性、准确性和效率。这些技术将作为一个名为FormalDP的基于类型的验证框架来实现，因此它将支持基于类型的形式推理，将隐私、准确性和效率结合起来，用于数据分析及其实现。这种方法的有效性将通过对准确性和效率水平的实验研究进行评估，以验证不同的私人实施可以实现。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.