View source for L4 microkernel family

{{Short description|Family of second-generation microkernels}}
{{Use dmy dates|date=June 2021}}
{{Infobox OS
| name = L4 microkernel family
| logo = <!-- Filename only: no wikilink, Image: or File: -->
| logo caption = 
| logo alt = 
| screenshot = <!-- Filename only: no wikilink, Image: or File: -->
| caption = 
| screenshot alt = 
| developer = [[Jochen Liedtke]]
| family = L4
| working state = Current
| source model = [[Open-source software|Open source]], [[closed source]]
| released = {{Start date and age|1993}}<!-- If known, add |mm|dd|df=yes -->
| latest release version = 
| latest release date = {{Start date and age|2020}}<!-- If known, add |mm|dd|df=yes -->
| repo = <!-- {{URL|https://example.com}} -->
| marketing target = Reliable computing
| programmed in = [[Assembly language]], then [[C (programming language)|C]], [[C++]]
| language = English, German
| language count = 
| update model = <!-- APT, Windows Update, etc. -->
| package manager = <!-- dpkg, rpm, Windows installer, etc. -->
| supported platforms = Intel [[i386]], [[x86]], [[x86-64]], [[ARM architecture|ARM]], [[MIPS architecture|MIPS]], [[SPARC]], [[Itanium]], [[RISC-V]]
| kernel type = [[Microkernel]]
| userland = 
| ui = 
| license = [[Source code]], [[Formal proof|proofs]]: [[GNU General Public License#Version 2|GPLv2]]<br/>[[Library (computing)|Libraries]], [[Programming tool|tools]]: [[BSD licenses#2-clause|BSD 2-clause]]
| preceded by = [[Eumel]]
| succeeded by = 
| website = {{URL|os.inf.tu-dresden.de/L4}}
| other articles = 
}}
'''L4''' is a family of second-generation [[microkernel]]s, used to implement a variety of types of [[operating system]]s (OS), though mostly for [[Unix-like]], ''Portable Operating System Interface'' ([[POSIX]]) compliant types.

L4, like its predecessor microkernel [[#L3|L3]], was created by [[Germany|German]] [[computer scientist]] [[Jochen Liedtke]] as a response to the poor performance of earlier microkernel-based OSes. Liedtke felt that a system designed from the start for high performance, rather than other goals, could produce a microkernel of practical use. His original implementation in hand-coded Intel [[i386]]-specific [[assembly language]] code in 1993 created attention by being 20 times faster than [[Mach (kernel)|Mach]].<ref name="Liedtke_93">{{cite conference
 |last=Liedtke |first=Jochen |author-link=Jochen Liedtke
 |title = Improving IPC by kernel design
 |book-title = 14th ACM Symposium on Operating System Principles
 |pages = 175–188
 |date=December 1993
 |location = Asheville, NC, USA
 |url = http://portal.acm.org/citation.cfm?id=168619.168633
}}</ref>
The follow-up publication two years later<ref name=Lie95>{{cite conference
 |last=Liedtke |first=Jochen |author-link=Jochen Liedtke
 |title = On μ-Kernel Construction
 |book-title = Proceedings 15th ACM Symposium on Operating Systems Principles (SOSP)
 |pages = 237–250
 |date = December 1995
 |url = http://os.itec.kit.edu/65_1029.php
 |archive-url = https://web.archive.org/web/20151025154932/http://os.itec.kit.edu/65_1029.php
 |archive-date = 25 October 2015
 |url-status = live}}</ref> was considered so influential that it won the 2015 [[ACM SIGOPS]] Hall of Fame Award.
Since its introduction, L4 has been developed to be [[Cross-platform software|cross-platform]] and to improve [[Computer security|security]], isolation, and [[Robustness (computer science)|robustness]].

There have been various re-implementations of the original L4 [[Kernel (operating system)|kernel]] [[application binary interface]] (ABI) and its successors, including ''L4Ka::Pistachio'' (implemented by Liedtke and his students at [[Karlsruhe Institute of Technology]]), ''L4/MIPS'' ([[University of New South Wales]] (UNSW)), ''Fiasco'' ([[Dresden University of Technology]] (TU Dresden)). For this reason, the name ''L4'' has been generalized and no longer refers to only Liedtke's original implementation. It now applies to the whole [[microkernel]] family including the L4 kernel [[Interface (computing)|interface]] and its different versions.

L4 is widely deployed. One variant, OKL4 from [[Open Kernel Labs]], shipped in billions of mobile devices.<ref name="OKL4 Microvisor">{{cite web |url=https://gdmissionsystems.com/cyber/products/trusted-computing-cross-domain/microvisor-products/ |title=Hypervisor Products: General Dynamics Mission Systems |website=General Dynamics Mission Systems |access-date=26 April 2018 |url-status=live |archive-url=https://web.archive.org/web/20171115152446/https://gdmissionsystems.com/cyber/products/trusted-computing-cross-domain/microvisor-products/ |archive-date=15 November 2017}}</ref><ref name=OKL_PR>
{{cite press release
 |title=Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments
 |url=http://www.ok-labs.com/releases/release/ok-labs-software-surpasses-milestone-of-1.5-billion-mobile-device-shipments
 |archive-url=https://web.archive.org/web/20120211210405/http://www.ok-labs.com/releases/release/ok-labs-software-surpasses-milestone-of-1.5-billion-mobile-device-shipments
 |archive-date=11 February 2012
 |url-status=dead
 |date=19 January 2012 |publisher=[[Open Kernel Labs]]
}}</ref>

== Design paradigm ==
Specifying the general idea of a [[microkernel]], [[Jochen Liedtke|Liedtke]] states:

<blockquote>A concept is tolerated inside the microkernel only if moving it outside the kernel, i.e., permitting competing implementations, would prevent the implementation of the system's required functionality.<ref name=Lie95 /></blockquote><!--http://portal.acm.org/citation.cfm?id=224075&coll=portal&dl=ACM&CFID=183836&CFTOKEN=65974839-->

In this spirit, the L4 microkernel provides few basic mechanisms: [[address space]]s (abstracting page tables and providing memory protection), [[Thread (computing)|threads]] and [[Scheduling (computing)|scheduling]] (abstracting execution and providing temporal protection), and [[inter-process communication]] (for controlled communication across isolation boundaries).

An operating system based on a microkernel like L4 provides services as servers in [[user space]] that [[monolithic kernel]]s like [[Linux]] or older generation microkernels include internally. For example, to implement a secure [[Unix-like]] system, servers must provide the rights management that [[Mach (kernel)|Mach]] included inside the kernel.

== History ==
The poor performance of first-generation microkernels, such as [[Mach (kernel)|Mach]], led a number of developers to re-examine the entire microkernel concept in the mid-1990s. The asynchronous in-kernel-buffering [[inter-process communication|process communication]] concept used in Mach turned out to be one of the main reasons for its poor performance. This induced developers of Mach-based operating systems to move some time-critical components, like file systems or drivers, back inside the kernel.{{Citation needed|date=August 2010}} While this somewhat ameliorated the performance issues, it plainly violates the minimality concept of a true microkernel (and squanders their major advantages).

Detailed analysis of the Mach bottleneck indicated that, among other things, its [[working set]] is too large: the IPC code expresses poor spatial locality; that is, it results in too many [[CPU cache|cache]] misses, of which most are in-kernel.<ref name=Lie95 /> This analysis gave rise to the principle that an efficient microkernel should be small enough that the majority of performance-critical code fits into the (first-level) cache (preferably a small fraction of said cache).

=== L3 ===
[[Jochen Liedtke]] set out to prove that a well-designed thinner [[inter-process communication]] (IPC) layer, with careful attention to performance and machine-specific (in contrast to [[cross-platform software]]) design could yield large real-world performance improvements. Instead of Mach's complex IPC system, his L3 microkernel simply passed the message with no added overhead. Defining and implementing the required security policies were considered to be duties of the [[user space]] servers. The role of the kernel was only to provide the needed mechanism to enable the user-level servers to enforce the policies. L3, developed in 1988, proved itself a safe and robust [[operating system]], used for many years for example by [[Technischer Überwachungsverein]] (Technical Inspection Association).{{Citation needed|date=September 2010}}

[[File:L4 family tree.svg|thumb|400px|L4 family tree (black arrows indicate code inheritance, green arrows ABI inheritance)]]

=== L4 ===
After some experience using L3, Liedtke came to the conclusion that several other Mach concepts were also misplaced. By simplifying the microkernel concepts even further he developed the first L4 kernel which was primarily designed for high performance. To maximise performance, the whole kernel was written in [[assembly language]], and its IPC was 20 times faster than Mach's.<ref name="Liedtke_93" /> Such dramatic performance increases are a rare event in operating systems, and Liedtke's work triggered new L4 implementations and work on L4-based systems at a number of universities and research institutes, including [[IBM]], where Liedtke started to work in 1996, TU Dresden and UNSW. At IBM's [[Thomas J. Watson Research Center]] Liedtke and his colleagues continued research on L4 and microkernel based systems in general, especially the Sawmill OS.<ref name="Gefflaut_JPLEUTDR_00">{{cite conference
 |last1=Gefflaut |first1=Alain
 |last2=Jaeger |first2=Trent
 |last3=Park |first3=Yoonho
 |last4=Liedtke |first4=Jochen |author4-link=Jochen Liedtke
 |last5=Elphinstone |first5=Kevin
 |last6=Uhlig |first6=Volkmar
 |last7=Tidswell |first7=Jonathon
 |last8=Deller |first8=Luke
 |last9=Reuther |first9=Lars
 |date = 2000
 |url=http://dl.acm.org/citation.cfm?id=566726.566751
 |title=The Sawmill multiserver approach
 |book-title=ACM SIGOPS European Workshop
 |pages=109–114
 |location=Kolding, Denmark
}}</ref>

=== L4Ka::Hazelnut ===
In 1999, Liedtke took over the Systems Architecture Group at the [[University of Karlsruhe]], where he continued the research into microkernel systems. As a proof of concept that a high performance microkernel could also be constructed in a higher level language, the group developed ''L4Ka::Hazelnut'', a [[C++]] version of the kernel that ran on [[IA-32]]- and [[ARM architecture|ARM]]-based machines. The effort was a success, performance was still acceptable, and with its release, the pure assembly language versions of the kernels were effectively discontinued.

=== L4/Fiasco ===
In parallel to the development of L4Ka::Hazelnut, in 1998 the Operating Systems Group TUD:OS of the TU Dresden started to develop their own C++ implementation of the L4 kernel interface, named L4/Fiasco. In contrast to L4Ka::Hazelnut, which allows no concurrency in the kernel, and its successor L4Ka::Pistachio, which allows interrupts in the kernel only at specific preemption points, ''L4/Fiasco'' was fully preemptible (with the exception of extremely short atomic operations) to achieve a low [[interrupt latency]]. This was considered necessary because L4/Fiasco is used as the basis of DROPS,<ref>{{cite web |url=http://os.inf.tu-dresden.de/drops/overview.html |title=DROPS – Overview |website=[[Dresden University of Technology]] |access-date=2011-08-10 |url-status=live |archive-url=https://web.archive.org/web/20110807170107/http://os.inf.tu-dresden.de/drops/overview.html |archive-date=2011-08-07}}</ref> a hard [[real-time computing]] capable operating system, also developed at the TU Dresden. However, the complexities of a fully preemptible design prompted later versions of Fiasco to return to the traditional L4 approach of running the kernel with interrupts disabled, except for a limited number of preemption points.

== Cross-platform ==

=== L4Ka::Pistachio ===
Up until the release of L4Ka::Pistachio and newer versions of Fiasco, all L4 microkernels had been inherently tied close to the underlying CPU architecture. The next big shift in L4 development was the development of a cross-platform (platform-independent) application programming interface ([[API]]) that still retained the high performance characteristics despite its higher level of portability. Although the underlying concepts of the kernel were the same, the new API provided many significant changes relative to prior L4 versions, including better support for multi-processor systems, looser ties between threads and address spaces, and the introduction of user-level thread control blocks (UTCBs) and virtual registers. After releasing the new L4 API (version X.2 a.k.a. version 4) in early 2001, the System Architecture Group at the University of Karlsruhe implemented a new kernel, ''L4Ka::Pistachio'', completely from scratch, now with focus on both high performance and portability. It was released under the [[BSD licenses#2-clause license ("Simplified BSD License" or "FreeBSD License")|two-clause BSD license]].<ref>[https://www.l4ka.org/65.php l4ka.org: L4Ka::Pistachio microkernel] Quote: "...The variety of supported architctures makes L4Ka::Pistachio an ideal research and development platform for a wide variety of systems..."</ref>

=== Newer Fiasco versions ===
The L4/Fiasco microkernel has also been extensively improved over the years. It now supports several hardware platforms ranging from x86 through AMD64 to several ARM platforms. Notably, a version of Fiasco (Fiasco-UX) can run as a user-level application on Linux.

L4/Fiasco implements several extensions to the L4v2 API. Exception IPC enables the kernel to send CPU exceptions to user-level handler applications. With the help of [[alien thread]]s, it is possible to perform fine-grained control over system calls. X.2-style UTCBs have been added. Also, Fiasco contains mechanisms for controlling communication rights and kernel-level resource use. On Fiasco, a collection of basic user level services are developed (named L4Env) that among others are used to para-virtualise the current Linux version (4.19 {{as of|2019|05|lc=y}}) (named [[L4Linux|L<sup>4</sup>Linux]]).

=== University of New South Wales and NICTA ===
Development also occurred at the [[University of New South Wales]] (UNSW), where developers implemented L4 on several 64-bit platforms. Their work resulted in ''L4/MIPS'' and ''L4/Alpha'', resulting in Liedtke's original version being retrospectively named ''L4/x86''. Like Liedtke's original kernels, the UNSW kernels (written in a mix of assembly and C) were unportable and each implemented from scratch. With the release of the highly portable L4Ka::Pistachio, the UNSW group abandoned their own kernels in favor of producing highly tuned ports of L4Ka::Pistachio, including the fastest-ever reported implementation of message passing (36 cycles on the [[Itanium]] architecture).<ref name=Gray_CCMH_05>{{cite conference |last1=Gray |first1=Charles |last2=Chapman |first2=Matthew |last3=Chubb |first3=Peter |last4=Mosberger-Tang |first4=David |last5=Heiser |first5=Gernot |author5-link=Gernot Heiser |title=Itanium: A system implementor's tale |book-title=USENIX Annual Technical Conference |pages=264–278 |date=April 2005 |location=Annaheim, CA, USA |url=http://www.usenix.org/publications/library/proceedings/usenix05/tech/general/gray.html |url-status=live |archive-url=https://web.archive.org/web/20070217224750/http://www.usenix.org/publications/library/proceedings/usenix05/tech/general/gray.html |archive-date=2007-02-17}}</ref> The group has also demonstrated that [[device driver]]s can perform equally well at user-level as in-kernel,<ref name=Leslie_CFGGMPSEH_05>{{cite journal |last1=Leslie |first1=Ben |last2=Chubb |first2=Peter |last3=FitzRoy-Dale |first3=Nicholas |last4=Götz |first4=Stefan |last5=Gray |first5=Charles |last6=Macpherson |first6=Luke |last7=Potts |first7=Daniel |last8=Shen |first8=Yueting |last9=Elphinstone |first9=Kevin |last10=Heiser |first10=Gernot |author10-link=Gernot Heiser |date=September 2005 |title=User-level device drivers: achieved performance |journal=Journal of Computer Science and Technology |volume=20 |issue=5 |pages=654–664 |doi=10.1007/s11390-005-0654-4 |citeseerx=10.1.1.59.6766 |s2cid=1121537}}</ref> and developed [[Wombat (operating system)|Wombat]], a highly portable version of [[Linux]] on L4 that runs on [[x86]], [[ARM architecture|ARM]], and [[MIPS architecture|MIPS]] processors. On [[XScale]] processors, Wombat context-switching costs are up to 50 times lower than in native Linux.<ref name=vanSchaik_Heiser_07>{{cite conference
 |last1=van Schaik |first1=Carl
 |last2=Heiser |first2=Gernot |author2-link=Gernot Heiser
 |date=January 2007
 |title = High-performance microkernels and virtualisation on ARM and segmented architectures
 |book-title = 1st International Workshop on Microkernels for Embedded Systems
 |pages = 11–21
 |publisher = [[NICTA]]
 |location = Sydney, Australia
 |url = http://ssrg.nicta.com.au/publications/papers/vanSchaik_Heiser_07.abstract.pml
 |access-date = 2015-10-25
 |archive-url = https://web.archive.org/web/20150301150250/http://ssrg.nicta.com.au/publications/papers/vanSchaik_Heiser_07.abstract
 |archive-date = 2015-03-01
 |url-status = live
}}</ref>

Later the UNSW group, now at [[NICTA]] (formerly ''National ICT Australia, Ltd''.), forked L4Ka::Pistachio into a new L4 version named ''NICTA::L4-embedded''. It was for use in commercial [[embedded system]]s, and consequently the implementation trade-offs favored small memory size and reduced complexity. The API was modified to keep almost all system calls short enough that they need no preemption points in order to ensure high real-time responsiveness.<ref name=Ruocco_08>{{cite journal
 |last=Ruocco |first=Sergio
 |date=October 2008
 |title = A Real-Time Programmer's Tour of General-Purpose L4 Microkernels
 |journal = EURASIP Journal on Embedded Systems
 |doi = 10.1155/2008/234710
 |volume = 2008
 |pages = 1–14
 |doi-broken-date=1 November 2024
 |s2cid = 7430332
 |doi-access=free
}}</ref>

== Commercial deployment ==
In November 2005, [[NICTA]] announced<ref>
{{cite press release
 | title = NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions
 | url = http://www.nicta.com.au/director/mediacentre/media_releases_2005.cfm?viewArticle=true&item_id=2563&startrow=1
 | url-status = dead
 | publisher = [[NICTA]]
 | date = 24 November 2005
 | archive-url = https://web.archive.org/web/20060825225104/http://www.nicta.com.au/director/mediacentre/media_releases_2005.cfm?viewArticle=true&item_id=2563&startrow=1
 | archive-date = 25 August 2006
}}</ref> that [[Qualcomm]] was deploying NICTA's L4 version on their ''[[Mobile Station Modem]]'' chipsets. This led to the use of L4 in [[mobile phone]] handsets on sale from late 2006. In August 2006, ERTOS leader and UNSW professor [[Gernot Heiser]] spun out a company named [[Open Kernel Labs]] (OK Labs) to support commercial L4 users and further develop L4 for commercial use under the brand name ''OKL4'', in close collaboration with NICTA. ''OKL4 μKernel'' Version 2.1, released in April 2008, was the first [[general availability|generally available]] version of L4 which featured [[capability-based security]]. OKL4 μKernel 3.0, released in October 2008, was the last open-source version of OKL4 μKernel. More recent versions are closed source and based on a rewrite to support a native hypervisor variant named the ''OKL4 Microvisor''. OK Labs also distributed a paravirtualized Linux named OK:Linux, a descendant of Wombat, and paravirtualized versions of [[SymbianOS]] and [[Android (operating system)|Android]]. OK Labs also acquired the rights to ''seL4'' from NICTA.

OKL4 shipments exceeded 1.5 billion in early 2012,<ref name=OKL_PR /> mostly on Qualcomm wireless modem chips. Other deployments include [[automotive infotainment]] systems.<ref name=OKL_PR_auto>
{{cite press release
 |title=Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems
 |url=http://www.ok-labs.com/releases/release/ok-labs-automotive-virtualization-selected-by-bosch-forinfotainment-systems
 |date=27 March 2012 
 |publisher=[[Open Kernel Labs]]
 |url-status=dead
 |archive-url=https://web.archive.org/web/20120702191648/http://www.ok-labs.com/releases/release/ok-labs-automotive-virtualization-selected-by-bosch-forinfotainment-systems
 |archive-date=2 July 2012
}}</ref>

[[Apple A series]] processors beginning with the [[Apple A7|A7]] contain a Secure Enclave [[coprocessor]] running an L4 operating system<ref>{{cite web|title=iOS Security, iOS 12.3|url=https://www.apple.com/tr/business/docs/site/iOS_Security_Guide.pdf |archive-url=https://web.archive.org/web/20200624043752/https://www.apple.com/tr/business/docs/site/iOS_Security_Guide.pdf |archive-date=2020-06-24 |url-status=live|publisher=Apple Inc.|date=May 2019}}</ref> called sepOS (Secure Enclave Processor OS)
based on the L4-embedded kernel developed at [[NICTA]] in 2006.<ref>
{{cite conference
 |last1=Mandt |first1=Tarjei
 |last2=Solnik |first2=Mathew
 |last3=Wang |first3=David
 |title = Demystifying the Secure Enclave Processor
 |url = https://www.blackhat.com/docs/us-16/materials/us-16-Mandt-Demystifying-The-Secure-Enclave-Processor.pdf
 |book-title = BlackHat USA
 |date = 31 July 2016
 |location = Las Vegas, Nevada, USA
 |url-status = live
 |archive-url = https://web.archive.org/web/20161021193045/https://www.blackhat.com/docs/us-16/materials/us-16-Mandt-Demystifying-The-Secure-Enclave-Processor.pdf
 |archive-date = 21 October 2016
}}</ref>
As a result, L4 ships on all modern Apple devices including Macs with [[Apple silicon]]. In 2015 alone, total shipments of iPhone was estimated at 310 million.<ref>
{{cite news
 |last=Elmer-DeWitt 
 |first=Philip 
 |date=28 October 2014 
 |title=Forecast: Apple will ship 310 million iOS devices in 2015 
 |url=http://fortune.com/2014/10/28/forecast-apple-will-ship-310-million-ios-devices-in-2015 
 |url-status=live
 |magazine=[[Fortune (magazine)|Fortune]] 
 |archive-url=https://web.archive.org/web/20150927083455/http://fortune.com/2014/10/28/forecast-apple-will-ship-310-million-ios-devices-in-2015/
 |archive-date=27 September 2015
 |access-date=25 October 2015 
}}</ref>

== High assurance: seL4 ==
In 2006, the [[NICTA]] group commenced a from-scratch design of a [[Microkernel#Third generation|third-generation microkernel]], named seL4, with the aim of providing a basis for highly secure and reliable systems, suitable for satisfying security requirements such as those of [[Common Criteria]] and beyond. From the beginning, development aimed for [[formal verification]] of the kernel. To ease meeting the sometimes conflicting requirements of performance and verification, the team used a [[middle-out]] software process starting from an executable [[specification]] written in the language [[Haskell]].<ref name=Derrin_EKCC_06>
{{cite conference
 |last1=Derrin |first1=Philip
 |last2=Elphinstone |first2=Kevin
 |last3=Klein |first3=Gerwin
 |last4=Cock |first4=David
 |last5=Chakravarty |first5=Manuel M. T.
 |date=September 2006
 |title = Running the manual: an approach to high-assurance microkernel development
 |book-title = ACM SIGPLAN Haskell Workshop
 |pages = 60–71
 |location = [[Portland, Oregon]]
 |url = http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956
}}</ref>
seL4 uses [[capability-based security]] access control to enable formal reasoning about object accessibility.

A [[formal proof]] of functional correctness was completed in 2009.<ref name="Klein_EHACDEEKNSTW_09">
{{cite conference
 |last1 = Klein |first1 = Gerwin
 |last2 = Elphinstone |first2 = Kevin
 |last3 = Heiser |first3 = Gernot |author3-link = Gernot Heiser
 |last4 = Andronick |first4 = June
 |last5 = Cock |first5 = David
 |last6 = Derrin |first6 = Philip
 |last7 = Elkaduwe |first7 = Dhammika
 |last8 = Engelhardt |first8 = Kai
 |last9 = Kolanski |first9 = Rafal
 |last10 = Norrish |first10 = Michael
 |last11 = Sewell |first11 = Thomas
 |last12 = Tuch |first12 = Harvey
 |last13 = Winwood |first13 = Simon
 |date = October 2009
 |title = seL4: Formal verification of an OS kernel
 |book-title = 22nd ACM Symposium on Operating System Principles
 |location = Big Sky, MT, USA
 |url = http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
 |url-status = live
 |archive-url = https://web.archive.org/web/20110728022610/http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
 |archive-date = 2011-07-28
}}</ref>
The proof provides a guarantee that the kernel's implementation is correct against its specification, and implies that it is free of implementation bugs such as [[deadlock (computer science)|deadlock]]s, [[livelock]]s, [[buffer overflow]]s, arithmetic exceptions or use of [[Uninitialized variable|uninitialised variables]]. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.<ref name="Klein_EHACDEEKNSTW_09" /> The work on seL4 won the 2019 [[ACM SIGOPS]] Hall of Fame Award.

seL4 takes a novel approach to kernel resource management,<ref name="Elkaduwe_DE_08">
{{cite conference
 |last1 = Elkaduwe |first1 = Dhammika
 |last2 = Derrin |first2 = Philip
 |last3 = Elphinstone |first3 = Kevin
 |date = April 2008
 |title = Kernel design for isolation and assurance of physical memory
 |location = Glasgow, UK
 |doi = 10.1145/1435458
 |url = https://ts.data61.csiro.au/publications/nictaabstracts/Elkaduwe_DE_08.abstract.pml
 |conference = 1st Workshop on Isolation and Integration in Embedded Systems
 |access-date = 2020-02-22
 |archive-date = 22 February 2020
 |archive-url = https://web.archive.org/web/20200222061257/https://ts.data61.csiro.au/publications/nictaabstracts/Elkaduwe_DE_08.abstract.pml
 |url-status = dead
|url-access = subscription
 }}</ref> exporting the management of kernel resources to user level and subjects them to the same [[capability-based security|capability-based]] access control as user resources. This model, which was also adopted by [[Barrelfish (operating system)|Barrelfish]], simplifies reasoning about isolation properties, and was an enabler for later proofs that seL4 enforces the core security properties of integrity and confidentiality.<ref name="Klein_AEMSKH_14">
{{cite journal
 |last1 = Klein |first1 = Gerwin
 |last2 = Andronick |first2 = June
 |last3 = Elphinstone |first3 = Kevin
 |last4 = Murray |first4 = Toby
 |last5 = Sewell |first5 = Thomas
 |last6 = Kolanski |first6 = Rafal
 |last7 = Heiser |first7 = Gernot |author7-link=Gernot Heiser
 |date = February 2014
 |title = Comprehensive Formal Verification of an OS Microkernel
 |journal = ACM Transactions on Computer Systems
 |volume = 32
 |issue = 1
 |pages = 2:1–2:70
 |doi = 10.1145/2560537
 |citeseerx = 10.1.1.431.9140
 |s2cid = 4474342
}}</ref> The NICTA team also proved correctness of the translation from the programming language [[C (programming language)|C]] to executable [[machine code]], taking the [[compiler]] out of the [[trusted computing base]] of seL4.<ref name="Sewell_MK_13">{{cite conference
 |last1 = Sewell |first1 = Thomas
 |last2 = Myreen |first2 = Magnus
 |last3 = Klein |first3 = Gerwin
 |date = June 2013
 |title = Translation Validation for a Verified OS Kernel
 |book-title = ACM SIGPLAN Conference on Programming Language Design and Implementation
 |location = Seattle, WA, USA
 |doi = 10.1145/2491956.2462183
 |url = https://dl.acm.org/doi/pdf/10.1145/2491956.2462183
|url-access = subscription
 }}</ref>
This implies that the high-level security proofs hold for the kernel executable. seL4 is also the first published protected-mode OS kernel with a complete and sound [[worst-case execution time]] (WCET) analysis, a prerequisite for its use in hard [[real-time computing]].<ref name="Klein_AEMSKH_14"/>

On 29 July 2014, [[NICTA]] and [[General Dynamics C4 Systems]] announced that seL4, with end to end proofs, was now released under [[open-source license]]s.<ref name=seL4_OSS>
{{cite press release
 |title = Secure operating system developed by NICTA goes open source
 |url = https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/
 |date = 29 July 2014
 |publisher = [[NICTA]]
 |url-status = live
 |archive-url = https://web.archive.org/web/20160315212902/https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/
 |archive-date = 15 March 2016
}}</ref>
The kernel [[source code]] and proofs are [[Software license|licensed]] under [[GNU General Public License#Version 2|GNU General Public License version 2]] (GPLv2), and most [[Library (computing)|libraries]] and [[Programming tool|tools]] are under the [[BSD licenses#2-clause|BSD 2-clause]]. In April 2020, it was announced that the seL4 Foundation was created under the umbrella of the [[Linux Foundation]] to accelerate development and deployment of seL4.<ref name=seL4_Foundation>
{{cite press release
 |title = Security Gets Support of Linux Foundation
 |url = https://www.linuxfoundation.org/press/press-release/sel4-microkernel-optimized-for-security-gets-support-of-linux-foundation/
 |date = 7 April 2020
 |publisher = [[Linux Foundation]]
 |url-status = live
 |archive-url = https://web.archive.org/web/20160315212902/https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/
 |archive-date = 15 March 2016
}}</ref>

The researchers state that the cost of formal software verification is lower than the cost of engineering traditional "high-assurance" software despite providing much more reliable results.<ref>{{cite journal |last1=Klein |first1=Gerwin |last2=Andronick |first2=June |last3=Elphinstone |first3=Kevin |last4=Murray |first4=Toby |last5=Sewell |first5=Thomas |last6=Kolanski |first6=Rafal |last7=Heiser |first7=Gernot |author7-link=Gernot Heiser |year=2014 |title=Comprehensive formal verification of an OS microkernel |url=http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf |journal=ACM Transactions on Computer Systems |volume=32 |page=64 |doi=10.1145/2560537 |url-status=live |archive-url=https://web.archive.org/web/20140803122308/http://www.nicta.com.au/pub?doc=7371&filename=Klein_AEMSKH_14.pdf |archive-date=2014-08-03 |citeseerx=10.1.1.431.9140 |s2cid=4474342}}</ref> Specifically, the cost of one [[source lines of code|line of code]] during the development of seL4 was estimated at around {{US$|400}}, compared to {{US$|1000}} for traditional high-assurance systems.<ref>{{Cite AV media |last=Heiser |first=Gernot |author-link=Gernot Heiser |date=16 January 2015 |url=https://www.youtube.com/watch?v=lRndE7rSXiI |title=seL4 Is Free: What Does This Mean for You? |publisher=Linux.conf.au |place=Auckland, New Zealand}}</ref>

Under the Defense Advanced Research Projects Agency ([[DARPA]]) High-Assurance Cyber Military Systems (HACMS) program, NICTA together with project partners [[Rockwell Collins]], Galois Inc, the [[University of Minnesota]] and [[Boeing]] developed a high-assurance drone using seL4, along with other assurance tools and software, with planned technology transfer onto the optionally piloted autonomous [[Boeing AH-6]] Unmanned Little Bird helicopter being developed by Boeing. Final demonstration of the HACMS technology took place in Sterling, VA in April 2017.<ref name=hacms_demo>
{{cite press release
 |title = DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms
 |url = https://www.rockwellcollins.com/Data/News/2017-Cal-Yr/GS/FY17GSNR38-HACMS.aspx
 |date = 24 April 2017
 |publisher = [[Rockwell Collins]]
 |url-status = live
 |archive-url = https://web.archive.org/web/20170511155335/http://rockwellcollins.com/Data/News/2017-Cal-Yr/GS/FY17GSNR38-HACMS.aspx
 |archive-date = 11 May 2017
}}</ref> DARPA also funded several [[Small Business Innovative Research]] (SBIR) contracts related to seL4 under a program started by [[John Launchbury]]. Small businesses receiving an seL4-related SBIR included: DornerWorks, Techshot, Wearable Inc, Real Time Innovations, and Critical Technologies.<ref name=sbir_sel4>
{{cite web
 |url = https://sbirsource.com/sbir/people/81829-dr-john-launchbury
 |title = DARPA Agency Sponsor Dr. John Launchbury
 |author = <!-- Unstated -->
 |date = 2017
 |website = SBIRSource
 |access-date = 16 May 2017
 |url-status = live
 |archive-url = https://web.archive.org/web/20170929000603/https://sbirsource.com/sbir/people/81829-dr-john-launchbury
 |archive-date = 29 September 2017
}}</ref>

In October 2023, [[Nio Inc.]] announced that their seL4-based SkyOS operating systems will be in mass-produced electric cars from 2024.<ref>{{Cite web |title=News about seL4 and the seL4 Foundation |url=https://sel4.systems/news/2023#nio-skyos |access-date=2024-09-20 |website=sel4.systems}}</ref>

In 2023, seL4 won the [[ACM Software System Award]].

== Other research and development ==
Osker, an OS written in [[Haskell]], targeted the L4 specification; although this project focused mainly on the use of a [[functional programming]] language for OS development, not on microkernel research.<ref>
{{cite journal
 |last1 = Hallgren |first1 = T.
 |last2 = Jones |first2 = M.P.
 |last3 = Leslie |first3 = R.
 |last4 = Tolmach |first4 = A.
 |journal = ACM SIGPLAN Notices
 |year = 2005
 |title = A principled approach to operating system construction in Haskell
 |url = http://web.cecs.pdx.edu/~apt/icfp05.pdf
 |volume = 40
 |issue = 9
 |pages = 116–128
 |issn = 0362-1340
 |doi = 10.1145/1090189.1086380
 |access-date = 2010-06-24
 |url-status = live
 |archive-url = https://web.archive.org/web/20100615164444/http://web.cecs.pdx.edu/~apt/icfp05.pdf
 |archive-date = 2010-06-15
}}</ref>

RedoxOS<ref>{{cite web |url=https://www.redox-os.org/ |title=RedoxOS |website=[[RedoxOS]]}}</ref> is a Rust based operating system, that is also inspired by seL4, and uses a micro kernel design.

CodeZero<ref>{{cite web |url=https://os.inf.tu-dresden.de/pipermail/l4-hackers/2009/004166.html |title=Announce: Introducing Codezero |website=[[Dresden University of Technology]]}}</ref> is an L4 microkernel for embedded systems with a focus on virtualization and implementation of native OS services. There is a [[GPL 3|GPL]]-licensed version,<ref>{{cite web |url=https://github.com/jserv/codezero |title=jserv/codezero: Codezero Microkernel |website=[[GitHub]] |access-date=2020-10-20 |url-status=live |archive-url=https://web.archive.org/web/20150815113256/https://github.com/jserv/codezero |archive-date=2015-08-15}}</ref> and a version that was relicensed by B Labs Ltd., acquired by [[Nvidia]], as closed source and forked in 2010.<ref>{{cite web |url=http://l4dev.org/ |title=Code Zero : Embedded Hypervisor and OS |access-date=25 January 2016 |url-status=dead |archive-url=https://web.archive.org/web/20160111122321/http://l4dev.org/ |archive-date=11 January 2016}}</ref><!-- clarify OKL4 and Iggy license |date=February 2015 --><ref>{{cite web |url=http://dev.b-labs.com/ |title=B Labs &#124; Mobile Virtualization solutions, Android and Linux virtualization for the ARM architecture |access-date=2 February 2014 |url-status=dead |archive-url=https://web.archive.org/web/20140202174213/http://dev.b-labs.com/ |archive-date=2 February 2014}}</ref>

F9 microkernel,<ref>{{cite web |url=https://github.com/f9micro |title=F9 Microkernel |website=[[GitHub]] |access-date=2020-10-20}}</ref> a BSD-licensed L4 implementation, is dedicated to [[ARM Cortex-M]] processors for deeply embedded devices with memory protection.

The NOVA OS Virtualization Architecture<ref>{{cite web |url=https://hypervisor.org/ |title=NOVA Microhypervisor website |access-date=2021-01-09}}</ref> is a research project with focus on constructing a secure and efficient virtualization environment<ref name="Steinberg_Kauer_EuroSys_2010">
{{cite conference
 |last1=Steinberg |first1=Udo
 |last2=Kauer |first2=Bernhard
 |title = NOVA: A Microhypervisor-Based Secure Virtualization Architecture
 |book-title = EuroSys '10: Proceedings of the 5th European Conference on Computer Systems
 |date=April 2010
 |location = [[Paris, France]]
}}</ref><ref name="Steinberg_Kauer_IIDS_2010">
{{cite conference
 |last1=Steinberg |first1=Udo
 |last2=Kauer |first2=Bernhard
 |title=Towards a Scalable Multiprocessor User-level Environment
 |book-title = IIDS'10: Workshop on Isolation and Integration for Dependable Systems
 |date=April 2010
 |location=[[Paris, France]]
}}</ref>
with a small trusted computing base. NOVA consists of a microhypervisor, a user level [[hypervisor]] ([[virtual machine]] monitor), and an unprivileged componentised multi-server user environment running on it named NUL. NOVA runs on ARMv8-A and x86-based multi-core systems.

WrmOS<ref>{{cite web |url=https://wrmlab.org/projects/wrmos |title= WrmOS |access-date=2020-10-20}}</ref> is a [[real-time operating system]] based on L4 microkernel. It has own implementations of kernel, standard libraries, and network stack, supporting ARM, SPARC, x86, and x86-64 architectures. There is the paravirtualized Linux kernel (w4linux<ref>{{cite web |url=https://wrmlab.org/projects/w4linux |title=w4linux is paravirtualized Linux kernel working on WrmOS |access-date=2020-10-20}}</ref>) working on WrmOS.

Helios is a microkernel inspired by seL4.<ref>{{Cite web |title=~sircmpwn/helios – An experimental microkernel – sourcehut git |url=https://git.sr.ht/~sircmpwn/helios |access-date=2023-02-20 |website=git.sr.ht}}</ref> It is part of the Ares operating system, supports x86-64 and aarch64 and is still under active development as of February 2023.<ref>{{Cite web |title=Helios |url=https://ares-os.org/docs/helios/ |access-date=2023-02-20 |website=ares-os.org |language=en-us}}</ref>

== See also ==
* [[PikeOS]]

== References ==
{{Reflist|colwidth=30em}}

== Further reading ==
* {{cite journal
 |first1=Jochen |last1=Liedtke |author-link=Jochen Liedtke
 |first2=Ulrich |last2=Bartling
 |first3=Uwe |last3=Beyer
 |first4=Dietmar |last4=Heinrichs
 |first5=Rudolf |last5=Ruland
 |first6=Gyula |last6=Szalay
 |title=Two years of experience with a μ-Kernel based OS
 |journal=ACM SIGOPS Operating Systems Review
 |volume=25 |issue=2 |date=April 1991
 |pages=51–62
 |doi=10.1145/122120.122124
 |s2cid=17602151 |doi-access=free
}} 
* {{Cite conference
 |last1=Liedtke |first1=Jochen |author-link=Jochen Liedtke
 |last2=Haeberlen |first2=Andreas
 |last3=Park |first3=Yoonho
 |last4=Reuther |first4=Lars
 |last5=Uhlig |first5=Volkmar
 |date = 2000-10-22
 |title = Stub-Code Performance is Becoming Important
 |book-title = Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), San Diego, CA, October 2000
 |url = http://l4ka.org/publications/
 |format = PDF
 |access-date = 2006-09-05
 |url-status = dead
 |archive-url = https://web.archive.org/web/20060905181634/http://www.l4ka.org/publications/
 |archive-date = 2006-09-05
}} (on L4 kernel and compiler)
* {{cite report |last1=Cheng |first1=Guanghui |last2=McGuire |first2=Nicholas |url=http://dslab.lzu.edu.cn:8080/docs/publications/l4_kickstart.pdf |title=L4/Fiasco/L4Linux Kickstart |website=Distributed & Embedded Systems Lab |publisher=Lanzhou University|archive-url=https://web.archive.org/web/20120327161621/http://dslab.lzu.edu.cn:8080/docs/publications/l4_kickstart.pdf |archive-date=27 March 2012 }}
* {{Cite conference
 |last1=Elphinstone |first1=Kevin
 |last2=Heiser |first2=Gernot |author2-link=Gernot Heiser
 |date = November 2013
 |title = From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?
 |book-title = 24th ACM SIGOPS Symposium on Operating Systems Principles
 |location = Farmington, PA, USA
 |pages = 133–150 |doi=10.1145/2517349.2522720 |isbn=978-1-4503-2388-8 |citeseerx=10.1.1.636.9410 
 |url =https://sigops.org/s/conferences/sosp/2013/talks/elphinstone_l3sel4_se03_03.pdf
}} Evolution of L4 design and implementation approaches

== External links ==
* {{Webarchive|url=https://web.archive.org/web/20191025002913/http://www.l4hq.org/ L4Hq: L4 headquarters, community site for L4 projects}}
* [http://os.inf.tu-dresden.de/L4/ The L4 μ-Kernel Family], overview of L4 implementations, documentation, projects
* [http://wiki.tudos.org Official TUD:OS Wiki]
* [http://www.l4ka.org L4Ka]: Implementations L4Ka::Pistachio and L4Ka::Hazelnut
* {{Official website|sel4.systems}}, seL4
* [http://www.cse.unsw.edu.au/~disy/L4/ UNSW]: Implementations for [[DEC Alpha]] and [[MIPS architecture]]
* {{Webarchive|url=https://web.archive.org/web/20080820043831/http://okl4.org/ OKL4}}: Commercial L4 version from {{Webarchive|url=https://web.archive.org/web/20090319021316/http://www.ok-labs.com/ Open Kernel Labs}}
* {{Webarchive|url=https://web.archive.org/web/20140717185304/http://www.ertos.nicta.com.au/research/l4/ NICTA L4]: Research Overview and Publications}}
* [https://trustworthy.systems Trustworthy Systems Group at CSIRO's Data61]: Present home of the former NICTA group that developed seL4
* [http://genode.org/about/index Genode Operating System Framework]: An offspring of the L4 community

{{Microkernel}}
{{Object-capability security}}
{{Linux Foundation}}

[[Category:Capability systems]]
[[Category:Microkernels]]
[[Category:Assembly language software]]