seL4: Formal Verification of an Operating-System Kernel.

We 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 8700 lines of C an...

Full description

Bibliographic Details

Published in:	Communications of the ACM Vol. 53; no. 6; pp. 107 - 116
Main Authors:	Klein, Gerwin, Andronick, June, Elphinstone, Kevin, Heiser, Gernot, Cock, David, Derrin, Philip, Elkaduwe, Dhammika, Engelhardt, Kai, Kolanski, Rafal, Norrish, Michael, Sewell, Thomas, Tuch, Harvey, Winwood, Simon
Format:	Article
Published:	Association for Computing Machinery Jun2010
Subjects:	Software verification Computer logic Computer software correctness Computer operating systems C (Computer program language) Computer science
Online Access:	View this record in EBSCOhost