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.