Information Flow
Motivation
The L4.verified project has proved that the seL4 microkernel is functionally correct. However, this proof does not, by itself, prove that seL4 is secure. For instance, it does not imply that two isolated subsystems, each of which does not possess any capabilities to the other nor to any shared resources, cannot send each other information, either directly or indirectly.
The information-flow project aims to prove properties about the absence of unwanted information flows within the seL4 kernel. These unwanted information flows include both direct information flows, such as when one thread is able to inadvertently modify the memory of a second when performing an IPC to a third thread, and indirect flows, such as those arising from covert storage and timing channels. This work is necessary in order to prove confidentiality and integrity properties about systems built on-top of seL4, such as the Secure Access Controller.
Overview
The information-flow project has two main thrusts. The first deals with proving the absence of unwanted direct information flows within seL4. This work aims to prove a theorem that states, for every kernel event and every object ob in the system, the set of objects that can affect ob when the event occurs (with all other objects being unable to affect ob here). An instance of this theorem might state that when one thread sends a message to a second, that no other objects in the system are affected other than the two threads in question (assuming that neither shares memory with a third). From this theorem, and an initial starting configuration for seL4, we will be able to deduce those events that can cause information to flow directly between otherwise isolated components. Ensuring the absence of such unwanted information flows will then be possible by ensuring that no such events can ever occur. Proving the absence of such events can be done easily on a very abstract model of the system design, such as that used for the initial analysis of the Secure Access Controller and should even be able to be done automatically using model-checking.
The second thrust of this project involves dealing with indirect information flows within seL4, such as those that arise from covert storage and timing channels within the kernel. Its aim is to prove the absence of covert storage channels, and to limit the bandwidth of covert timing channels within seL4. This work also includes an investigation of scheduling mechanisms to ensure temporal isolation of subsystems.
Status
The information-flow project is presently in its very early stages. To date we have constructed a formal framework which allows us to reason about direct information flows within seL4. This includes a refinement-closed formulation of the absence of direct information flow. However, work is yet to begin on applying this framework to the kernel models created during the L4.verified project, in order to prove theorems about the absence of unwanted direct information flows within seL4.
We have also begun some initial investigations regarding applying specific scheduling policies to limit the bandwidth of remotely exploitable timing channels. This work will involve building both practical demonstrations of such channels, and their mitigation, as well as producing theoretical models that can be used to reason about such channels.