Proofs as Polynomials

Location: TU Wien, FAV Hörsaal 1 Helmut Veith (Favoritenstr. 11, Room HEEG02)
Date & Time: 2024-09-27; 9:00 - 10:00

Abstract: Zero-knowledge (ZK) protocols are well-known cryptographic primitives that allow one party to prove to another party a statement without revealing anything beyond the statement. A ZK protocol consists of two parties: a “prover” and a “verifier”. In our work, the prover holds a secret formula and its proof of validity and needs to convince the verifier about the correctness of the proof. The verifier validates the prover’s claims, by checking every step of the proof. To be able to do that without revealing any details about the formula, we use so-called commitment schemes. Commitment schemes are a fundamental part of zero-knowledge protocols as they allow a prover to commit to a value while keeping it hidden, ensuring the value cannot be altered later. A polynomial commitment scheme can be used to commit polynomials and prove the properties of the polynomials. Our work encodes proofs as polynomials and transforms this way checking the proofs steps into checking relations between polynomials. By doing these, we are able to verify the proof without revealing the formulae (and the proof itself).

In this talk, we focus on proofs for formulas produced in the verification process and we explain how to encode them as polynomials. Initially, we developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. We use the resolution calculus to produce a proof of unsatisfiability: we encoded each clause appearing in the proof as a polynomial and we reduced checking the correctness of the resolution rule to checking the divisibility of two polynomials.

A natural extension of this technique is to consider more expressive logics, such as those supported by SMT (Satisfiability Modulo Theories) solvers. To this end, we extended our initial work and developed a virtual machine for validating general unsatisfiability proofs. This virtual machine can support the majority of popular theories when proving program safety while being complete and sound. To demonstrate this, we use theories of equality and linear integer arithmetic as examples. These theories require non-trivial checking procedures and we proposed optimized arithmetizations based on multiset interpretation and polynomial encodings.

Finally, we will conclude the talk by outlining how this approach benefits and empowers the verification process: we can now obtain privacy while preserving correctness.

This talk is based on the following papers:

[1] Ning Luo, Timos Antonopoulos, William Harris, Ruzica Piskac, Eran Tromer, Xiao Wang: Proving UNSAT in Zero Knowledge, CCS 2022

[2] Daniel Luick, John C. Kolesar, Timos Antonopoulos, William R. Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, Ning Luo: ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge. USENIX ‘24 Security.

Bio: Ruzica Piskac is a Professor of Computer Science at Yale University, where she leads the Rigorous Software Engineering (ROSE) group. Her research interests span the areas of software verification, security and applied cryptography, automated reasoning, and code synthesis. Much of her research has focused on using formal techniques to improve software reliability and trustworthiness. Piskac joined Yale’s Department of Computer Science in 2013. She was previously an Independent Research Group Leader at the Max Planck Institute for Software Systems in Germany. Her research has received a range of professional honors, including multiple Amazon Research Awards, Yale University’s Ackerman Award for Teaching and Mentoring, the Facebook Communications and Networking Award, and the Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF). In 2019, Yale named Piskac the Donna L. Dubinsky Associate Professor of Computer Science. Piskac holds a Ph.D. from the Swiss Federal Institute of Technology (EPFL), where her dissertation won the Patrick Denantes Prize. Her current and recent professional activities include service as Program Chair of the 37th International Conference on Computer Aided Verification and the Steering Committee of the Formal Methods in Computer-Aided Design conference. Piskac has graduated five PhD students, four of them are currently holding a position of an assistant professor of computer science.