This proof establishes that seL4 enforces information flow, and so enforces the security property of confidentiality. Information flow security is defined in terms of (intransitive) noninterference, and implies confidentiality: data cannot be inferred without appropriate read authority. This proof is described in a 2013 IEEE Symposium on Security and Privacy paper. This proof firstly establishes noninterference for seL4's abstract specification, building on top of the Access Control Proof, before transferring the noninterference result to the kernel's C implementation via the Design Spec Refinement Proof and the C Refinement Proof.
To build from the l4v/ directory, run:
./isabelle/bin/isabelle build -d . -v -b InfoFlow
The top-level theory where noninterference is proved for the seL4
abstract specification is Noninterference; it
is transferred to the C implementation via refinement in the theory
Noninterference_Refinement. The base
theory where noninterference is (generically) defined is
Noninterference_Base. The bottom-level
theory where confidentiality is formalised over the seL4 abstract
specification is InfoFlow. Confidentiality is
a relational property and the theory EquivValid
defines these generically for the nondeterministic state monad of the
abstract specification.