[Ed. I'm re-posting this, since it looks like I made a stupid typo the first time, which lead to the munging of the message's headers. Sorry for the inconvenience. This one should be correct... KRvW]
an interesting paper. the authors evidently have made MOPS an addon package to GCC, which is something i've advocated before (make tools easy to use and integrated with the build environment). http://www.cs.berkeley.edu/~hchen/paper/ndss04.html Authors Hao Chen, Drew Dean, and David Wagner. Source Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS), San Diego, CA, February 4--6, 2004. 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. ________ jose nazario, [EMAIL PROTECTED] http://monkey.org/~jose/ http://infosecdaily.net/
