Ruzica Piskac (Yale): Privacy-preserving Automated Reasoning

Thumbnail

Event details

Date 04.09.2023
Hour 14:0015:00
Location
Category Conferences - Seminars
Event Language English

Formal methods offer a vast collection of techniques to analyze and ensure the correctness, robustness, and safety of software and hardware systems against a specification. The efficacy of such tools allows their application to even large-scale industrial codebases.  Despite the significant success of formal method techniques, privacy requirements are not considered in their design. When using automated reasoning tools, the implicit requirement is that the formula to be proved is public. To overcome this problem, we propose the concept of privacy-preserving formal reasoning.
We first present privacy-preserving Boolean satisfiability (ppSAT) solver, which allows mutually distrustful parties to evaluate the conjunction of their input formulas while maintaining privacy. We construct an oblivious variant of the classic DPLL algorithm which can be integrated with existing secure two-party computation (2PC) techniques. This solver takes input two private SAT formulas and checks if their conjunction is satisfiable. However, in verification, the users might want to keep their programs private and show in a privacy-preserving manner that their programs adhere to the given public specification.  To this end, we developed a zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic. Our protocol is based on a resolution proof of unsatisfiability. We encoded verification of the resolution proof using polynomial equivalence checking, which enabled us to use fast ZKP protocols for polynomial satisfiability.
Finally, we will conclude the talk by outlining future directions towards privacy-preserving SMT solvers and fully automated privacy-preserving program verification.

Bio : 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.

Practical information

  • General public
  • Free

Organizer

  • Viktor Kuncak

Contact

  • viktor.kuncak@epfl.ch

Event broadcasted in

File

Share