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.
CAREER: Foundational Theories and Enforcement Tools for Secure Software Systems