secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
seL4-L4.verified/spec/sep-abstract
History
Corey Lewis fca3eaeff1 arm proof: update for det_ext refactor 
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
 		2025-05-01 10:55:20 +10:00
..
Decode_SA.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Ipc_SA.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
README.md READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
Syscall_SA.thy arm proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00

README.md

Static Separation Kernel API

This specification is a cut-down version of the seL4 abstract specification that removes all system calls apart from notifications. The resulting kernel is a classic static separation kernel without any dynamism.

A proof that seL4 is equivalent to this cut-down version if configured appropriately can be found in the proof directory under bisim.

Building

To build from the l4v/ directory for the ARM architecture, run:

L4V_ARCH=ARM ./run_tests ASepSpec

Important Theories

Theory Syscall_SA contains the top-level definition. The specification directly includes parts of the 'normal' abstract specification of seL4 from directory abstract.