seL4 is the world’s first microkernel that brings with it a formal proof of correctness. The kernel was designed against a specification and the translation of the source code to binary representation hold correctness proofs with them as well.

• In the L4 Family of Microkernels
  • Stems from Jochen Liedtke 1993 i386 assembly version
  • Has been generalized because the different L4’s don’t necessarily use the original ABI
  • L4 Kernels have a branching history of implementations
    • The UNSW (Univ New South Wales) group at NICTA’s L4-embedded version was the first to focus on embedded systems favoring
      • smaller memory footprints
      • lower complexity
    • OKLabs spun out from UNSW/NICTA with a commercial offering of L4, OKL4 (2006-2008)
      • This had capability based security
  • Share basic mechanism concepts
    • Address Spaces
    • Threads
    • Scheduling
    • Thin IPC implementation between isolated servers
• seL4 was originally created at OKLabs from scratch and implemented in a Haskell specification
  • Resource access is determined by a capability model which enables formal reasoning about an object’s permissions
  • Formal proof of functional correctness was completed in 2009
    • Proves implementation is correct against the Haskell specification
    • Proves the kernel is free of deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialized variables
  • Formal proof of C to binary translation

• Have been around since the early 70’s
  • Being formally recognized/coined in 1981 (Accent from Carnegie-Mellon)
• Near minimum amount of software that can provide mechanisms needed for an operating system
• Some mechanisms (Bare-minimum)
  • Low level address space management
  • Thread Management
  • Inter Process Communication
  • Interrupt management/routing
• Generally the kernel is the most privileged, everything else contained in user space

• Performance
  • More context switches
  • Because of crossing from User space to kernel space
    • A user space driver now communicates via IPC messages to another user space process
  • In a monolithic kernel a driver would be in kernel space and already be at a high privilege
• Complex process management
• Generally not as many applications/services for developers to build on
  • Usually need to implement your own key components

• Modularity
  • Servers can be plugged, swapped, and restarted easily
• Security
  • Separation of address spaces managed by the kernel
• Robustness
  • The limited requirements of a microkernel generally lead to a simpler code base
  • This is easier to test/peer review
  • Driver cannot directly crash the kernel
  • A system can be resurrected by monitor servers

• User space drivers and applications
• IPC communication
• Small kernel because of small set of responsibilities

• L4 Family (seL4, OKL4, Fiasco.OC)
• GNU Hurd (GNU’s perpetually unfinished microkernel based OS)
• MINIX (Andrew Tanenbaum’s academic microkernel)
• Magenta (Google’s microkernel for Fuchsia OS)
• Redox (A Rust microkernel)
• QNX (Blackberry’s microkernel)

This wiki serves as a companion to the tutorials provided by Data61, the tutorials provided by DornerWorks, and the wiki provided by Data61. This wiki consists of several main sections:

• Kernel Overview
• Deep Dive into the Initial seL4 User Space
• CAmkES Overview
• Development Environment

• Official Tutorials
  • Tutorials From Data61 Wiki
  • Tutorial Applicatons
  • Tutorial Manifest

• Latest seL4 Manual
• Latest CAmkES Manual
• Data61 seL4 Page
• Official seL4 Site
• CapDL: A Language for Describing Capability Based Systems
• Periodic Tasks With seL4/CAmkES
• BeagleBoneBlack UART with seL4/CAmkES
• Genode on seL4
• seL4: Formal Verification of an OS Kernel
  • This is from 2009 and may be outdated as far as API goes but the concepts are worth looking at
• seL4 Abstract Formal Specification
• FOSDEM 2015 seL4 Status
• DornerWorks seL4 Page