adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/spec/abstract
History
Gerwin Klein 66e67fdd77 aarch64 haskell+aspec: finalise_cap for VSpace 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2022-04-20 09:16:19 +10:00
..
AARCH64 aarch64 haskell+aspec: finalise_cap for VSpace 2022-04-20 09:16:19 +10:00
ARM spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
ARM_HYP arm_hyp aspec+haskell: call vcpu_switch in associate_vcpu_tcb 2022-03-08 21:49:10 +10:30
RISCV64 spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
X64 spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
document aarch64 aspec: initial setup from RISCV64 2022-04-20 09:16:19 +10:00
CSpaceAcc_A.thy various: resolve some existing fixmes 2021-07-22 10:44:43 +10:00
CSpace_A.thy spec proof: resolve_address_bits'.simps[simp del] 2020-11-09 17:18:41 +11:00
CapRights_A.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Decode_A.thy spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
Deterministic_A.thy spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
ExceptionTypes_A.thy aspec+ainvs: remove interrupt/irq from p_monad 2020-10-25 13:15:00 +11:00
Exceptions_A.thy aspec+ainvs: remove interrupt/irq from p_monad 2020-10-25 13:15:00 +11:00
Glossary_Doc.thy aspec: include doc build in ASpec again 2020-10-27 15:52:31 +10:00
Interrupt_A.thy spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
Intro_Doc.thy aspec: include doc build in ASpec again 2020-10-27 15:52:31 +10:00
InvocationLabels_A.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Invocations_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
IpcCancel_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
Ipc_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
KHeap_A.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
KernelInit_A.thy arm+arm-hyp: kernelBase and physMappingOffset renames 2020-11-16 16:52:40 +11:00
MiscMachine_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
Retype_A.thy spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
Schedule_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
Structures_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
Syscall_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
TcbAcc_A.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Tcb_A.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
VMRights_A.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00

README.md

The Abstract Specification of seL4

l4v/spec/abstract/

This directory contains the main Isabelle sources of the seL4 abstract specification. The specification draws in additional interface files from design and machine.

The specification is written in monadic style. See l4v/lib/Monad_WP/NonDetMonad for the definition of this monad.

Top-Level Theory

The top-level theory file that draws the whole specification together is Syscall_A, the top-level function in that theory is call_kernel.

This top-level function defines in-kernel behaviour. Later in the proof, in particular in invariant-abstract, this function is further wrapped in an automaton that describes system behaviour.

Entry Points

Two useful entry points for browsing the abstract specification are the theories Structures_A and ARM_Structs_A. They define the state space of the kernel model, including what capabilities and kernel objects are.

The theories Invocations_A and ArchInvocation_A define datatypes for the capability invocations/operations the kernel understands.

Most theories are named after the subsystem of the kernel they specify.

Building

The corresponding Isabelle session is ASpec. It is set up to build a human-readable PDF document. Glossary_Doc contains definitions of common seL4 terms.

To build, run in directory l4v/spec:

make ASpec

Remarks

  • Note that this specification is actually an extensible family of specifications, with predefined extension points. These points can either be left generic, as for most of the abstract invariant proofs, or they can be instantiated to more precise behaviour, such as in the theory Deterministic_A, which is used for the information flow proofs.

  • The theory Init_A does not define real kernel initialisation. Instead it is a dummy initial state for the kernel to demonstrate non-emptiness of abstract kernel invariants.

  • KernelInit_A is a paused project and not currently included in the rest of the specification.