User Tools

Site Tools


start

The Secure Embedded L4 Microkernel (seL4)

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.

Background

  • 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

Microkernels

  • 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

Disadvantages

  • 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

Advantages

  • 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

Common Characteristics

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

Other Microkernels

  • 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:

More Resources

Tutorials

Data 61 Material

start.txt · Last modified: 2018/05/08 19:30 (external edit)