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 41 articles )
Showing results 1 to 20 of 41.
Sorted by year (- 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)
- Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
- Miller, Dale: Proof checking and logic programming (2017)
- Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
- Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
- Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Foster, Simon; Zeyda, Frank; Woodcock, Jim: Unifying heterogeneous state-spaces with lenses (2016)
- Mahboubi, Assia: Machine-checked mathematics (2016)
- Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
- Ma, Sha; Shi, Zhiping; Shao, Zhenzhou; Guan, Yong; Li, Liming; Li, Yongdong: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm (2016)
- Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
- Rabe, Florian: The future of logic: foundation-independence (2016)
- Rizkallah, Christine; Lim, Japheth; Nagashima, Yutaka; Sewell, Thomas; Chen, Zilin; O’Connor, Liam; Murray, Toby; Keller, Gabriele; Klein, Gerwin: A framework for the automatic formal verification of refinement from cogent to C (2016)
- Schubert, Aleksy; Urzyczyn, Paweł; Walukiewicz-Chrząszcz, Daria: How hard is positive quantification? (2016)
- Tan, Jiaqi; Tay, Hui Jun; Gandhi, Rajeev; Narasimhan, Priya: AUSPICE-R: automatic safety-property proofs for realistic features in machine code (2016)
- Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
- Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
- Klimiankou, Y.: A method for supporting runtime environments simultaneously served by multiple memory managers for operating systems based on second-generation microkernel (2015) ioport