Open Research will be unavailable from 10.15am - 11am on Saturday 14th March 2026 AEDT due to scheduled maintenance.
 

SeL4: Formal verification of an operating-system kernel

Simple item page
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.date.issued2010
dc.date.updated2016-02-24T08:26:30Z
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.identifier.issn0001-0782
dc.identifier.urihttp://hdl.handle.net/1885/52945
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.bibliographicCitation.issue6
local.bibliographicCitation.lastpage115
local.bibliographicCitation.startpage107
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.contributor.authoruidNorrish, Michael, u4087502
local.description.embargo2037-12-31
local.description.notesImported from ARIES
local.identifier.absfor080199 - Artificial Intelligence and Image Processing not elsewhere classified
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
local.identifier.ariespublicationf2965xPUB260
local.identifier.citationvolume53
local.identifier.doi10.1145/1743546.1743574
local.identifier.scopusID2-s2.0-77953210383
local.identifier.thomsonID000278635800034
local.type.statusPublished Version

Downloads

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
01_Klein_SeL4:_Formal_verification_of_2010.pdf
Size:
420.52 KB
Format:
Adobe Portable Document Format
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS