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.

References in zbMATH (referenced in 21 articles )

Showing results 1 to 20 of 21.
Sorted by year (citations)

1 2 next

  1. Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
  2. Rabe, Florian: The future of logic: foundation-independence (2016)
  3. Cheng, Shu; Woodcock, Jim; D’Souza, Deepak: Using formal reasoning on a model of tasks for FreeRTOS (2015)
  4. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  5. Klimiankou, Y.: A method for supporting runtime environments simultaneously served by multiple memory managers for operating systems based on second-generation microkernel (2015)
  6. Théry, Laurent (ed.); Wiedijk, Freek (ed.): Foreword to the special focus on formal proofs for mathematics and computer science (2015)
  7. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  8. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  9. Daum, Matthias; Billing, Nelson; Klein, Gerwin: Concerned with the unprivileged: user programs in kernel refinement (2014)
  10. Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
  11. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014)
  12. Lopriore, Lanfranco: Object protection in distributed systems (2013)
  13. Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare: SMT proof checking using a logical framework (2013)
  14. Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff: ATP and presentation service for Mizar formalizations (2013)
  15. Wiedijk, Freek: A synthesis of the procedural and declarative styles of interactive theorem proving (2012)
  16. Wiedijk, Freek: Pollack-inconsistency (2012)
  17. Malecha, Gregory; Morrisett, Greg; Wisnesky, Ryan: Trace-based verification of imperative programs with I/O (2011)
  18. Marić, Filip; Janičić, Predrag: Formalization of abstract state transition systems for SAT (2011)
  19. Sewell, Thomas; Winwood, Simon; Gammie, Peter; Murray, Toby; Andronick, June; Klein, Gerwin: seL4 enforces integrity (2011)
  20. Ahrendt, Wolfgang; Beckert, Bernhard; Giese, Martin; Rümmer, Philipp: Practical aspects of automated deduction for program verification (2010)

1 2 next