Collaborative Research: FMitF: Track I: Automating and Synthesizing Parallel Zero-Knowledge Protocols

Zero-knowledge proof (ZKP) protocols allow one party to prove to others the correctness of a statement without revealing why. Although a relatively old and well-understood concept in cryptography, ZKP protocols recently came into the spotlight again given their many applications in blockchain privacy, private auditing, verifiable computation, and anonymous networks. While ZKP protocols offer exciting capabilities, they also come with a huge overhead in computational resources. For ZKP protocols to reach the same level of practical significance as machine learning algorithms, an automated framework is needed that can allow even non-cryptographers to develop optimized applications backed by parallelizable protocols. The project's broader significance and importance are advancing deployability of state-of-the-art ZKP protocols from a cryptography perspective. The project's novelties are the formal systematization of ZKP protocols to obtain novel parallel and highly optimized ZKP algorithms. Furthermore, the investigators are developing a course that encompasses the foundations of formal computing methods and cryptography and their applications in practical settings. The framework enables non-expert programmers to write efficient and intuitive programs in that domain, by taking full advantage of the scalability and cost savings offered by distributed computing and ZKP-specific optimizations. In particular, the project enables programmers with little background in cryptography to write ZKP applications, automatically obtain optimized versions of the algorithms, and deploy them on multiple machines for improved end-to-end running time. The framework features (i) a programming language where developers can write applications with a sequential mindset, (ii) a compilation and optimization toolset that can first optimize the program and then automatically partition the resulting application into smaller ones, and (iii) a set of supporting components that can help programmers verify and synthesize code in the framework's language. The problem of parallelizing ZKP protocols is studied from a formal methods lens, where many new research questions emerge regarding new optimization problems requiring careful language design and rigorous proofs of security. 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.