Develop the template of an operating sytem that is provably secure, yet able to scale to the power of mainstream systems such as Linux.
An operating system can only be considered secure in a strong sense if it can provably enforce a security policy.
seL4's provable enforcement of basic security (isolation) properties, confidentiality, integrity and availability is an enabler of such provable security. But so far this was only achieved for static architectures, such as the CDDC. Such static architectures can go a long way in embedded and cyberphysical systems, as we demonstrated in the DARPA HACMS and CASE projects. However, they are a far cry from the power of general-purpose operating systems, such as Linux. As long as we cannot get general-purpose systems secure, we have to live with insecure, unsafe and unreliable systems.
While the world at large seems to have given up on real security and consigned itself to live with inherently insecure system, we at TS we do not believe that this is an acceptable state. We are consequently working on demonstrating that a truly secure OS is possible.
The 1970s and '80s saw a number of attempts to produce a truly secure OS, notable examples are PSOS, SAT and VAX VMM. These systems failed to achieve the goal of provable security, as the formal methods available at the time could not scale to the task at hand.
Moreover, these systems were far from general purpose. They supported classical, but highly restrictive military-style hierarchical security policies, which do not map onto most commercial use cases. Furthermore, the design of those systems did not allow incorporating untrusted components into the OS, meaning that the complete OS functionality would have to be verified.
We aim to develop a prototype of a system that is secure yet deployable to a wide range of real-world use cases. This means that it must combine security with usability. Specifically, we aim to demonstrate that the system meets the following requirements:
The figure on the right shows the high-level architecture of the system. It has three core servers:
The core servers have strong mutual dependencies, they may or may not be implemented as separate processes, but the goal has to be that their correctness can be formally verified.
For simplicity, the diagram does not show connections to the connection server, which each task is given as part of the startup protocol. In order to obtain any service, a client needs to establish a connection to the corresponding server, using the connection server's connection establishment protocol.
The resource manager provides a resource container object abstraction, which represents an amount of a resource (initially only spatial resources, such as memory or persistent storage). Low-level system abstractions, such as connections, tasks and threads) are created by allocating them from a container object. Container objects can themselves be allocated from a container, this supports sharing a subset of resources.
In particular, sub-containers support resource donation: Object servers, such as file servers, generally need memory to store metadata for the objects they provide. A client must provide this memory to the server as part of the server's object creation protocol. The client only loans the resource to the server, it can revoke it at any time (implicitly destroying the object that uses the resource), the system's revocation protocol notifies the server of such a revocation.
Each object server has a policy enforcement module (PEM) which consults the security server on each security-sensitive operation. The security requirement of complete mediation implies that the object server will have to be verified to invoke its PEM whenever needed and obey the result, and that the PEM communicates correctly with the security server. The PEM itself is policy-free, security policy is only represented in the security server.
The security server itself has a policy store, which defines the current security policy, it only changes if the system's global security policy changes. The present security state of the system is stored separately, it changes frequently as subjects come and go or connections are established between previously unconnected components. The server's decision-making logic queries the policy and present security state on a request from a PEM, and potentially updates the security state before replying to the PEM.
The project is at an early state. We are presently developing the multi-server framework to the point where we can informally reason about its security and evaluate performance limitations.