CapDL initialiser for seL4

This repository contains the capDL initialiser for seL4.

The capDL initialiser is the root task for a seL4 system that takes a description of the state to be initialised using capDL, and starts the system in conformance with the specification.

The code is an implementation of the formal algorithm specified in Isabelle/HOL.

Repository overview


The capDL loader uses capDL-tool to generate a data structure containing the capDL specification to be initialised.

The formal model for the capDL initialiser is documented in ICFEM ‘13 paper and Andrew Boyton’s PhD thesis.


The files in this repository are release under standard open source licenses. Please see individual file headers and the LICENSE_BSD2.txt file for details.

File included from github repo edit