seL4
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.
Keywords for this software
References in zbMATH (referenced in 78 articles , 1 standard article )
Showing results 1 to 20 of 78.
Sorted by year (- Zhang, Xingyuan; Urban, Christian; Wu, Chunhan: Priority inheritance protocol proved correct (2020)
- Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos: System-level non-interference of constant-time cryptography. I: Model (2019)
- Miller, Dale: Mechanized metatheory Revisited (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L.: Bar induction is compatible with constructive type theory (2019)
- Straßburger, Lutz: The problem of proof identity, and why computer scientists should care about Hilbert’s 24th problem (2019)
- Achermann, Reto; Humbel, Lukas; Cock, David; Roscoe, Timothy: Physical addressing on real hardware in Isabelle/HOL (2018)
- Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
- Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
- Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol: The role of the Mizar mathematical library for interactive proof development in Mizar (2018)
- Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
- Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
- Müller, Peter (ed.); Schaefer, Ina (ed.): Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018 (2018)
- Nemati, Hamed; Baumann, Christoph; Guanciale, Roberto; Dam, Mads: Formal verification of integrity-preserving countermeasures against cache storage side-channels (2018)
- Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
- Syeda, Hira Taqdees; Klein, Gerwin: Program verification in the presence of cached address translation (2018)
- Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
- Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael: Verified characteristic formulae for CakeML (2017)
- Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland: A formal proof of the Kepler conjecture (2017)
- Hóu, Zhé; Sanán, David; Tiu, Alwen; Liu, Yang: Proof tactics for assertions in separation logic (2017)