Model Checking One Million Lines of C Code
Hao Chen, Drew Dean, and David Wagner have a paper of that name in Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS), pages 171–185, San Diego, CA, February 2004. Hao Chen’s papers page has powerpoint, PDF and PS, as well as this abstract:
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 examples
of security vulnerabilities that can be analyzed using model checking,
we pick five important classes of vulnerabilities and show how to
codify them as temporal safety properties, and then we describe the
results of checking 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 important,
widely-deployed applications. This demonstrates for the first time
that model checking is practical and useful for detecting security
weaknesses at large scale in real, legacy systems.
I’ve talked about MOPS before , as well as using source analysis for a signal, and some problems with that. Oh, and MOPS is in its second public release. More comments after I’ve played with it.
(Thanks, Mort!)
Have you come across any such tools for high level interpreted languages? When Gary chose Java & Perl, back in 95, it was partly for security reasons – we wanted interpreted high level languages – and partly for speed of development (faster coding also helps security by the indirect feedback of getting more code done and deployed).
Since then, they’ve more or less performed as expected, and I’m wondering what a tool would do. Security problems tend to fall into one of three categories: a) those where the programmer leaves in an application bug, b) those where the programmer hasn’t written with security in mind, and c) those where the language producer has made it insecure.
For example of a) one security program wasn’t checking for negative integers of amounts. Luckily the one that mattered was checking ;). For c), which is the largest component because it is so hard to address, lack of inter process communications represents a systemic hole in large Java deployments. For Perl, lack of proper signal handling resulted in weaknesses. Java especially is getting more insecure as time goes on as each new release builds on bad designs. C.f., JCE.