Technical Information
The seL4 project developed two closely intertwined results. The first result being the evolution of the L4 API into something capable of providing and reasoning about stronger security guarantees, and the other result being the exploration of an approach to specifying, and prototyping a microkernel API and implementation that is amenable to formal verification. The actual work specifically on formal verification of seL4 is covered in more detail on the L4.verified project pages.
Security
The security results of the seL4 project address two general areas that were lacking in the older L4 APIs: communication control between applications, and kernel physical memory management. Control of communication is critical for both providing isolation guarantees between subsystems, and providing confinement guarantees of information possessed by an application. Control of physical memory consumed by the kernel is critical for providing availability guarantees for kernel services, and also for the predictability of their execution times.
The capability model implemented by seL4 was inspired by secure operating systems like KeyKOS and EROS, and by capability machines such as the Cambridge CAP computer. The resulting seL4 design features an API that requires explicit authority for all operations — all system calls require an appropriate capability as an argument in order to perform the operation. Thus, like traditional capability systems, all authority an application possesses is determined by the capabilities it possesses.
The capability model has been modelled in the Isabelle interactive theorem prover, and the model has been proven capable of confining authority in a subsystem, and also isolating a subsystem, provided subsystems meet some simple and intuitive pre-conditions.
Our research has also extended the capability model to reason about and control kernel physical memory consumption. There is a direct correspondence between capabilities possessed by a subsystem and physical memory consumed by the subsystem. To state this another way — any security policy enforced via a specific capability distribution in the system, is also enforced internally within the kernel in its allocation of physical memory. This result is achieved by removing all implicit allocation of memory from the kernel, and providing a capability-based model of explicit allocation, which is performed by applications possessing the appropriate authority.
Summarising, seL4 has a precise and strong security model, based on capabilities, that encompasses both kernel services and in-kernel memory consumption. The security model can be used to instantiate systems with authority-confined or isolated subsystems, where the properties are enforced both at application level, and within the kernel itself.
Development for verification
On embarking on the seL4 project, we wanted an approach that had the following properties, while enabling the exploration of the design space of potential API solutions that achieve the goals outlined above.
- The resulting API specification must be precise. English manual-like descriptions are ambiguous and thus unsatisfactory.
- The approach must expose enough of the implementation details to allow the experimenter to be convinced that a high performance implementation is possible.
- It should provide a method for gaining experience and evaluating the construction of higher-level systems.
- It must be readily amenable to formalisation.
- The approach must also be usable by kernel programmers who are not adept in formal methods.
The approach taken was to use literate Haskell to specify and implement the seL4 API. Haskell, as a functional programming language, is not a large paradigm shift for typical kernel programmers compared to more formal specification alternatives such as the B-method. Haskell is side-effect free functional programming language that allows us to explore implementation details of the kernel using a pseudo-imperative style with the help of Monads.
For validation, to enable the API to be used without requiring a real kernel implementation together with all the debugging complexities of managing real hardware, we created a simulator that implements the ARM processor user-level instruction set. The simulator enables ARM application binaries to be executed. When an exception would normally be generated resulting in execution transfer to the kernel running in privileged mode (a system call for example), the simulator invokes the Haskell kernel specification directly, which proceeds to resolve the exception and gives the illusion that the application is running on real hardware with a kernel implementing the API specification.
We have successfully used the above approach to develop a working executable specification of a kernel. When combined with the simulator, we have an initial port of local basic application software. One should note that this executable specification is the low-level design model in the formal verification work, as the subset Haskell that we use is readily translatable into a model in Isabelle/HOL.
The Haskell artifact was used as a basis for manually developing a high-performance C programming language implementation of seL4 for ARM processors. The combination of the formal methods work and the practical use in the simulation environment gave us a high level of confidence in the design when translated into C.
Future work
We are currently working towards supporting seL4 on multiprocessors. The true concurrency present on multiprocessors makes the formal verification aspects of seL4 extremely difficult. The challenge is to minimise the concurrency while still efficiently supporting multiprocessors.
We also have ongoing work in evolving the security model, and making a formal connection between the model and an abstract model of the seL4 API. Eventually, we aim to develop a formal connection between interesting properties of the security model and the actual implementation in the C programming language in order to have extremely high assurance of security for systems constructed on seL4.