Paper Info
Title
seL4 in Australia: from research to real-world trustworthy systems
Abstract
TEN YEARS AGO, the functional correctness proof of the seL4 microkernel marked the first a completed operating system (OS) kernel had been verified to the source-code level.(4) This means there was a machine-checked proof that the implementation in the C language satisfied the kernel's specification, expressed in mathematical logic.Much has happened since then: We have extended the verification to show the kernel enforces desired security and safety properties, we have removed the need to trust the compiler, and we verified implementations for processor architectures other than the original Arm v6. We used experience from deploying seL4 in a number of real-world systems to evolve the kernel and its proofs to support a broader class of use cases, and we have made significant progress toward extending the assurance to systemwide properties. We will provide a brief overview of these developments, as well as ongoing research.
Year
DOI
Venue
2020
10.1145/3378426
Communications of the ACM
DocType
Volume
Issue
Journal
63
4
ISSN
Citations 
PageRank 
0001-0782
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Gernot Heiser12525137.42
Gerwin Klein2145087.47
June Andronick390342.66