CT-T: Collaborative Research: Manifest Security

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

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.