The Software Security Project
Studying how to secure our software infrastructure


We are studying how to secure software against malicious attack. In particular, we are investigating tools for identifying and eliminating security vulnerabilities in legacy systems, techniques to prove the absence of such vulnerabilities, and ways to help programmers avoid security holes when developing new software. We are especially interested in open source software as a platform for empirical evaluation of these techniques.

We rely heavily on techniques from static analysis, model checking, and related fields. A key selling point of these static techniques for source code analysis is that they allow us to proactively eliminate or neutralize security bugs before they are deployed or exploited.


Project participants include David Wagner, Hao Chen, Rob Johnson, and Umesh Shankar. We are actively collaborating with others, including Berkeley's Open Source Quality group and security researchers at SRI.

Enforcing rules of good programming practice

We are investigating model checking as a technique for enforcing programming disciplines designed to improve security. Our approach is to select appropriate principles of good coding practice that reduce the odds of falling prey to certain classes of common security flaws, express these principles as properties in a temporal logic that can be model-checked effectively, and build a tool to verify that source code obeys these rules.

We are currently applying these techniques to large open source software packages to evaluate their utility in practice. Further information may be found in a paper published at the ACM CCS conference:

MOPS: An Infrastructure for Examining Security Properties of Software
Hao Chen and David Wagner. To appear at ACM CCS 2002. [also available in pdf]
The following talk also contain highlights of the approach:
MOPS: MOdelchecking Security Properties
David Wagner. Summary talk at the CHATS Summer PI meeting. [also available in powerpoint]
Model Checking Software for Security Violations
Hao Chen, David Wagner, and Robert Johnson. Short talk at 2001 IEEE Symposium on Security and Privacy.
The tool, named MOPS, is now available in a public release.

Helping programmers deal with untrusted data

One reason that writing secure software is so hard is that programmers must handle data from untrusted sources with great care. We are building tools to help programmers with this error-prone task. Our approach is to extend the underlying type system to document the programmer's assumptions and to check that these are consistent with security.

We are collaborating with the Open Source Quality research group on this work. Further information may be found in a paper that was recently published at the Usenix Security conference:

Detecting Format String Vulnerabilities With Type Qualifiers
Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. 10th USENIX Security Symposium, 2001. [pdf]
The tool, named Cqual, has been publicly released.

Helping programmers understand and manage privileges

Another challenge in writing secure software is managing one's privileges. Security-critical programs often must juggle various forms of privileges, and this has unexpected pitfalls associated with it. We are working on techniques for helping programmers with this task and for automatically deriving models of the semantics of operating system API's for managing privileges (e.g., the setuid()-like system calls).

Further information may be found in a paper that has been accepted at the Usenix Security conference:

Setuid Demystified
Hao Chen, David Wagner, and Drew Dean. To appear at 11th USENIX Security Symposium, 2002. [pdf]
This work was done jointly in collaboration with a group at SRI.

Buffer overruns

As part of his Ph.D. work, Wagner developed techniques for automated detection of buffer overrun vulnerabilities The buffer overrun detection tool, named BOON, is now available in a public release.

Earlier work

Wagner's Ph.D. also described techniques for improving intrusion detection through static analysis. We will build on this experience as we continue to explore practical techniques for improving the quality of security-critical software.


This work is funded through generous support from a NSF CAREER award, a NSF ITR award, and substantial gifts from Microsoft. Previous donors include DARPA's CHATS program, an equipment grant from Intel, and an Okawa Foundation Award for 2000-2001.

David Wagner,,