Friday, February 15, 2013 - 10:00am to 11:10am
KEC 1007

Speaker Information

Zachary Tatlock
PhD Candidate
Computer Science and Engineering
UC San Diego

Abstract

As our dependence on software grows, so too do the risks posed by programming errors. In principle, programmers could eliminate the dangerous and exploitable errors that plague modern systems by formally proving their code correct. Unfortunately, the overwhelming burden of constructing such machine-checkable proofs has made formal verification prohibitively expensive for most applications.

In this talk I will describe techniques I developed to radically reduce the formal verification proof burden. In particular, I will focus on formal shim verification, a new method to scale formal verification up to large systems. With formal shim verification, a system is partitioned into components which must interact and access resources through a narrow interface known as the shim. By sandboxing all untrusted components and verifying the shim, we can establish formal correctness guarantees for the entire system while only reasoning about a tiny fraction of the code. We applied formal shim verification to guarantee several important security properties in a new, modern web browser dubbed QUARK. In addition, I will also briefly discuss my previous work on automated, domain specific language (DSL) based techniques to reduce the proof burden for formally verifying compiler optimizations.

Speaker Bio

Zachary Tatlock is a PhD candidate in Computer Science and Engineering at UC San Diego where he is a member of the Programming Systems group. He received BS degrees in Computer Science and Mathematics from Purdue University. His research draws upon proof assistants, Satisfiability Modulo Theories (SMT) solvers, and type systems to improve software reliability and security in domains ranging from embedded database query languages and compiler optimizations to web browsers.