User Tools

Site Tools


start

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

start [2018/05/08 19:30] (current)
Line 1: Line 1:
 +====== 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:
 +
 +  * [[wiki:​kerneloverview|Kernel Overview]]
 +  * [[wiki:​initialuserspace|Deep Dive into the Initial seL4 User Space]]
 +  * [[wiki:​camkesoverview|CAmkES Overview]]
 +  * [[wiki:​developmentenvironment|Development Environment]]
 +
 +====== More Resources ======
 +
 +===== Tutorials =====
 +
 +==== Data 61 Material ====
 +
 +  * Official Tutorials
 +    * [[https://​wiki.sel4.systems/​Tutorials|Tutorials From Data61 Wiki]]
 +    * [[https://​github.com/​SEL4PROJ/​sel4-tutorials|Tutorial Applicatons]]
 +    * [[https://​github.com/​SEL4PROJ/​sel4-tutorials-manifest/​|Tutorial Manifest]]
 +
 +===== Other Documents and Links =====
 +
 +  * [[https://​sel4.systems/​Info/​Docs/​seL4-manual-latest.pdf|Latest seL4 Manual]]
 +  * [[https://​github.com/​seL4/​camkes-tool/​blob/​master/​docs/​index.md|Latest CAmkES Manual]]
 +  * [[http://​ts.data61.csiro.au/​projects/​seL4/​|Data61 seL4 Page]]
 +  * [[https://​seL4.systems|Official seL4 Site]]
 +  * [[https://​www.cse.unsw.edu.au/​~kleing/​papers/​Kuz_KLW_10.pdf|CapDL:​ A Language for Describing Capability Based Systems]]
 +  * [[http://​julien.gunnm.org/​geek/​sel4/​2016/​04/​18/​periodic-tasks-with-sel4/​|Periodic Tasks With seL4/​CAmkES]]
 +  * [[http://​julien.gunnm.org/​geek/​sel4/​2016/​04/​18/​periodic-tasks-with-sel4/​|BeagleBoneBlack UART with seL4/​CAmkES]]
 +  * [[http://​genode.org/​documentation/​articles/​sel4_part_1|Genode on seL4]]
 +  * [[https://​www.sigops.org/​sosp/​sosp09/​papers/​klein-sosp09.pdf|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
 +  * [[http://​sel4.org/​Info/​Docs/​seL4-spec.pdf|seL4 Abstract Formal Specification]]
 +  * [[https://​archive.fosdem.org/​2015/​schedule/​event/​sel4/​attachments/​slides/​790/​export/​events/​attachments/​sel4/​slides/​790/​1502_fosdem.pdf|FOSDEM 2015 seL4 Status]]
 +  * [[https://​dornerworks.com/​sel4-microkernel|DornerWorks seL4 Page]]
 +
  
start.txt · Last modified: 2018/05/08 19:30 (external edit)