TWC: Small: Using a Capability-Enhanced Microkernel as a Testbed for Language-based Security (CEMLaBS)

TWC：小型：使用功能增强的微内核作为基于语言的安全性的测试平台 (CEMLaBS)

• 批准号: 1422979
• 负责人: Mark Jones
• 金额: $ 32.44万
• 依托单位: Portland State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-10-01 至 2018-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1422979&HistoricalAwards=false
• 关键词: TWC; Small; Using; Capability; Enhanced

This project is investigating the potential for language-based security techniques in the construction of low-level systems software. The specific focus is on the development of an open, capability-enhanced microkernel whose design is based on seL4, a "security enhanced" version of the L4 microkernel that was developed, by a team in Australia, as the first fully verified, general purpose operating system.The work on seL4 is rightly celebrated as a landmark for formal verification, and provides a strong foundation for building trustworthy systems. The costs of its development and maintenance, however, are quite high. We have observed that many of the security properties established in the seL4 verification (including the absence of code injection attacks, buffer overflows, and null pointer dereferences) could have been guaranteed automatically by writing it in a language that incorporates language-based security mechanisms such as an enhanced type system. Motivated by such insights, the specific goals of this project are to evaluate: whether it is actually feasible to write software of this kind in a language with meaningful, language-based security guarantees; what practical impact this might have, particularly in reducing verification costs; and whether it is possible to meet the performance goals that aretypically required in such applications.The primary impact of this project will be in increasing the applicability of verification and language-based security techniques for the construction of secure computer systems. It will also generate and distribute key artefacts including the microkernel implementation, with associated teaching materials, for use in education, research, and industry.

该项目正在研究低级系统软件构建基于语言的安全技术的潜力。 具体的重点是开发一个开放的，功能增强的微孔，其设计基于SEL4，该版本的“安全性增强”版本的L4微粒，该版本是由澳大利亚的一个团队开发的，是第一个完全验证的通用操作系统。在SEL4上的第一个全面验证的，对SEL4上的工作是正确庆祝的正式验证的地标，并为建筑物提供了强大的基础，可以建立信任系统。 但是，其开发和维护的成本很高。 我们已经观察到，可以通过以一种结合基于语言的安全机制（例如增强的类型系统）的语言来自动保证，可以自动保证SEL4验证中建立的许多安全属性（包括没有代码注射攻击，缓冲区溢出和空指针效率）。 在这种见解的推动下，该项目的具体目标是评估：用具有有意义的，基于语言的安全性保证的语言编写此类软件是否实际上是可行的；这可能会产生什么实际影响，尤其是在降低验证成本方面；以及是否有可能实现此类应用程序中型的性能目标。该项目的主要影响将是增加验证和基于语言的安全技术在构建安全计算机系统中的适用性。 它还将生成和分发关键的人工制品，包括微核实施以及相关的教材，用于教育，研究和行业。