Name | Date | Size | ||
---|---|---|---|---|
.. | 30-Nov-2020 | 17 | ||
Arch_DR.thy | H A D | 30-Oct-2020 | 94.5 KiB | |
base/ | H | 30-Oct-2020 | 3 | |
CNode_DR.thy | H A D | 30-Oct-2020 | 132.4 KiB | |
Corres_D.thy | H A D | 09-Apr-2020 | 27.7 KiB | |
Finalise_DR.thy | H A D | 30-Oct-2020 | 174 KiB | |
Intent_DR.thy | H A D | 30-Oct-2020 | 96.5 KiB | |
Interrupt_DR.thy | H A D | 09-Apr-2020 | 29.7 KiB | |
Ipc_DR.thy | H A D | 30-Oct-2020 | 136.3 KiB | |
KHeap_DR.thy | H A D | 30-Oct-2020 | 167.4 KiB | |
Lemmas_D.thy | H A D | 09-Apr-2020 | 982 | |
MoreCorres.thy | H A D | 09-Apr-2020 | 4.7 KiB | |
MoreHOL.thy | H A D | 09-Apr-2020 | 347 | |
README.md | H A D | 30-Nov-2020 | 1.1 KiB | |
Refine_D.thy | H A D | 30-Oct-2020 | 2.3 KiB | |
Schedule_DR.thy | H A D | 30-Oct-2020 | 35.8 KiB | |
StateTranslation_D.thy | H A D | 30-Oct-2020 | 48.5 KiB | |
StateTranslationProofs_DR.thy | H A D | 30-Oct-2020 | 12.8 KiB | |
Syscall_DR.thy | H A D | 30-Oct-2020 | 82.5 KiB | |
Tcb_DR.thy | H A D | 30-Oct-2020 | 90.6 KiB | |
Untyped_DR.thy | H A D | 30-Oct-2020 | 87 KiB |
README.md
1<!-- 2 Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 4 SPDX-License-Identifier: CC-BY-SA-4.0 5--> 6 7CapDL Refinement Proof 8====================== 9 10This proof establishes that seL4's [abstract specification][aspec] is 11a formal *refinement* (i.e. a correct implementation) of its [capDL 12specification][capDL]. It is described as part of an ICFEM '13 13[paper][paper]. 14 15 [aspec]: ../../spec/abstract/ 16 [capdl]: ../../spec/capDL/ 17 [paper]: https://ts.data61.csiro.au/publications/nictaabstracts/Boyton_ABFGGKLS_13.abstract.pml "Formally Verified System Initialisation" 18 19Building 20-------- 21 22To build from the `l4v/` directory, run: 23 24 ./isabelle/bin/isabelle build -d . -v -b DRefine 25 26Important Theories 27------------------ 28 29The top-level theory where the refinement statement is established over 30the entire kernel is [`Refine_D`](Refine_D.thy); the state-relation that 31relates the state-spaces of the two specifications is defined in 32[`StateTranslation_D`](StateTranslation_D.thy) and the basic 33correspondence property proved over each kernel function is defined in 34[`Corres_D`](Corres_D.thy). 35 36