Computer Science Department
University of California, San Diego
"Securing Software via Design and Proof"
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.
Zach 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.