CAREER: Foundational Theories and Enforcement Tools for Secure Software Systems

这个项目解决的问题是，为了可靠而又实用，实施软件安全的机制必须(1)经过严格的分析，提供正式的安全保证，以及(2)迅速开发。该项目通过创建(1)正式的软件安全基础理论和(2)用于快速生成可证明合理的执行机制的便利工具来解决这一问题。基本理论由正式定义和规则组成，用于精确指定和推理一般安全原则：威胁、策略、机制以及机制执行策略以防止攻击的方法。这些理论旨在使研究人员和开发人员能够准确地分析真实的机制，并在实践中证明这些机制可以阻止哪些攻击，以及不能阻止哪些攻击。实施工具包括将要实施的策略的表现性规范转换为保证实施这些策略的具体机制的技术。这些工具旨在使研究人员和开发人员能够快速方便地定义、具体化和部署新的安全机制。执行工具和基础理论是相互联系的，因为这些理论提供了建立工具生成机制的可信性的模型。总而言之，这些创建和连接理论和工具的研究任务使安全软件系统的可靠执行机制能够快速开发和部署。

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.