Collaborative Research: SHF: Medium: Foundations of Zero Knowledge Computation

Non-interactive Zero-Knowledge (NIZK) proofs provide a powerful means of verifying properties of private data without revealing any of that data: anyone can check the resulting proofs at any time in the future. Rapid advancements in recent years have made NIZK technology a promising tool for verifiable computation, privacy enhancing technology, and verifiable machine learning; however, these systems are built and optimized in an ad-hoc manner, with very little exploration of the fundamental programming abstractions that NIZK proofs enable. The project’s novelties are programming abstractions that simplify the development and maintenance of projects using NIZKs, techniques for reasoning about the security of large programs using NIZKs and the performance implications of using NIZK technologies, and languages for describing the security policies of realistic applications. The project's impacts are increased productivity of developers and increased software quality of software artifacts that leverage NIZK technologies. The project will also train graduate students. This project will develop techniques for (1) combining code that efficiently generates a NIZK proof and code that verifies it, tackling its inherent duality head on; (2) expressing the security guarantees provided by NIZKs in the language of information-flow control (IFC), addressing both how such guarantees compose in larger systems, as well as exploring the performance overhead of the new abstractions using static amortized resource analysis; and (3) integrating advances in realistic applications, verifying end-to-end security properties of systems that rely on NIZK proofs, such as anonymous credential systems and private payment systems with anti-money laundering protections. 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.