Skip navigation
Skip navigation

SeL4: Formal verification of an operating-system kernel

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

Description

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 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...[Show more]

dc.contributor.authorKlein, Gerwin
dc.contributor.authorAndronick, June
dc.contributor.authorElphinstone, Kevin
dc.contributor.authorHeiser, Gernot
dc.contributor.authorCock, David
dc.contributor.authorDerrin, Philip
dc.contributor.authorElkaduwe, Dhammika
dc.contributor.authorEngelhardt, Kai
dc.contributor.authorKolanski, Rafal
dc.contributor.authorNorrish, Michael
dc.contributor.authorSewell, Thomas
dc.contributor.authorTuch, Harvey
dc.contributor.authorWinwood, Simon
dc.date.accessioned2015-12-10T22:23:45Z
dc.identifier.issn0001-0782
dc.identifier.urihttp://hdl.handle.net/1885/52945
dc.description.abstractWe 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 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 behavior. 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.
dc.publisherAssociation for Computing Machinery Inc (ACM)
dc.sourceCommunications of the Association for Computing Machinery
dc.subjectKeywords: Abstract specifications; Assembly code; Formal verifications; Safety property; System kernel; Third generation; Specifications; Abstracting
dc.titleSeL4: Formal verification of an operating-system kernel
dc.typeJournal article
local.description.notesImported from ARIES
local.identifier.citationvolume53
dc.date.issued2010
local.identifier.absfor080199 - Artificial Intelligence and Image Processing not elsewhere classified
local.identifier.ariespublicationf2965xPUB260
local.type.statusPublished Version
local.contributor.affiliationKlein, Gerwin, National ICT Australia
local.contributor.affiliationAndronick, June, University of New South Wales
local.contributor.affiliationElphinstone, Kevin, University of New South Wales
local.contributor.affiliationHeiser, Gernot, University of New South Wales
local.contributor.affiliationCock, David, University of New South Wales
local.contributor.affiliationDerrin, Philip, University of New South Wales
local.contributor.affiliationElkaduwe, Dhammika, University of New South Wales
local.contributor.affiliationEngelhardt, Kai, University of New South Wales
local.contributor.affiliationKolanski, Rafal, University of New South Wales
local.contributor.affiliationNorrish, Michael, College of Engineering and Computer Science, ANU
local.contributor.affiliationSewell, Thomas, University of New South Wales
local.contributor.affiliationTuch, Harvey, National ICT Australia
local.contributor.affiliationWinwood, Simon, University of New South Wales
local.description.embargo2037-12-31
local.bibliographicCitation.issue6
local.bibliographicCitation.startpage107
local.bibliographicCitation.lastpage115
local.identifier.doi10.1145/1743546.1743574
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
dc.date.updated2016-02-24T08:26:30Z
local.identifier.scopusID2-s2.0-77953210383
local.identifier.thomsonID000278635800034
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Klein_SeL4:_Formal_verification_of_2010.pdf420.52 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator