Model Checking One Million Lines of C Code

Implementation bugs in security-critical software are pervasive. Several authors have previously suggested model checking as a promising means to detect improper use of system interfaces and thereby detect a broad class of security vulnerabilities. In this paper, we report on our practical experience using MOPS, a tool for software model checking security-critical applications. As exam- ples of security vulnerabilities that can be analyzed using model checking, we pick five important classes of vulnera- bilities and show how to codify them as temporal safety properties, and then we describe the results of check- ing them on several significant Unix applications using MOPS. After analyzing over one million lines of code, we found more than a dozen new security weaknesses in im- portant, widely-deployed applications. This demonstrates for the first time that model checking is practical and use- ful for detecting security weaknesses at large scale in real, legacy systems.