Award Abstract # 2040249
CAREER: FormalDP: Formally Verified, Private, Accurate and Efficient Data Analysis

NSF Org: CNS
Division Of Computer and Network Systems
Recipient: TRUSTEES OF BOSTON UNIVERSITY
Initial Amendment Date: August 18, 2020
Latest Amendment Date: June 2, 2023
Award Number: 2040249
Award Instrument: Continuing Grant
Program Manager: Sol Greenspan
sgreensp@nsf.gov
 (703)292-7841
CNS
 Division Of Computer and Network Systems
CSE
 Directorate for Computer and Information Science and Engineering
Start Date: January 1, 2020
End Date: April 30, 2025 (Estimated)
Total Intended Award Amount: $488,314.00
Total Awarded Amount to Date: $488,314.00
Funds Obligated to Date: FY 2019 = $179,439.00
FY 2021 = $117,126.00

FY 2022 = $98,164.00

FY 2023 = $93,585.00
History of Investigator:
  • Marco Gaboardi (Principal Investigator)
    gaboardi@bu.edu
Recipient Sponsored Research Office: Trustees of Boston University
1 SILBER WAY
BOSTON
MA  US  02215-1703
(617)353-4365
Sponsor Congressional District: 07
Primary Place of Performance: Trustees of Boston University
881 Commonwealth Ave
Boston
MA  US  02215-1300
Primary Place of Performance
Congressional District:
07
Unique Entity Identifier (UEI): THL6A6JLE1S7
Parent UEI:
NSF Program(s): Secure &Trustworthy Cyberspace
Primary Program Source: 01002122DB NSF RESEARCH & RELATED ACTIVIT
01001920DB NSF RESEARCH & RELATED ACTIVIT

01002223DB NSF RESEARCH & RELATED ACTIVIT

01002324DB NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s): 025Z, 1045, 7434
Program Element Code(s): 806000
Award Agency Code: 4900
Fund Agency Code: 4900
Assistance Listing Number(s): 47.070

ABSTRACT

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.

PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH

Note:  When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

wunder, june and Azevedo de Amorim, Arthur and Baillot, Patrick and Gaboardi, Marco "Bunched Fuzz: Sensitivity for Vector Metrics" Lecture notes in computer science , v.13990 , 2023 Citation Details
Zhang, Cheng and de Amorim, Arthur Azevedo and Gaboardi, Marco "On incorrectness logic and Kleene algebra with top and tests" Proceedings of the ACM on Programming Languages , v.6 , 2022 https://doi.org/10.1145/3498690 Citation Details
Bao, Jialu and Gaboardi, Marco and Hsu, Justin and Tassarotti, Joseph "A separation logic for negative dependence" Proceedings of the ACM on Programming Languages , v.6 , 2022 https://doi.org/10.1145/3498719 Citation Details
Bun, Mark and Gaboardi, Marco and Glinskih, Ludmila "The Complexity of Verifying Boolean Programs as Differentially Private" IEEE 35th Computer Security Foundations Symposium (CSF) , 2022 https://doi.org/10.1109/CSF54842.2022.9919653 Citation Details
Rajani, Vineet and Gaboardi, Marco and Garg, Deepak and Hoffmann, Jan "A unifying type-theory for higher-order (amortized) cost analysis" Proceedings of the ACM on Programming Languages , v.5 , 2021 https://doi.org/10.1145/3434308 Citation Details
Sivakumar, Satchit and Bun, Mark and Gaboardi, Marco "Multiclass versus Binary Differentially Private PAC Learning" Advances in Neural Information Processing Systems 34 (NeurIPS 2021) , 2021 Citation Details
Stoughton, Alley and Chen, Carol and Gaboardi, Marco and Qu, Weihao "Formalizing Algorithmic Bounds in the Query Model in EasyCrypt" Leibniz international proceedings in informatics , v.237 , 2022 Citation Details

Please report errors in award information by writing to: awardsearch@nsf.gov.

Print this page

Back to Top of page