Robigalia: An Operating System for the Modern Era

By Corey Richardson

TODO: rewrite more defensively.

Current user operating systems such as GNU/Linux and Windows have proven themselves not up to the task of secure application development. They encourage ad hoc design and make it challenging for programs to communicate securely. Mark Miller, in his dissertation "Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control", describes an architecture for building applications using object capability systems. These systems have, by construction, properties which make it much easier to write programs and components which can compose constructively rather than destructively. They provide the ability to isolate programs and ensure their privilege is limited to the minimum required for their proper functioning. These ideas have taken hold in newer operating systems like Android and, to a limited extent, iOS and macOS. (CITE: EROS, iOS reference?, Android Binder)

Meanwhile, in the operating systems space, microkernels have been improving dramatically since the original implementations. Third-generation microkernels such as seL4 are built entirely around capability systems for secure communication. They are small, usually less than 10k lines of code, and have formal mathematical specifications of their behavior. In the case of seL4, the entire implementation is verified to meet its specification. This is not at the expense of performance: seL4 is one of the highest performing kernels of any kind. Building on this foundation, it is possible to achieve a small trusted code base (TCB) upon which robust systems can be built.

Programming languages have also made significant advances in the past decades. The Rust programming language brings many concepts from the academic realm into an industry-ready programming language. Using affine types, algebraic datatypes, type classes, and regions, it offers the ability to write safe high-performance programs with minimal memory management overhead and at a high level of abstraction relative to languages like C++.

These themes run throughout the ideas behind Robigalia: formal methods, capability systems, and programming languages. This is not new, or ground-breaking. But it is our hope that we can provide a practical, usable system as an example of what a modern capability operating system could look like.