Date of Award
Spring 2022
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Department
Computer Science
First Advisor
Piskac, Ruzica
Abstract
Software and hardware can often exhibit undesirable behaviors, leading to catastrophic consequences. Formal methods techniques 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 methods, privacy requirements are not considered in their design. However, formal methods are often used to verify the critical components of systems, which is valuable intellectual property. In some settings, the verification requirements are often imposed by outside parties, such as regulatory agencies or software marketplaces, that the system owners do not always trust. These proprietary concerns guide my study of designing efficient formal methods that retain the privacy of the program or even the specification. This thesis introduces a suite of privacy-preserving formal method techniques. 1. 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 thesis describes ppSAT: a privacy-preserving SAT solver. ppSAT enables two parties to decide if the conjunction of their secret formulas is satisfiable while maintaining the privacy of each party’s input formulas. 2. 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. The existing state-of-the-art techniques utilize resolution proofs. This thesis presents a zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic. We encode the validation of a resolution proof using polynomial equivalence checking, which enables us to take advantage of fast ZK protocols to verify relations between polynomials. 3. Privacy-preserving model checking for CTL formulas. Model checking is the problem of verifying whether an abstract model of a computational system meets a specification of behavior described as a logic formula. This thesis explains how to maintain the privacy of both the model and the specification during model checking by applying secure multiparty computation (MPC). Our approach adopts oblivious graph algorithms to allow secure computation of global explicit state model checking with specifications written in computation tree logic (CTL). 4. 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 regular expression pattern matching. These queries are also increasingly concerned with privacy issues. This thesis demonstrates a private regular expression pattern matching based on the oblivious stack and the oblivious transfer (OT) protocols. The former results in the best-known asymptotic complexity for regular expression pattern matching, while the latter leads to optimal numerical performance.
Recommended Citation
LUO, NING, "Privacy-preserving formal methods" (2022). Yale Graduate School of Arts and Sciences Dissertations. 921.
https://elischolar.library.yale.edu/gsas_dissertations/921
