Our Partners

Provably Secure, General-Purpose Operating System

Aim

Develop the template of an operating sytem that is provably secure, yet able to scale to the power of mainstream systems such as Linux.

Context

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.

Background

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.

Objective

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:

1. security: the system shall provably enforce a security policy
2. policy diversity: the system shall support a wide range of (adaptable) security policies, suitable to military as well as commercial use cases
3. functionality: the system shall, in principle, be able to scale to functionality comparable to that of Linux
4. evolution: the system shall be able to adapt to new hardware and functional requirements
5. performance: the system shall be able to achieve performance comparable to that of Linux.

High-Level Design

The figure on the right shows the high-level architecture of the system. It has three core servers:

1. the security server maintains security state and is consulted on each security-relevant operation;
2. the resource manager, responsible for resource isolation and sharing
3. the connection server establishes and removes connections between active entities.

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.

Connections

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.

Resource management

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.

Policy enforcement

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.

Status

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.

Support

Initial work on the project was supported by UK's National Cyber Security Centre (NCSC) and Google.

Collaborations

We are collaborating with the group of Trent Jaeger at Penn State.

People