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...

Descripción completa

Detalles Bibliográficos

Publicado en:	Communications of the ACM Vol. 53; no. 6; pp. 107 - 116
Autores principales:	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
Formato:	Artículo
Publicado:	Association for Computing Machinery Jun2010
Materias:	Software verification Computer logic Computer software correctness Computer operating systems C (Computer program language) Computer science
Acceso en línea:	Ver este registro en EBSCOhost