1<!-- 2 Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 4 SPDX-License-Identifier: CC-BY-SA-4.0 5--> 6 7The Abstract Specification of seL4 8================================== 9 10 l4v/spec/abstract/ 11 12This directory contains the main Isabelle sources of the seL4 abstract 13specification. The specification draws in additional interface files from 14`design` and `machine`. 15 16The specification is written in monadic style. See 17`l4v/lib/Monad_WP/NonDetMonad` for the definition of this monad. 18 19Top-Level Theory 20---------------- 21 22The top-level theory file that draws the whole specification together is 23`Syscall_A`, the top-level function in that theory is `call_kernel`. 24 25This top-level function defines in-kernel behaviour. Later in the proof, 26in particular in `invariant-abstract`, this function is further wrapped 27in an automaton that describes system behaviour. 28 29Entry Points 30------------ 31 32Two useful entry points for browsing the abstract specification are the 33theories `Structures_A` and `ARM_Structs_A`. They define the state space 34of the kernel model, including what capabilities and kernel objects are. 35 36The theories `Invocations_A` and `ArchInvocation_A` define datatypes for 37the capability invocations/operations the kernel understands. 38 39Most theories are named after the subsystem of the kernel they specify. 40 41Building 42-------- 43 44The corresponding Isabelle session is `ASpec`. It is set up to build a 45human-readable PDF document. `Glossary_Doc` contains definitions of common 46seL4 terms. 47 48To build, run in directory `l4v/spec`: 49 50 make ASpec 51 52Remarks 53------- 54 55 * Note that this specification is actually an extensible _family_ of 56 specifications, with predefined extension points. These points can 57 either be left generic, as for most of the abstract invariant proofs, 58 or they can be instantiated to more precise behaviour, such as in 59 the theory `Deterministic_A`, which is used for the information flow 60 proofs. 61 62 * The theory `Init_A` *does not* define real kernel initialisation. 63 Instead it is a dummy initial state for the kernel to demonstrate 64 non-emptiness of abstract kernel invariants. 65 66 * `KernelInit_A` is a paused project and not currently included in 67 the rest of the specification. 68 69