|
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.
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:
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:
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:
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.
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.