CAREER: Foundational Theories and Enforcement Tools for Secure Software Systems

职业：安全软件系统的基础理论和实施工具

• 批准号: 0742736
• 负责人: Jay Ligatti
• 金额: $ 33.11万
• 依托单位: University of South Florida
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-02-01 至 2014-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0742736&HistoricalAwards=false
• 关键词: CAREER; Foundational; Theories; Enforcement; Tools

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.

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