Lightweight model checking for improving software security

Software assurance is a grand challenge in computer security; software vulnerabilities are responsible for many recurring attacks on computer systems. However, developers have few effective means of improving software security. Manual code inspection is tedious and unreliable. Complete formal verification is an automated approach that provides high assurance for software systems, however, it does not scale to large programs and it requires high expertise for writing specifications. As a result, software developers acutely need an effective yet practical approach that they can use for discovering and preventing security bugs in software development process.; This dissertation shows that lightweight model checking is an effective, practical approach for improving software security. First, we designed a formal framework for checking source code for violations of security properties. Then, we implemented the framework in a tool called MOPS and developed the following key features for making MOPS practical: it scales to large programs; it allows ordinary programmers to write specifications; it reports concise, comprehensive error traces; and it integrates into software build process automatically. To validate our design goal of MOPS, we used MOPS to audit both application and kernel code: we ran MOPS on 60 million lines of C programs in RedHat Linux, during which we discovered dozens of security bugs, and we used MOPS to verify design invariants in the EROS kernel.; Our success shows that lightweight model checking is a powerful, practical approach for improving security of large software systems.