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

Dependencies

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 a ICFEM ‘13 paper and Andrew Boyton’s PhD thesis.

License

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