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， seL4是L4微内核的“安全增强”版本，由澳大利亚的一个团队开发，作为第一个完全验证的通用操作系统。seL4上的工作被正确地视为形式化验证的里程碑，并为构建可信赖的系统提供了坚实的基础。然而，它的开发和维护成本相当高。我们已经观察到，在seL4验证中建立的许多安全属性（包括没有代码注入攻击、缓冲区溢出和空指针解引用）可以通过使用一种包含基于语言的安全机制（如增强的类型系统）的语言来编写来自动保证。基于这样的见解，这个项目的具体目标是评估：用一种有意义的、基于语言的安全保证的语言编写这种软件是否切实可行；这可能产生什么实际影响，特别是在减少核查费用方面；以及是否有可能满足此类应用程序中通常要求的性能目标。这个项目的主要影响将是增加核查和基于语言的安全技术在建立安全的计算机系统方面的适用性。它还将生成和分发关键的工件，包括微内核实现，以及相关的教学材料，用于教育、研究和工业。