Comprehensive Formal Verification of an OS Microkernel

Provided by: Association for Computing Machinery
Topic: Hardware
Format: PDF
The authors present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel. They discuss the kernel design they used to make its verification tractable. They then describe the functional correctness proof of the kernel's C implementation and they cover further steps that transform this result into a comprehensive formal verification of the kernel: a formally verified IPC fast path, a proof that the binary code of the kernel correctly implements the C semantics, a proof of correct access-control enforcement, a proof of information-flow noninterference, a sound worst-case execution time analysis of the binary, and an automatic initialiser for user-level systems that connects kernel-level access-control enforcement with reasoning about system behavior.

Find By Topic