swMATH ID: 15222
Software Authors: Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.
Description: seL4: formal verification of an OS kernel. Complete formal verification is the only known way to guarantee that a system is free of programming errors. We present our experience in performing 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, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. To our knowledge, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation. seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.
Homepage: http://dl.acm.org/citation.cfm?id=1629596
Related Software: Isabelle/HOL; Coq; Isabelle; HOL; HOL Light; kepler98; Mizar; Sledgehammer; Archive Formal Proofs; z3; CakeML; Flyspeck; ML; PVS; ACL2; Agda; VCC; CertiKOS; Haskell; LCF
Referenced in: 84 Publications
all top 5

Referenced by 212 Authors

12 Klein, Gerwin
5 Murray, Toby
5 Popescu, Andrei
3 Blanchette, Jasmin Christian
3 Dam, Mads
3 Kaliszyk, Cezary
3 Nipkow, Tobias
3 Paulson, Lawrence Charles
3 Rabe, Florian
3 Rizkallah, Christine
3 Sewell, Thomas D.
3 Urban, Josef
3 Wiedijk, Freek
2 Adams, Mark
2 Andronick, June
2 Aransay, Jesús
2 Barthe, Gilles
2 Bauereiß, Thomas
2 Chen, Zilin
2 Cristiá, Maximiliano
2 Daum, Matthias
2 Divasón, Jose
2 Dreyer, Derek R.
2 Filliâtre, Jean-Christophe
2 Foster, Simon
2 Gammie, Peter
2 Guanciale, Roberto
2 Hou, Zhe
2 Kohlhase, Michael
2 Kolanski, Rafal
2 Lim, Japheth
2 Liu, Yang
2 Malecha, Gregory
2 Matichuk, Daniel
2 Nagashima, Yutaka
2 Nanevski, Aleksandar
2 O’Connor, Liam
2 Oe, Duckki
2 Pesenti Gritti, Armando
2 Raimondi, Franco
2 Rossi, Gianfranco
2 Sanán, David
2 Stump, Aaron
2 Sutcliffe, Geoff
2 Syeda, Hira Taqdees
2 Tiu, Alwen Fernanto
2 Wenzel, Makarius
2 Woodcock, James C. P.
2 Ziliani, Beta
1 Achermann, Reto
1 Alkassar, Eyad
1 Amani, Sidney
1 Aoki, Toshiaki
1 Aspinall, David
1 Avigad, Jeremy
1 Bancerek, Grzegorz
1 Bauer, Gertrud
1 Baumann, Christoph
1 Bengtson, Jesper
1 Betarte, Gustavo
1 Bickford, Mark
1 Billing, Nelson
1 Böhme, Sascha
1 Boldo, Sylvie
1 Bourke, Timothy
1 Boyton, Andrew
1 Brassil, Matthew
1 Byliński, Czesław
1 Campo, Juan Diego
1 Cheng, Shu
1 Chiba, Yuki
1 Chlipala, Adam J.
1 Clancy, Kevin
1 Clément, François
1 Cock, David
1 Cohen, Liron
1 Constable, Robert Lee
1 Cook, Byron
1 Dang, Tat Dat
1 Demange, Vincent
1 Derrin, Philip
1 Dixon, Lucas
1 D’Souza, Deepak
1 Dubut, Jérémy
1 Elphinstone, Kevin
1 Gandhi, Rajeev
1 Gleirscher, Mario
1 Gonthier, Georges
1 Goodloe, Alwyn E.
1 Grabowski, Adam
1 Greenaway, David
1 Grégoire, Benjamin
1 Groce, Alex
1 Grov, Gudmund
1 Gu, Ronghui
1 Guan, Yong
1 Guéneau, Armaël
1 Hadarean, Liana
1 Hales, Thomas Callister
1 Haslbeck, Maximilian P. L.
...and 112 more Authors

Referencing Publications by Year