1Separation Kernel Bisimilarity 2============================== 3 4This proof establishes that seL4, if configured fully statically with 1-level 5CSpaces and notification caps only, is bi-similar to a static separation 6kernel that has no other system calls than signalling notifications. 7 8Building 9-------- 10 11To build from the `l4v/` directory, run: 12 13 ./isabelle/bin/isabelle build -d . -v -b Bisim 14 15Important Theories 16------------------ 17 18Theory [`Separation`](Separation.thy) defines static configurations, and 19theory [`Syscall_S`](Syscall_S.thy) contains the proof that this is equivalent 20to a static kernel. 21 22The definition of a static kernel API can be found in the `spec` directory 23under [`sep-abstract`](../../spec/sep-abstract/). 24