The computer security community has long advocated the concept of building multiple layers of defense to protect a system. Unfortunately, it has been difficult to realize this vision in the practice of software development, and software often ships with inadequate defenses, typically developed in an ad hoc fashion.
Developers face a number of challenges when protecting a software system with multiple layers of defense. They lack holistic frameworks in which to express policies and mechanisms for different software layers, automated tools to add these defenses, and tools to prove that software enhanced with defenses has an advertised level of assurance.
This project develops new techniques to retrofit software for defense in depth. It takes a comprehensive view of the problem, with an emphasis on automated, interactive tools that developers can use to identify site-level security goals, explore the design space of adding security mechanisms, and retrofit legacy code to enforce security policies in a manner that can be machine-verified for assurance. The project develops theory and tools for formal policy language design and validation, static and dynamic code analyses, interactive tools for developers to explore the design space of security, functionality and performance tradeoffs, and methods to formally verify the correctness of program transformations to introduce defenses such as authorization, attacker containment, and auditing mechanisms.
The broader impact stems from the improved security of systems and the reduced cost of achieving better security, also education activities in the form of summer schools for graduate, undergraduate and high-school students. The tools developed will be released to the public domain, benefiting software developers in the field.