This is the L4.verified git repository with formal specifications and proofs for the seL4 microkernel.
For software dependencies and Isabelle setup, see the
setup.md file in the
Contributions to this repository are welcome.
CONTRIBUTING.md for details.
The repository is organised as follows.
docs: documentation on conventions, style, etc.
spec: a number of different formal specifications of seL4
abstract: the functional abstract specification of seL4
sep-abstract: an abstract specification for a reduced version of seL4 that is configured as a separation kernel
haskell: Haskell model of the seL4 kernel, kept in sync with the C code
machine: the machine interface of these two specifications
cspec: the entry point for automatically translating the seL4 C code into Isabelle
capDL: a specification of seL4 that abstracts from memory content and concrete execution behaviour, modelling the protection state of the system in terms of capabilities. This specification corresponds to the capability distribution language capDL that can be used to initialise user-level systems on top of seL4.
take-grant: a formalisation of the classical take-grant security model, applied to seL4, but not connected to the code of seL4.
There are additional specifications that are not tracked in this repository, but are generated from other files:
proof: the seL4 proofs
invariant-abstract: invariants of the seL4 abstract specification
refine: refinement between abstract and design specifications
crefine: refinement between design specification and C semantics
access-control: integrity and authority confinement proofs
infoflow: confidentiality and intransitive non-interference proofs
asmrefine: Isabelle/HOL part of the seL4 binary verification
drefine: refinement between capDL and abstract specification
sep-capDL: a separation logic instance on capDL
capDL-api: separation logic specifications of selected seL4 APIs
lib: generic proof libraries, proof methods and tools. Among these, further libraries for fixed-size machine words, a formalisation of state monads with nondeterminism and exceptions, a generic verification condition generator for monads, a recursive invariant prover for these (
crunch), an abstract separation logic formalisation, a prototype of the Eisbach proof method language, a prototype
levityrefactoring tool, and others.
tools: larger, self-contained proof tools
asmrefine: the generic Isabelle/HOL part of the binary verification tool
c-parser: a parser from C into the Simpl language in Isabelle/HOL. Includes a C memory model.
autocorres: an automated, proof-producing abstraction tool from C into higher-level Isabelle/HOL functions, based on the C parser above
haskell-translator: a basic python script for converting the Haskell prototype of seL4 into the executable design specification in Isabelle/HOL.
misc: miscellaneous scripts and build tools
camkes: an initial formalisation of the CAmkES component platform on seL4. Work in progress.
sys-init: specification of a capDL-based, user-level system initialiser for seL4, with proof that the specification leads to correctly initialised systems.
Almost all proofs in this repository should work within 4GB of RAM. Proofs involving the C refinement, will usually need the 64bit mode of polyml and about 16GB of RAM.
The proofs distribute reasonably well over multiple cores, up to about 8 cores are useful.
We provide a jEdit macro that is very useful when working with large theory files, goto-error, which moves the cursor to the first error in the file.
To install the macro, run the following commands in the directory
mkdir -p ~/.isabelle/jedit/macros cp misc/jedit/macros/goto-error.bsh ~/.isabelle/jedit/macros/.
You can add keybindings for this macro in the usual way, by going to
Utilities -> Global Options -> jEdit -> Shortcuts.
Additionally, our fork of Isabelle/jEdit has an updated indenter which is more
proof-context aware than the 'original' indenter. Pressing
ctrl+i while some
apply-script text is selected should auto-indent the script while respecting
subgoal depth and maintaining the relative indentation of multi-line
Running the Proofs
If Isabelle is set up correctly, a full test for the proofs in this repository can be run with the command
from the directory
Not all of the proof sessions can be built directly with the
isabelle build command.
The seL4 verification proofs depend on Isabelle specifications that are
generated from the C source code and Haskell model.
Therefore, it's recommended to always build using the supplied makefiles,
which will ensure that these generated specs are up to date.
To do this, enter one level under the
l4v/ directory and run
For example, to build the C refinement proof session, do
cd l4v/proof make CRefine
As another example, to build the session for the Haskell model, do
cd l4v/spec make ExecSpec
HEAPS variable in the corresponding
Makefile for available targets.
Proof sessions that do not depend on generated inputs can be built directly with
./isabelle/bin/isabelle build -d . -v -b <session name>
from the directory
l4v/. For available sessions, see the corresponding
ROOT files in this repository. There is roughly one session corresponding to
each major directory in the repository.
For interactively exploring, say the invariant proof of the abstract specification with a pre-built logic image for the abstract specification and all of the invariant proof's dependencies, run
./isabelle/bin/isabelle jedit -d . -R AInvs
l4v/ and open one of the files in