Secure Microkernel Project (seL4)
The seL4 microkernel is a key enabler of our work. It provides a minimal and efficient lowest software level, and is the only part of our software that executes in the privileged mode of the hardware. It is a third-generation microkernel that builds on the strengths of the L4 microkernel architecture, such as small size, high performance, and policy freedom, and extends it with a built-in capability model, which provides a mechanism to enforce security guarantees at the operating system and application levels.
Why microkernel?
Trustworthiness of a system has a lot to do with its size. Even well-engineered code has of the order of several defects per thousand lines of code (loc). Hence, a bigger system has inherently more bugs than a small system.
This is particularly relevant for the kernel, as it is manages the hardware at the lowest level, and it is not subject to protection or fault isolation mechanisms provided by the hardware — in fact, it is responsible for controlling. Therefore any kernel bug is potentially fatal for the system—the kernel is always part of the trusted computing base (TCB). Minimising the exposure to faults means minimising the TCB, hence a small kernel.
L4 is one of the smallest general purpose kernels in existence and is known for its excellent performance, making it an ideal original starting for our work. The seL4 project has extended L4's applicability to application domains requiring strong security guarantees, and also made it more amenable to formal verification of correctness.
Overview of seL4
Strong security is a fundamental requirement for some existing and emerging embedded application domains and devices, such as personal digital assistants, mobile phones, and set-top boxes.
It is widely acknowledged that to build a secure system, security must be considered in all layers of the system—from hardware to software applications. It is also widely acknowledged that it is extremely difficult (if not impossible) to retrofit security mechanisms to an existing insecure system. Security is becoming a critical component of new embedded devices such as mobile phones, personal digital assistants, and set-top boxes. There is an expectation from users and service providers that such devices will store sensitive data owned by either party, i.e., data that either party wishes to control access to and dissemination of. Such devices are also expected to run third-party applications whose origin, quality and functionality is not directly or even indirectly controlled by the embedded-device supplier. Given that end-users are unlikely to be able or willing to identify applications of dubious nature (or outright malicious intent), any secure embedded system must be capable of enforcing security requirements between application instances on an individual device, in an environment where hostile applications are unknowingly installed by end users.
The susceptibility to viruses, trojan horses, ad-ware, and spyware of modern desktop platforms is largely due to the inability of the underlying base system to apply and enforce the principle of least authority, which undermines the ability of higher-level layers to provide security. The inability of users to finely control their own software results in uncontrolled propagation of viruses, the disclosure or modification of private data, or denial of service to the user. Attempts to secure platforms via various scanners, fire walls, and integrity checkers have been of only limited success, and largely unsatisfactory if one requires strong guarantees regarding control of their data.
seL4's provides the secure software base upon which further secure software layers (system and application services) can be composed to form a trustworthy embedded system. The system could be as simple as an industrial controller needing isolation between two activities it manages, or as complex as virtualisation infrastructure requiring strong isolation between the virtual machines it provides to clients. Both scenarios rely on the guarantees provided by the underlying kernel.
To provide a high degree of assurance of the guarantees, we have a strong collaboration with the NICTA Formal Methods and Logic and Computation programs in the form of the L4.verified project. A high degree of assurance can ultimately only be established by mathematical rigour.The collaboration has resulted in the formal modelling of the kernel's programming interface, and the formal verification of the implementation of the modelled interface. Ultimately, strong security guarantees are assured by mathematical proof, and the mathematical proof covers not only the design at differing levels of depth, but also the implementation of the design down to the programming language level.
The practical result of our work is the most trustworthy general purpose microkernel in the world.
Technical Information
Further technical details of the project are available here.
Availability
The evolution of seL4 is continuing within NICTA, and it is the basis of ongoing research activities here at NICTA. However, it is also the subject of commercialisation activities, and thus is currently proprietary. We are endeavouring to release seL4 in the future, but the time-line and exact nature of the release is yet to be decided. Stay tuned for further info.
