This research aims to develop tools and techniques to find and eliminate security vulnerabilities in software. The approach is based on static analysis, which by analyzing source code can model all possible executions of a program. The distinguishing feature of the project is to show that very large applications are free from classes of security vulnerabilities. Thus, the focus is not just in finding security holes in software, but in verifying their absence. Previous experience has shown that simple, approximate tools do not find all or even nearly all security vulnerabilities; the higher assurance given by verification is needed. The experimental goal is to apply these techniques to the Linux kernel, a security-critical application with millions of lines of code.
The main technical approach being investigated is based on user-defined type qualifiers that refine the standard types of the programming language. Previous work has shown that type qualifiers are a natural and useful way to explicitly specify desired security properties that are normally only implicit in a program. In much the same way that a correctly typed program cannot have run-time type errors, having consistent type qualifiers throughout a program implies that the property expressed by those qualifiers must hold in every execution. The significance of this work is that, if successful, it will improve the understanding of how to perform sophisticated static analysis of very large programs. The broader impact will be in discovering and repairing new security vulnerabilities in widely-used software infrastructure and in verifying that some of that infrastructure is free from at least some security flaws.
