TC: Small: Compositional End-to-End Security for Systems

TC：小型：系统的组合式端到端安全性

• 批准号: 1018061
• 负责人: Anupam Datta
• 金额: $ 50万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-09-01 至 2015-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1018061&HistoricalAwards=false
• 关键词: TC; Small; Compositional; End; Security

Compositional security is a recognized central scientific challenge for trustworthy computing. Contemporary systems are built up from smaller components. However, even if each component is secure in isolation, the composed system may not achieve the desired end-to-end security property: an adversary may exploit complex interactions between components to compromise security. This project addresses this important problem by developing a general model of systems and adversaries and techniques for modular reasoning and design. A central idea is to view a trusted system in terms of the interfaces that the various components expose: larger trusted components are built by combining interface calls in known ways; the adversary is constrained to the interfaces it has access to, but may combine interface calls without restriction. At a technical level, we are developing an expressive concurrent programming language with recursive functions for modeling interfaces and higher-order data for modeling code obtained at run time, and a logic of programs to capture reasoning principles for compositional security. We are using this framework to develop a systematic basis for web security, to formalize attacker models for web browsers proposed in literature and develop new ones, and to build an understanding of relevant security policies, end-to-end security properties, attacks in the wild, and ways to defend and prove web applications secure against these attacks. This study could have impact on security mechanisms and policies used in web applications in practice. The reasoning methods developed in the project will be mechanized in a tool.

组合安全性是公认的可信计算的核心科学挑战。现代系统是由更小的部件组成的。然而，即使每个组件都是独立安全的，组合的系统也可能无法实现期望的端到端安全属性：攻击者可能会利用组件之间的复杂交互来破坏安全性。该项目通过开发系统和对手的通用模型以及模块化推理和设计技术来解决这个重要问题。核心思想是根据各种组件公开的接口来查看可信系统：通过以已知方式组合接口调用来构建较大的可信组件；攻击者被限制到它可以访问的接口，但可以不受限制地组合接口调用。在技术层面上，我们正在开发一种表达性的并发编程语言，它具有用于接口建模的递归函数和用于在运行时获得的代码建模的高阶数据，以及用于捕获用于组合安全性的推理原则的程序逻辑。我们正在使用这个框架来开发web安全的系统基础，将文献中提出的web浏览器攻击者模型形式化并开发新的攻击者模型，并构建对相关安全策略、端到端安全属性、野外攻击以及防御和证明web应用程序免受这些攻击的方法的理解。本研究对实际应用中使用的安全机制和策略有一定的影响。在项目中开发的推理方法将在一个工具中机械化。