In seL4: Formal Verification of an Operating-System Kernel, Communications of the ACM, June, 2010 Klein et al

...report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code.

seL4 is a third-generation microkernel of L4 provenance, comprising 8,700 lines of C and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.

We prove that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as that the kernel will never crash, and it will never perform an unsafe operation. It also implies much more: we can predict precisely how the kernel will behave in every possible situation.

Overall the paper is more of an experience report than an in depth exploration of the kernel and its proofs but there is a some meat to be found. More information can be found at the sel4 website.

## Recent comments

3 min 21 sec ago

1 hour 43 min ago

11 hours 41 min ago

11 hours 46 min ago

15 hours 49 min ago

16 hours 9 min ago

16 hours 44 min ago

17 hours 5 min ago

19 hours 40 min ago

20 hours 26 min ago