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.
