Paper Info
Title
From a verified kernel towards verified systems
Abstract
The L4.verified project has produced a formal, machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper briefly summarises the proof, its main implications and assumptions, reports on the experience in conducting such a large-scale verification, and finally lays out a vision how this formally verified kernel may be used for gaining formal, code-level assurance about safety and security properties of systems on the order of a million lines of code.
Year
DOI
Venue
2010
10.1007/978-3-642-17164-2_3
APLAS
Keywords
Field
DocType
hol proof,machine-checked isabelle,paper briefly,code-level assurance,sel4 os microkernel,million line,abstract implementation,main implication,large-scale verification,c code,lines of code
HOL,Kernel (linear algebra),Programming language,Computer science,Microkernel,Theoretical computer science,Security analysis,Security properties,Source lines of code
Conference
Volume
ISSN
ISBN
6461
0302-9743
3-642-17163-X
Citations 
PageRank 
References 
7
0.49
16
Authors
1
Name
Order
Citations
PageRank
Gerwin Klein1145087.47