Email Gateway (Aug 18 2022 at 16:52): Email Gateway (Aug 18 2022 at 16:52):From: Gerwin Klein <gerwin.klein@nicta.com.au>
It took some time, but NICTA and Open Kernel Labs have now released the formal Isabelle/HOL specification of the seL4 microkernel. The C code of the kernel is verified (in Isabelle) to implement this specification. The release includes ARM and x86 binaries of the kernel, documentation, user-level libraries and examples, and a paravirtualised Linux that runs on top of seL4/x86:
http://ertos.nicta.com.au/software/seL4/
The specification works with Isabelle2009-2, and the release contains all files and libraries necessary to process it in Isabelle.
Please note that the release is for non-commercial only. Educational and academic research use is explicitly allowed.
Cheers,
Gerwin
Last updated: Apr 19 2024 at 16:20 UTC