The last ten years have seen substantial progress in our ability to automatically analyze source code for security properties. These advances are transitioning into practice and making a broad impact on software security. However, the success of this work has been partially limited by the fact that there are many security properties that we do not know how to analyze.

This project seeks to take several initial steps towards extending the range and scope of security properties that can be checked on large software systems. The research involves three tracks. First, we will investigate how the design of programming languages can support secure programming practices. Second, we will study techniques for analyzing memory safety, a a complex yet fundamental security property that, surprisingly, is still not statically checkable today. Third, we will study how to check that networking software is consistent with the specifications implied in standards committees' descriptions of network protocols. Integrated together, these three directions will allow us to provide end-to-end guarantees of security properties that span from low to high level. The goal of this project is to begin the work of developing a future generation of techniques for improving software security.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Network Systems (CNS)
Type
Standard Grant (Standard)
Application #
0716715
Program Officer
Karl Levitt
Project Start
Project End
Budget Start
2007-10-01
Budget End
2008-09-30
Support Year
Fiscal Year
2007
Total Cost
$50,000
Indirect Cost
Name
University of California Berkeley
Department
Type
DUNS #
City
Berkeley
State
CA
Country
United States
Zip Code
94704