Model Checking One Million Lines of C Code
(Posted by adam)
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!)
Bookmark this post: Posted by adam on January 14, 2005 at 6:12 PM
in Economics
, information security
. You can:
comment, view comments (1),
see trackbacks (0) or
search Technorati.
Comments
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.
Posted by: Iang | January 15, 2005 7:40 AM