Tutorial: Using the seL4 Microkernel
Gernot Heiser, Ivan Velickovic · 2023
The seL4 microkernel [3] is the first general-purpose operating system (OS) kernel with a formal proof of implementation correctness. By now, its verification covers functional correctness to the binary (taking the compiler out of the trust chain), proofs of security enforcement and worst-case execution-time bounds, and span three architectures (32-bit Arm and 64-bit RISC-V and x86) [1]. All this while featuring unbeaten performance. seL4 is now being deployed in safety- and security-critical systems around the world, and is backed by the non-profit seL4 Foundation [2].