LCM: Large-Scale Capability Management

点击翻译按钮获取中文摘要

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.