A System's Hackers Crash Course: Techniques that Find Lots of Bugs in Real (Storage) System Code

This talk describes several effective bug-finding tools we have developed, which exploit not-widely-understood techniques—implementation-level model checking and symbolic execution—focusing on the key intuitions and ideas behind them.

These tools have found errors in every system we checked, including: three version control systems, BerkelyDB, an NFS implementation, ten file systems, a RAID system, and the popular VMware GSX virtual machine. These errors have been serious, such as where an inopportune crash will cause various Linux file systems (e.g., ext3) to to trash their entire root directory "/" or bad disk images that, when mounted, will crash the system.

The talk will close with some of the weird surprises that happen when academics try to commercialize bug-finding research.

Dawson Engler is an Associate Professor in CS and EE at Stanford. He received his PhD from MIT for his work on the exokernel operating system and his undergraduate degree from University of Arizona, the latter in large part funded by being a bouncer. His research focuses on developing techniques to find interesting bugs in real code, including static analysis, implementation level model checking, and symbolic execution. His research group has won numerous "Best Paper" awards and its static tools have found thousands of errors in open source systems (e.g., Linux and BSD) and have formed the basis of a company, Coverity, which has over 200 customers and 70 employees. He won the 2006 Weiser award.