MCS:
The L4.verified Proofs
This is the L4.verified git repository with formal specifications and proofs for the seL4 microkernel.
Most proofs in this repository are conducted in the interactive proof assistant Isabelle/HOL. For an introduction to Isabelle, see its official website and documentation.
Setup
This repository is meant to be used as part of a Google repo setup. Instead
of cloning it directly, please follow the directions for software dependencies
and Isabelle installation in the setup.md file in the docs
directory.
Contributing
Contributions to this repository are welcome.
Please read CONTRIBUTING.md for details.
Overview
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:
design: the design-level specification of seL4, generated from the Haskell model.c: the C code of the seL4 kernel, preprocessed into a form that can be read into Isabelle. This is generated from the seL4 repository.
-
-
proof: the seL4 proofsinvariant-abstract: invariants of the seL4 abstract specificationrefine: refinement between abstract and design specificationscrefine: refinement between design specification and C semanticsaccess-control: integrity and authority confinement proofsinfoflow: confidentiality and intransitive non-interference proofsasmrefine: Isabelle/HOL part of the seL4 binary verificationdrefine: refinement between capDL and abstract specificationsep-capDL: a separation logic instance on capDLcapDL-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 prototypelevityrefactoring tool, and others. -
tools: larger, self-contained proof toolsasmrefine: the generic Isabelle/HOL part of the binary verification toolc-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 abovehaskell-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.
Hardware requirements
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.
Running the Proofs
If Isabelle is set up correctly, a full test for the proofs in this repository
for seL4 on the ARM architecture can be run with the command
L4V_ARCH=ARM ./run_tests
from the directory l4v/.
Set the environment variable L4V_ARCH to one of ARM, ARM_HYP, X64,
RISCV64, or AARCH64 to get the proofs for the respective architecture. ARM
has the most complete set of proofs, the other architectures tend to support
only a subset of the proof sessions defined for ARM.
Not all of the proof sessions can be built directly with the isabelle build
command. The seL4 proofs depend on Isabelle specifications that are generated
from the C source code and Haskell model. Therefore, it is recommended to always
build using the run_tests command or 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 make <session-name>.
For example, to build the abstract specification, do
export L4V_ARCH=ARM
cd l4v/spec
make ASpec
See the HEAPS variable in the corresponding Makefile for available targets.
The sessions that directly depend on generated sources are ASpec, ExecSpec,
and CKernel. These, and all sessions that depend on them, need to be run using
run_tests or make.
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 and their dependencies, 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 on ARM, note that in proof/ROOT the parent session for
AInvs is ASpec and therefore run:
export L4V_ARCH=ARM
./run_tests ASpec
./isabelle/bin/isabelle jedit -d . -R AInvs
or, if you prefer make:
export L4V_ARCH=ARM
cd spec; make ASpec
../isabelle/bin/isabelle jedit -d . -R AInvs
in l4v/ and open one of the files in proof/invariant-abstract.