Dissertation Defense
Ning Luo
Time is tentative
Title: Privacy-preserving formal methods
Advisor: Ruzica Piskac
Other Committee Members:
Timos Antonopoulos
Clark Barrett (Stanford University)
Dan Boneh (Stanford University)
Zhong Shao
Abstract:
Software and hardware can often exhibit undesirable behaviors, which can lead to catastrophic consequences. Formal methods offer a vast collection of techniques to analyze and verify these systems mathematically to ensure the correctness, robustness, and safety of software and hardware systems against a specification.
Despite the significant success of formal method techniques, privacy requirements are not being considered in their design. On the other hand, formal methods are often used to verify the critical components of systems, which is frequently valuable intellectual property. Furthermore, the specification requirements are often imposed by outside parties in some settings, such as regulatory agencies or software marketplaces, entities that are not always trusted by the system owners.
My study of designing efficient formal methods that retain a program’s privacy is guided by these proprietary concerns. In this dissertation, I introduce a suite of privacy-preserving formal method techniques I have designed:
- Privacy-preserving SAT solving. The SAT problem is finding an assignment of variables to make a Boolean formula evaluate to true. As one of the most fundamental problems, it is the core of many verification techniques with SMT solvers often being crucial components. This dissertation describes ppSAT: a privacy-preserving SAT solver that enables two parties to decide whether the conjunction of their secret formulae is satisfiable or not while maintaining the privacy of each party’s input formulae.
- Refutation proofs in zero knowledge. Proving that a given Boolean formula is unsatisfiable is critical in formal methods for illustrating the safety or robustness of a system, and the existing state-of-the-art techniques utilize resolution proofs. This dissertation presents a zero-knowledge protocol for proving the unsatisfiability of Boolean formulae in propositional logic. We encode the verification of a resolution proof using polynomial equivalence checking, which enabled us to use a fast ZK protocol for verifying relations between polynomials.
- Privacy-preserving model checking for CTL formulae. Model checking is the problem of verifying whether an abstract model of a computational system meets a specification of behavior given as a logic formula. This dissertation explains how to apply secure multiparty computation (MPC) to model-checking algorithms to maintain the privacy of both the model and the specification. Our approach adopts oblivious graph algorithms to allow for secure computation of global explicit state model checking with specifications written in Computation Tree Logic (CTL).
- Private regular expression pattern matching based on NFA. Regular expression pattern matching is one of the fundamental query operations in computer science and formal languages. Many applications, such as network intrusion detection and policy checking for DNS queries, depend on such queries which are also increasingly concerned with privacy issues. This dissertation demonstrates a private regular expression pattern-matching design based on the oblivious stack and transfer protocols. The former results in the best-known asymptotic complexity for regular expression pattern matching, while the latter leads to optimal numerical performance.