History

Gerwin Klein 6b9d9d24dd Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")		2018-08-20 09:06:35 +10:00
..
Decode_SA.thy	Isabelle2018: new "op x" syntax; now is "(x)"	2018-08-20 09:06:35 +10:00
Ipc_SA.thy	globally use session-qualified imports; add Lib session	2018-08-20 09:06:34 +10:00
README.md	terminology in comments: async ep -> notifications	2015-11-24 16:58:22 +13:00
Syscall_SA.thy	ARM bisim: proof update for user_context refactor	2018-03-08 18:41:28 +11: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, run:

./isabelle/bin/isabelle build -d . -v -b 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.