Model Checking An Entire Linux Distribution for Security Violations

Benjamin Schwarz, Hao Chen, David Wagner, Geoff Morrison, Jacob West, Jeremy Lin, and Wei Tu

Software model checking has become a popular tool for verifying
programs' behavior.  Recent results suggest that it is viable for
finding and eradicating security bugs quickly.  However, even
state-of-the-art model checkers are limited in use when they report an
overwhelming number of false positives, or when their lengthy running
time dwarfs other software development processes.  In this paper we
report our experiences with software model checking for security
properties on an extremely large scale---an entire Linux distribution
consisting of 839 packages and 60 million lines of code.  To date, we
have discovered 108 exploitable bugs.  Our results indicate that model
checking can be both a feasible and integral part of the software
development process.