Overview

After sixty years of operating systems evolution, we continue to find new and different isolation mechanisms: threads, processes, containers, virtual machines, lightweight contexts. Even applications provide isolation mechanisms: a JVM is a user-level process that provides isolation units whose API is Java bytecodes; some browsers offer units of isolation between each browser tab.

We ask whether we really need to have N different isolation mechanisms or whether instead, we could develop a model in which all these different mechanisms represent points on a continuum. If we could do that, then perhaps both compare and find new isolation mechanisms. The project has the following goals:

• Develop a theoretical model that depicts an isolation mechanism in a high dimensional space.
• Compare isolation mechanism using this model: Early result show that the model is a Graph, with nodes for resources, and protection domains, and there is a partial order between the different mechanism's depictions
• Explore the space to identify novel points that satisfy a desired performance, and security trade-off.
• Implement the model in seL4 and Linux: Wiki for the prototype OS CellulOS
• Formally verify the model in Verus.

Sid gave a lightning(gong) talk at HPTS2022 based on this work. A prior version of the model is in our Arxiv submission, and SOSP 2023 Poster. Stay tuned for the latest model.