adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/bisim
History
Gerwin Klein 0cf64b5498
READMEs: use run_tests consistently in READMEs (#622) 
Avoid mixing `isabelle`, `make`, and `run_tests` invocations.
Standardise on `run_tests` and mention `L4V_ARCH` each time to
indicate that you can and should set `L4V_ARCH`.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2023-03-30 13:59:18 +11:00
..
document license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
README.md READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
Separation.thy spec proof: resolve_address_bits'.simps[simp del] 2020-11-09 17:18:41 +11:00
Syscall_S.thy proofs: hoare_pre_cont variable renamed 2023-02-09 11:46:51 +11:00

README.md

Separation Kernel Bisimilarity

This proof establishes that seL4, if configured fully statically with 1-level CSpaces and notification caps only, is bi-similar to a static separation kernel that has no other system calls than signalling notifications.

Building

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

L4V_ARCH=ARM ./run_tests Bisim

Important Theories

Theory Separation defines static configurations, and theory Syscall_S contains the proof that this is equivalent to a static kernel.

The definition of a static kernel API can be found in the spec directory under sep-abstract.