Paper Info
Title
The L4.verified project: next steps
Abstract
Last year, the NICTA L4.verified project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper gives a brief overview of the proof together with its main implications and assumptions, and paints a vision on how this verified kernel can be used for gaining assurance of overall system security on the code level for systems of a million lines of code or more.
Year
DOI
Venue
2010
10.1007/978-3-642-15057-9_6
VSTTE
Keywords
Field
DocType
last year,nicta l4,hol proof,brief overview,million line,abstract implementation,main implication,c code,next step,formal machine-checked isabelle,code level,system security,lines of code
HOL,Kernel (linear algebra),Programming language,Computer science,Microkernel,Security analysis,Project NExT,Operating system kernel,Network interface controller,Source lines of code
Conference
Volume
ISSN
ISBN
6217
0302-9743
3-642-15056-X
Citations 
PageRank 
References 
0
0.34
9
Authors
1
Name
Order
Citations
PageRank
Gerwin Klein1145087.47