Model Checking An Entire Linux Distribution for Security ViolationsBenjamin Schwarz Hao Chen David Wagner{bschwarz, hchen, daw}@cs.berkeley.eduGeoff Morrison Jacob West{gmorrison, jwest}@fortifysoftware.comJeremy Lin ([email protected])WeiTu([email protected])University of California, BerkeleyAbstractSoftware model checking has become a popular tool forverifying programs’ behavior. Recent results suggest that itis viable for finding and eradicating security bugs quickly.However, even state-of-the-art model checkers are limitedin use when they report an overwhelming number of falsepositives, or when their lengthy running time dwarfs othersoftware development processes. In this paper we reportour experiences with software model checking for securityproperties on an extremely large scale—an entire Linux dis-tribution consisting of 839 packages and 60 million lines ofcode. To date, we have discovered 108 exploitable bugs.Our results indicate that model checking can be both a fea-sible and integral part of the software development process.1 IntroductionSoftware bugs are frequent sources of security vulnera-bilities. Moreover, they can be incredibly difficult to trackdown. Automated detection of possible security violationshas become a quickly-expanding area, due in part to the ad-vent of model checkin g tools that can analyze millions oflines of code [6].In this paper we d escribe our experience using MOPS,a static analyzer, to verify security properties in an entireLinux distribution. We use the following recipe for findingsecurity bugs: identify an important class of security vul-nerabilities, specify a temporal safety property expressingthe condition when programs are free of this class of bugs,and use MOPS to decide which programs violate the prop-erty. We have developed six security properties—expressedas finite state automata (FSAs)—and refined them to min-imize false positives while preserving high effectiveness.These properties aim at finding security bugs that arise fromthe misuse of system calls, often vulnerable interactionamong these calls. For example, time-of-check-to-time-of-use (TOCTTOU) bugs involve a sequence of two or moresystem calls acting on the same file (see Section 3.1).Our primary contribution is the scale of our experiment.We ra n MOPS on the entire Red Hat Linux 9 distribution,which contains 839 packages totaling 60.0 million lin esof code (counting total lines in all .h, .c,and.cc files).MOPS successfully analyzed 87% (732) of these packages;the remaining 107 packages could not be analyzed becauseMOPS’s parser cannot parse some files in these packages.To the best of our knowledge, our experiment is the largestsecurity audit of software using automated tools reported inthe literature. Model checking at this scale introduces majorchallenges in error reporting, build integration, and scalabil-ity. Many of these technical challenges have been addressedin our work; we show how to surmount them, and demon-strate that mode l checking is feasible and effective even forvery large software systems.As part of this experiment, we have worked out how toexpress several new security properties in a form that can bereadily model checked by existing tools. Earlier work de-veloped simple versions of some of these properties [6], butin the process of applying them at scale we discovered thatmajor revisions and refinements were necessary to capturethe full breadth of program ming idioms seen in the wild.Some of the properties checked in this paper are novel; forinstance, we introduce a TOCTTOU property that turnedout to be very effective in finding bugs. In our experiments,we focused on finding bugs rather than proving their ab-sence. Verification is difficult, especially since MOPS isnot completely sound because it does not yet analyze func-tion pointers and signals. However, we expect that our tech-niques could point the way to formal verification of the ab-sence of certain classes of bugs, as better model checkersare developed in the future.The technical contributions of this paper are threefold: 1)We show how to express six important security properties ina form that can be model checked by off-the-shelf tools; 2)We report on practical experience with model checking atProceedings of the 21st Annual Computer Security Applications Conference (ACSAC 2005) 1063-9527/05 $20.00 © 2005 IEEEa very large scale, and demonstrate for the first time thatthese approaches are feasible and u seful; 3) We measurethe effectiveness of MOPS on a very large corpus of code,characterizing the false positive and bug detection rates fordifferent classes of security bugs.The full version of this paper [1] contains further detailon our experiments, some of which is omitted from the con-ference version due to space constraints. MOPS is freelyavailable from mopscode.sourceforge.net.2 The MOPS Model CheckerMOPS is a static (compile time) analysis tool that modelchecks whether programs vio late security properties [7].Given a security property—expressed as a finite-state au-tomaton (FSA) by the user—and the source code for aprogram, MOPS determines whether any execution paththrough the program might violate the security property.In more detail, the MOPS process works as follows.First, the u ser identifies a set of security-relevant operations(e.g., a set of system calls relevant to the desired property).Then, the user finds all the sequences of these operationsthat violate the property, and encodes them using an FSA.Meanwhile, any execution of a program defines a trace,thesequence of security-relevant operations performed duringthat execution. MOPS uses the FSA to monitor program ex-ecution: as the program executes a security-relevant opera-tion, the FSA transitions to a new state. If the FSA enters anerror state, the program violates the security property, andthis execution defines an error trace.At its core, MOPS determines whether a program con-tains any feasible traces (according to the program’s sourcecode) that v iolate a security property (according to theFSA). Since this question is generally undecidable, MOPSerrs on the conservative side: MOPS will catch all the bugsfor this property (in other words, it is sound, subject tocertain requirements [7]), but it might also report spuri-ous warnings. This requires the user to determine manu-ally whether each error trace reported by MOPS representsa real security hole.Specification of Security Properties. MOPS provides acustom