seL4: formal verification of an operating-system kernel

Commun. ACM, pp. 107-115, 2010.

Cited by: 1526|Views112
EI

Abstract:

We report on the formal, machine-checked verication of the seL4 microkernel from an abstract specication 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 8,700 lines of C and 600 lines of assembler. Its performance i...More

Code:

Data:

Your rating :
0

 

Tags
Comments