How to Prove your Kernel Secure: putting the "s" into seL4 -- provably
Toby Murray
Abstract:
Implementation-level proofs of operating system security have been a dream for at least 30 years. We present recent work on verifying security properties of the seL4 microkernel, the results of which are security theorems that hold for seL4's C code implementation asserting that it enforces authority confinement, integrity and information flow security (confidentiality). To our knowledge, these are the first such security theorems that hold for the implementation of a general-purpose kernel.
We describe how to capture and tame seL4's dynamic capability-based access control mechanism in a formal model of access control, which the kernel's implementation provably enforces. We then phrase integrity and confidentiality with reference to this model and prove them against seL4's abstract functional specification. We obtain code level theorems by virtue of the earlier functional correctness verification of seL4, because our security properties are preserved by refinement. Finally, we consider the implications and limitations of these results: "what do they mean and how much assurance do they provide?"
Bio: Toby Murray is a researcher with NICTA, whose interests focus on how to apply formal methods and verification to build more secure systems. He recently led the successful verification of information flow security for the seL4 microkernel, the result of which was the world's first proof of confidentiality that applied to the implementation of a general-purpose OS kernel. He previously completed a DPhil (PhD) at Oxford under the supervision of Gavin Lowe, researching the application of the process algebra CSP to reason about the security of object-capability patterns, and has also worked for the Australian Defence Science and Technology Organisation (DSTO), researching and building security architectures for pervasive systems.