Technical Information
The seL4 project has developed into two closely intertwined tasks. The first task being the evolution of the L4 API into something capable of providing stronger security guarantees, and also the task of specifying, developing, and validating a microkernel API.
The security goals address two general areas that are lacking in the existing L4 API: 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.
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 unsatisfactory.
- The approach must expose enough of the implementation details to allow the experimenter to be convinced 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, and allows us to explore implementation details of the kernel if desired.
For validation, to enable the API to be used without requiring a real kernel implementation together with all the 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.
At the present time, we have an initial seL4 API in Haskell together with the simulator executing ARM binaries. We have formalised this implementation and are now further validating the API by attempting to prove the first security properties and at the same time porting our high-level application environment (Iguana) to the new platform.
As experienced in the design iterations so far, we expect to be able to readily adapt the API as we gain more experience with its use, without the time consuming debugging usually associated with kernel programming and without large time investments for tracking changes in the formalisation.