Piskac Group Wins ACM Award
Professor Ruzica Piskac and her group have won a Distinguished Paper award at the ACM Conference on Computer and Communications Security (CCS) for their paper, “Proving UNSAT in Zero Knowledge.”
 |
| Ruzica Piskac |
Distinguished Paper Awards are presented at CCS to authors whose work represents groundbreaking research in their respective areas. By recognizing these select papers for their ingenuity and importance, this award highlights the theoretical and practical innovations likely to shape the future of computing.
The paper from Piskac, associate professor of computer science, and her group solves a problem that has long beleaguered software developers. When developers upload their software, auditing methods on these platforms validate whether these programs follow the security policies that the platform is enforcing. Because of IP protection concerns, though, developers often want to keep their programs private before any commitment has been made. But to verify that the software follows the company's policies, the developers still need to provide access to the code. As a result, there are several well-known examples of programs being scooped before they could be deployed.
“Our methods solve this issue – now, the auditing/validation tools can be deployed in the privacy-preserving mode,” said Ning Luo, lead author of the paper, and who will receive her Ph.D. this week. “With our methods, the developer can convince the auditors that her software satisfies desired properties without revealing what their programs are.”
 |
| Ning Luo |
This paper on proving the unsatisfiability of Boolean formulas in zero knowledge is a part of work on privacy-preserving formal methods, a field introduced by Professor Piskac and her group. Under the name "formal methods" we assume rigorous software engineering for proving program correctness. The standard process of proving program correctness includes translating a program into a mathematical formalism, such as a formula, and then automatically reasoning about that formula.
However, modern applications require that the program is private so we cannot apply the decades-worth of research done in formal methods. This means that all the tools and methods used in formal verification, while being widely used in industry nowadays, cannot ensure the privacy of programs. Adding privacy concerns to the verification problem requires an entire approach to the problem.
In this paper, the Piskac group introduces algorithms that enable users to verify or prove the correctness and safety of programs, even when the program is private. Proving UNSAT in zero knowledge enables an untrusted party to prove the unsatisfiability of a formula without revealing the proof or even the formula. As many problems on the correctness and safety can be reduced to the problem of the unsatisfiability of Boolean formulas, this paper, therefore, provides the foundation for privacy-preserving formal methods.
Overall, privacy-preserving formal methods present a novel synergy of cryptography and formal methods. The former offers advanced techniques for enhanced privacy, while the latter is widely used to ensure the correctness and safety of programs in practice. Together with their collaborators, Timos Antonopoulos (research scientist at Yale), William R. Harris (Google LLC), Eran Tromer (Columbia University), and Xiao Wang (Northwestern University), Professor Piskac and her group have been developing a suite of privacy-preserving formal methods, including this paper, privacy-preserving model checking (WPES 2020) and privacy-preserving SAT solver (USENIX Security 2022).