From sclist Thu Aug 19 13:57:09 2004
Received: from web1.nidhog.com (web1.nidhog.com [66.207.132.2])
by ping.echomatrix.net (8.12.9p1/8.12.3) with ESMTP id i7JHv9ph061205
for <[EMAIL PROTECTED]>; Thu, 19 Aug 2004 13:57:09 -0400 (EDT)
(envelope-from [EMAIL PROTECTED])
Received: (from [EMAIL PROTECTED])
by web1.nidhog.com (8.12.9p1/8.11.3) id i7JHvCdG064201
for [EMAIL PROTECTED]; Thu, 19 Aug 2004 13:57:12 -0400 (EDT)
(envelope-from [EMAIL PROTECTED])
Received: from naughty.monkey.org (naughty.monkey.org [65.23.81.140])
by web1.nidhog.com (8.12.9p1/8.11.3) with ESMTP id i7JHvCgX064146
for <[EMAIL PROTECTED]>; Thu, 19 Aug 2004 13:57:12 -0400 (EDT)
(envelope-from [EMAIL PROTECTED])
Received: by naughty.monkey.org (Postfix, from userid 6)
id 9CA80537583; Thu, 19 Aug 2004 13:56:48 -0400 (EDT)
Received: from localhost (localhost [127.0.0.1])
by naughty.monkey.org (Postfix) with ESMTP id 966C7537577
for <[EMAIL PROTECTED]>; Thu, 19 Aug 2004 13:56:48 -0400 (EDT)
Date: Thu, 19 Aug 2004 13:56:48 -0400 (EDT)
From: Jose Nazario <[EMAIL PROTECTED]>
To: [EMAIL PROTECTED]
Subject: [paper] Model Checking One Million Lines of C Code
Message-ID: <[EMAIL PROTECTED]>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Virus-Scanned: Secured by aspStation
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, ph.d. [EMAIL PROTECTED]
http://monkey.org/~jose/ http://infosecdaily.net/
