LCM: Large-Scale Capability Management

在操作系统的上下文中，功能是控制其他孤立组件之间交互的机制。基于能力的系统在学术研究的象牙塔中停留了很长一段时间，但到目前为止，它已成为在某种意义上至关重要的系统选择的技术基础，主要是在与安全相关的环境中。部署的例子是关键政府或军事机构或汽车计算机系统中的笔记本电脑和工作站计算机。基于能力的操作系统的例子包括L4/Fiasco和M3，这两种系统都是由德累斯顿工业大学创建的，目前仍在由德国工业大学和工业界开发。该项目的目标是分析是否可以构建非常大的系统，这些系统直接依赖于通过功能控制通信提供组件交互的底层系统。换句话说，如果可以构建一个可扩展的功能系统来支持非常大的“应用程序”系统。据我们所知，令我们吃惊的是，这个问题从来没有被探讨过。关键的挑战是结构和算法的设计和实现，这些结构和算法允许在大规模环境中保护和执行能力，提供基于能力的系统的关键操作，即委托和撤销，并且在出现故障时是健壮的。填补这一重要知识空白的努力已经开始（2017年初）。Pramod Bhatotia博士（共同申请人）在德累斯顿工业大学期间与Hermann博士教授Härtig （PI）一起，他的团队发明了L4/Fiasco和M3。第一种方法是基于构建SemperOS （M3能力系统的分布式变体，支持多达640个节点[6]）进行更专门的分析。在这个项目中，我们努力以更基本的方式分析这个问题。这一基本方法包括为大规模能力系统设计规范结构，对算法进行形式化描述和验证，以及基于模拟和实际实现的全面评估。

Capabilities - in the context of Operating Systems - are mechanisms to control the interaction of otherwise isolated components. Capability-based systems remained for a long time in the ivory tower of academic research but by now became the technical basis of choice for systems that are critical in some sense, mostly in a security-related context. Examples for deployments are laptop and workstation computers in critical government or military institutions or automotive computer systems. Among examples for capability-based operating systems are L4/Fiasco and M3, both systems have been created at TU Dresden and are still developed at TUD and in industry.The goal of the project is an analysis of whether or not very large systems can be built which directly rely on an underlying system that provides the interaction of components via capability-controlled communication. In other words, if a scalable capability system can be built that supports very large "application" systems on top. To the best of our knowledge and to our surprise, this question has never been approached. The key challenge is the design and implementation of structures and algorithms that allow to protect and enforce capabilities in a large scale environment, provide the key operations of capability-based systems, namely delegation and revocation, and are robust in the presence of failures. Efforts to fill this important gap of knowledge have been started (beginning of 2017) by Asst.Prof. Dr. Pramod Bhatotia (Co-applicant) during his time at TU Dresden, together with Prof. Dr. Hermann Härtig (PI), who’s team has invented both L4/Fiasco and M3.A first approach to the topic consisted of a more ad-hoc analysis based on building SemperOS – a distributed variant of the M3 capability system supporting up to 640 nodes [6]. In this project we strive to analyze the problem in a more fundamental way. This fundamental approach includes the design of a canonical structure for large-scale capability systems, formal descriptions and verification of algorithms, and a thorough evaluation based on simulations and real implementations.