CIS Homeline
arrow About CIS
spacer spacer
arrow Events
  CIS events in Penn Calendar
spacer spacer
arrow People
spacer spacer
arrow Research
spacer spacer
arrow Undergraduate program
spacer spacer
arrow Graduate program
spacer spacer
arrow Job Openings


CIS Home divider Penn Engineering divider PENN   spacer  

 2013 Distinguished Lecture and Colloquium Series  


Tuesday, March 19th, 2013
3:05 pm
Wu & Chen Auditorium
101 Levine Hall


Zack Tatlock
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.




CIS Home divider Penn Engineering divider PENN   spacer
  Send comments on this page to