RISE Seminar 4/26/19: Designing Systems for Push-Button Verification, a talk by Xi Wang

April 26, 2019

Title: Designing Systems for Push-Button Verification

Speaker: Xi Wang

Affiliation: University of Washington

Date and location: Friday, April 26, 12:30 – 1:30pm; Wozniak Lounge (430 Soda Hall)

Abstract: I will give an overview of our research projects on designing systems for highly automated formal verification: Hyperkernel (SOSP’17), Nickel (OSDI’18), and more recent work on RISC-V security monitors. Formal verification is effective in eliminating entire classes of bugs, but verifying systems software is a major undertaking and often requires years of expert work.  To free developers from such a proof burden, our key observation is that by co-designing systems and verifiers, we can use SMT solvers such as Z3 to achieve fully automated verification of those systems in a push-button style.  Our results show that it is feasible to radically reduce the verification effort of a set of systems, including file systems and OS kernels, from multiple person-years to a few person-months or even person-weeks.

Bio: Xi Wang is an assistant professor in the Paul G. Allen School of Computer Science & Engineering at the University of Washington.  His research interests are in building secure and reliable systems.  Xi received his PhD from MIT, and B.E. and M.E. from Tsinghua.  His awards include best paper awards at OSDI 2016 and SOSP 2013.