capDL Loader

The capDL loader is a C program that is intended to run as the initial root task in a system. It creates seL4 kernel objects and capabilities according to a declarative capDL specification.

Formal Correctness

The capDL loader is an implementation of an algorithm that is formally specified and proved correct (on the model level, but not the implementation level) in the theorem prover Isabelle/HOL.

The correctness statement is that the loader will bring the system into a state that contains only the capabilities and objects in the capDL specification in addition to capabilities that remain inert in the loader’s capability space after it has terminated. The input capDL specification must satisfy certain wellformedness criteria for this theorem to hold. They are documented in the formal definition in the verification repository.

The formal model for the capDL initialiser is documented in a research publication by Boyton et al (2013), as well as in Boyton’s PhD thesis (2014).

The Isabelle formalisation is part of the seL4 proofs that are continually updated and maintained in the l4v repository.

Implementation and use

The implementation of the capDL loader is comparatively small. It consists entirely of the following three source files:

• src/main.c: The implementation of the initialiser.
• include/capdl.h: C type definitions for capDL specifications.
• include/capdl_spec.h: Interface link point for the input capDL spec.

The capDL loader expects to be linked against an object file that contains the input capDL specification for the symbol extern CDL_Model capdl_spec. Typically, this would be a C file that is generated by the capDL translator tool from a textual or XML capDL specification.

The C loader contains more features than the formal model allows in wellformed specifications. The formal verification does not hold for these features, but they remain usable. For instance, they can be used for debugging and prototyping or for systems that do not require formal verification.

The capDL loader is used in CAmkES applications as the system initialisation task, and is invoked as part of the CAmkES build in all of the CAmkES examples.

Expecting to be linked against the specification can be limiting for some build system setups, because the specification must be compiled against the capDL loader sources. We would welcome contributions that allow providing the specification at runtime instead.