Correct Programs, Executed Correctly: Verifying Specifications And Executions

Computer programs control vital infrastructure, safeguard national security, and process all financialtransactions, 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 verifica-tion 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 proper- ties. 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 specificdomains, 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.

Author dc:creator

• Ioannidis, Eleftherios

Advisors dc:contributor.advisor

• Angel, Sebastian
• Zdancewic, Steve

• Computer Sciences

Language dc:language.iso

en

Repository record dc:identifier.uri

https://repository.upenn.edu/handle/20.500.14332/61703

OAI identifier oai:identifier

oai:repository.upenn.edu:20.500.14332/61703