| <!-- |
| Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) |
| |
| SPDX-License-Identifier: CC-BY-SA-4.0 |
| --> |
| |
| # 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][Kuz_KLW_10], |
| and starts the system in conformance with the specification. |
| |
| The code is an implementation of the formal algorithm specified |
| in Isabelle/HOL. |
| |
| [Kuz_KLW_10]: https://ts.data61.csiro.au/publications/nicta_full_text/3679.pdf "capDL: A language for describing capability-based systems" |
| |
| ## Repository overview |
| |
| * [`src/main.c`](src/main.c): The implementation of the initialiser |
| * [`include/capdl.h`](include/capdl.h): The data structure for capDL. |
| |
| ## Dependencies |
| |
| The capDL loader uses `capDL-tool` to generate a data structure |
| containing the capDL specification to be initialised. |
| |
| ## Related papers |
| |
| The formal model for the capDL initialiser is documented in a |
| [ICFEM '13 paper][Boyton_13] and Andrew Boyton's [PhD thesis][Boyton_14]. |
| |
| [Boyton_13]: https://ts.data61.csiro.au/publications/nicta_full_text/7047.pdf "Formally Verified System Initialisation" |
| [Boyton_14]: https://ts.data61.csiro.au/publications/nicta_full_text/9141.pdf "Secure architectures on a verified microkernel" |
| |
| ## 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. |
