This project addresses the problem that, to be trustworthy yet practical, mechanisms for enforcing software security must (1) undergo rigorous analysis that provides formal security guarantees and (2) be developed quickly. The project addresses this problem by creating (1) formal, foundational theories of software security and (2) convenient tools for quickly generating provably sound enforcement mechanisms. The foundational theories consist of formal definitions and rules for precisely specifying and reasoning about general security principles: threats, policies, mechanisms, and the means by which mechanisms enforce policies to prevent attacks. These theories aim to enable researchers and developers to analyze real mechanisms precisely and to prove which attacks those mechanisms can and cannot prevent in practice. The enforcement tools consist of technologies for converting expressive specifications of policies to be enforced into concrete mechanisms guaranteed to enforce those policies. These tools aim to enable researchers and developers to quickly and conveniently define, concretize, and deploy new security mechanisms. The enforcement tools and foundational theories are connected in that the theories provide models in which to establish the trustworthiness of tool-generated mechanisms. Taken together, these research tasks for creating and connecting theories and tools enable rapid development and deployment of trustworthy enforcement mechanisms for secure software systems.
This project aimed to improve the security of software. We used two approaches. The first approach involved modeling and analyzing attacks and how mechanisms can prevent those attacks. The second approach involved educating students to understand how their software can be attacked and how to make their software more secure. The research outcomes have included new systems for preventing computer attacks: We have uncovered new ways for attackers to steal or delete information from databases, like credit cards or medical records, using ordinary web browsers. We have also created and published mechanisms for preventing these new attacks. We have modeled certain kinds of security mechanisms, like anti-virus software, that work by monitoring other programs. We have proved fundamental limits to how helpful such security mechanisms can be. For example, software monitors can never fully prevent certain kinds of denial-of-service attacks. We have created and tested several systems for enforcing customizable policies. With these systems, users can customize the security and privacy constraints they want to impose on software. For example, users may want to enforce very strict privacy policies when they're off duty, but still allow their employers to track and monitor their work activities when they're on duty. We have implemented many systems to help users create and customize these sorts of policies. All of our implementations can be downloaded online for free. The educational outcomes have included security training for many students: An estimated 140 students have enrolled in a new course developed for this project. The course, being offered at the University of South Florida, is called "Foundations of Software Security". The course covers all the basics of how software can be attacked and defended. Many of the course's alumni have gone on to work at contractors for the US Department of Defense, or to work as security engineers at commercial software vendors. This project has directly funded at least 9 students, all of whom received one-on-one, hands-on training in software security. After graduation, these students have accepted jobs at companies like American Express (helping to secure mobile-payment systems), Epic Systems (helping to secure medical records), and Mozilla (helping to secure web browsers). Because this project is a CAREER award, the funding also played a major role in establishing the Principal Investigator as a long-term faculty member. The project's funding has thus enabled the Principal Investigator to train many additional students---students who have not been funded directly by the project but who have nonetheless received one-on-one, hands-on training with the Principal Investigator. Since 2007, the Principal Investigator has supervised and trained a total of 80 independent-study and thesis students. These 80 students have received valuable training by completing hands-on projects in the areas of programming languages and software security. By improving our understanding of attacks and how to prevent attacks, and by teaching that understanding to the next generation of programmers and system engineers, this project has helped to improve the security of software.
