CT-T: Collaborative Research: Manifest Security

CT-T：协作研究：明显的安全性

• 批准号: 0716469
• 负责人: Frank Pfenning
• 金额: --
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-09-15 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0716469&HistoricalAwards=false
• 关键词: CT; Collaborative; Research; Manifest; Security

The project proposes "manifest security" as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure software and to demonstrate its feasibility in practice.Manifest security applies to extensible software platforms, where it addresses two fundamental problems: (1) how to specify policies about what resources an extension may use and how it can handle sensitive data, and (2) how to enforce such policies. The project is developing a novel high-level logical specification language, encompassing both authorization properties for access control and information flow properties to restrict the use of sensitive data. Adherence to the specification is enforced by a combination of static and dynamic methods, and trustworthiness of the code is established by the explicit representation and verification of formal proofs. Such proofs make the security properties manifest.Because extensible systems are in widespread use (for example, in web browsers, office software, media players, games, virtual communities, and operating systems) the concept of manifest security has significant potential for broad impact. Rigorous verification methods based on logic and type theory are increasingly important to the software industry; the project advances the use of these methods to ensure security. Results from the research are released via publications and a software platform for secure browser extension, making advances accessible to researchers and practitioners. Results are being integrated into graduate and undergraduate teaching materials as well as courses at summer schools.

该项目提出将“清单安全”作为安全可扩展系统的一种新的架构原则。它的研究目标是为明显安全的软件开发理论基础并在实践中证明其可行性。清单安全适用于可扩展的软件平台，其中解决了两个基本问题：(1)如何指定关于扩展可以使用什么资源以及如何处理敏感数据的策略，以及(2)如何执行这些策略。该项目正在开发一种新的高级逻辑规范语言，包括访问控制的授权属性和限制敏感数据使用的信息流属性。对规范的遵守是通过静态和动态方法的组合来强制的，而代码的可信性是通过形式证明的显式表示和验证来建立的。由于可扩展系统被广泛使用(例如，在Web浏览器、办公软件、媒体播放器、游戏、虚拟社区和操作系统中)，清单安全的概念具有广泛影响的巨大潜力。基于逻辑和类型理论的严格验证方法对软件行业越来越重要；该项目推动了这些方法的使用，以确保安全性。研究结果通过出版物和用于安全浏览器扩展的软件平台发布，使研究人员和从业者能够获得进展。结果正在被纳入研究生和本科生的教材以及暑期学校的课程。