Secure Software by Design and Proof
Friday, February 15, 2013 - 10:00am - 11:10am
KEC 1007
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 Biography:
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.
_______________________________________________
Colloquium mailing list
[email protected]
https://secure.engr.oregonstate.edu/mailman/listinfo/colloquium
