TACAS Invited Speaker Ruzica Piskac
Ruzica Piskac is an associate professor of computer science at Yale University. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica’s research is improving software reliability and trustworthiness using formal techniques. Ruzica joined Yale in 2013 as an assistant professor and prior to that, she was an independent research group leader at the Max Planck Institute for Software Systems in Germany. In July 2019, she was named the Donna L. Dubinsky Associate Professor of Computer Science, one of the highest recognition that an untenured faculty member at Yale can receive. Ruzica has received various recognitions for research and teaching, including the Patrick Denantes Prize for her PhD thesis, a CACM Research Highlight paper, an NSF CAREER award, the Facebook Communications and Networking award, the Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF), the Amazon Research Award, and the 2019 Ackerman Award for Teaching and Mentoring.
Talk
Expressive and Scalable Privacy-Preserving Automated Reasoning
Thursday, 9:00
Room: Europe A
Program verification provides stronger guarantees of correctness than standard testing. The verification process takes as input a program and derives a mathematical formula. Proving that a program is correct reduces to establishing that this derived formula is unsatisfiable. Traditionally, one can use automated reasoning tools to automatically determine that the formula is unsatisfiable. Furthermore, modern solvers can also produce a proof of unsatisfiability. However, these techniques rely on the fact that the proof and underlying code are publicly available, which may not be desirable for some applications. Our work addresses this problem. Previously, we developed a protocol, called ZKUNSAT, for validating unsatisfiability of Boolean formulas in privacy-preserving settings. A natural extension would be to develop similar techniques for more expressive logics such as those supported by SMT (Satisfiability Modulo Theories) solvers.
In this talk, I will present ZKSMT, a virtual machine for validating unsatisfiability results of SMT solvers in Zero Knowledge (ZK) settings. I will describe theoretical foundations of such virtual machines, and I will show how to use them on the theories of uninterpreted functions and linear integer arithmetic, which are two of the most widely used SMT theories. We empirically evaluated our tool on proofs generated by Boogie, a common tool for software verification. Our results show that ZKSMT is faster than a generic ZK solution by three orders of magnitude.
I will also discuss our recent work, Ou, the first programming framework that provides fully automated and optimal parallelization for zero-knowledge proofs. A zero-knowledge proof (ZKP) is a powerful cryptographic primitive used in many decentralized or privacy-focused applications. However, the high overhead of ZKPs can restrict their practical applicability. The frontend language of our framework ensures privacy and correctness through its robust type system. It also enables cryptography experts to introduce optimizations, such as the employment of extended witnesses or random challenges. In addition, the backend of Ou efficiently and automatically parallelizes ZKPs by formulating program parallelization as integer linear programming problems.
I will conclude by outlining how the full formal verification workflow can be applied in privacy-preserving settings.
This talk is based on the following papers:
[1] Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao: Ou: Automating the Parallelization of Zero-Knowledge Protocols. CCS 2023.
[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. To appear in USENIX ‘24 Security.