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.
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.