Content area
Computer programs control vital infrastructure, safeguard national security, and process all financial transactions, making their correctness and security paramount. Formal verification is a key tool for program trust and assurance. However, as the complexity of computer systems grows, the complexity of their properties does as well. While traditional verification has focused on proving safety, the same techniques do not extend to other properties of interest, such as liveness, correct execution, and cryptographic properties, like zero-knowledge security. While these properties are valuable in cloud computing, where execution is outsourced to untrusted third-party providers, they remain understudied.
This dissertation presents new languages, proof systems, and techniques targeting the verification of programs and their executions. Domain-specific languages (DSLs) are key in this effort. By restricting program syntax to a mathematically well-understood subset, we prove important properties. This dissertation introduces four new languages and proof systems: Ticl, a structural temporal logic for modularly proving complex liveness specifications for infinite, nondeterministic programs; Reef, a system for verifiable regular expression matching that keeps matched text confidential; Otti, a framework for proving correct execution of optimization problems like machine learning training; and Zippel, a language for implementing and automatically verifying properties of non-interactive zero-knowledge protocols.
Each one of those works shows that, by carefully designing languages and proof systems for specific domains, we can have both expressive languages, and practical verification of complex properties which were previously difficult, or impossible to prove. We demonstrate this through case studies in distributed systems, secure computation, and cryptographic protocols.