| Developer | Jochen Liedtke |
|---|---|
| Written in | Assembly language, thenC,C++ |
| OS family | L4 |
| Working state | Current |
| Source model | Open source,closed source |
| Initial release | 1993; 32 years ago (1993) |
| Marketing target | Reliable computing |
| Available in | English, German |
| Platforms | Inteli386,x86,x86-64,ARM,MIPS,SPARC,Itanium,RISC-V |
| Kernel type | Microkernel |
| License | Source code,proofs:GPLv2 Libraries,tools:BSD 2-clause |
| Preceded by | Eumel |
| Official website | os |
L4 is a family of second-generationmicrokernels, used to implement a variety of types ofoperating systems (OS), though mostly forUnix-like,Portable Operating System Interface (POSIX) compliant types.
L4, like its predecessor microkernelL3, was created byGermancomputer scientistJochen 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 Inteli386-specificassembly language code in 1993 created attention by being 20 times faster thanMach.[1]The follow-up publication two years later[2] was considered so influential that it won the 2015ACM SIGOPS Hall of Fame Award.Since its introduction, L4 has been developed to becross-platform and to improvesecurity, isolation, androbustness.
There have been various re-implementations of the original L4kernelapplication binary interface (ABI) and its successors, includingL4Ka::Pistachio (implemented by Liedtke and his students atKarlsruhe Institute of Technology),L4/MIPS (University of New South Wales (UNSW)),Fiasco (Dresden University of Technology (TU Dresden)). For this reason, the nameL4 has been generalized and no longer refers to only Liedtke's original implementation. It now applies to the wholemicrokernel family including the L4 kernelinterface and its different versions.
L4 is widely deployed. One variant, OKL4 fromOpen Kernel Labs, shipped in billions of mobile devices.[3][4]
Specifying the general idea of amicrokernel,Liedtke states:
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.[2]
In this spirit, the L4 microkernel provides few basic mechanisms:address spaces (abstracting page tables and providing memory protection),threads andscheduling (abstracting execution and providing temporal protection), andinter-process communication (for controlled communication across isolation boundaries).
An operating system based on a microkernel like L4 provides services as servers inuser space thatmonolithic kernels likeLinux or older generation microkernels include internally. For example, to implement a secureUnix-like system, servers must provide the rights management thatMach included inside the kernel.
The poor performance of first-generation microkernels, such asMach, led a number of developers to re-examine the entire microkernel concept in the mid-1990s. The asynchronous in-kernel-bufferingprocess 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] 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, itsworking set is too large: the IPC code expresses poor spatial locality; that is, it results in too manycache misses, of which most are in-kernel.[2] 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).
Jochen Liedtke set out to prove that a well-designed thinnerinter-process communication (IPC) layer, with careful attention to performance and machine-specific (in contrast tocross-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 theuser 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 robustoperating system, used for many years for example byTechnischer Überwachungsverein (Technical Inspection Association).[citation needed]
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 inassembly language, and its IPC was 20 times faster than Mach's.[1] 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, includingIBM, where Liedtke started to work in 1996, TU Dresden and UNSW. At IBM'sThomas J. Watson Research Center Liedtke and his colleagues continued research on L4 and microkernel based systems in general, especially the Sawmill OS.[5]
In 1999, Liedtke took over the Systems Architecture Group at theUniversity 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 developedL4Ka::Hazelnut, aC++ version of the kernel that ran onIA-32- andARM-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.
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 lowinterrupt latency. This was considered necessary because L4/Fiasco is used as the basis of DROPS,[6] a hardreal-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.
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 thetwo-clause BSD license.[7]
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 ofalien threads, 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 May 2019[update]) (namedL4Linux).
Development also occurred at theUniversity of New South Wales (UNSW), where developers implemented L4 on several 64-bit platforms. Their work resulted inL4/MIPS andL4/Alpha, resulting in Liedtke's original version being retrospectively namedL4/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 theItanium architecture).[8] The group has also demonstrated thatdevice drivers can perform equally well at user-level as in-kernel,[9] and developedWombat, a highly portable version ofLinux on L4 that runs onx86,ARM, andMIPS processors. OnXScale processors, Wombat context-switching costs are up to 50 times lower than in native Linux.[10]
Later the UNSW group, now atNICTA (formerlyNational ICT Australia, Ltd.), forked L4Ka::Pistachio into a new L4 version namedNICTA::L4-embedded. It was for use in commercialembedded systems, 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.[11]
In November 2005,NICTA announced[12] thatQualcomm was deploying NICTA's L4 version on theirMobile Station Modem chipsets. This led to the use of L4 inmobile phone handsets on sale from late 2006. In August 2006, ERTOS leader and UNSW professorGernot Heiser spun out a company namedOpen Kernel Labs (OK Labs) to support commercial L4 users and further develop L4 for commercial use under the brand nameOKL4, in close collaboration with NICTA.OKL4 μKernel Version 2.1, released in April 2008, was the firstgenerally available version of L4 which featuredcapability-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 theOKL4 Microvisor. OK Labs also distributed a paravirtualized Linux named OK:Linux, a descendant of Wombat, and paravirtualized versions ofSymbianOS andAndroid. OK Labs also acquired the rights toseL4 from NICTA.
OKL4 shipments exceeded 1.5 billion in early 2012,[4] mostly on Qualcomm wireless modem chips. Other deployments includeautomotive infotainment systems.[13]
Apple A series processors beginning with theA7 contain a Secure Enclavecoprocessor running an L4 operating system[14] called sepOS (Secure Enclave Processor OS)based on the L4-embedded kernel developed atNICTA in 2006.[15]As a result, L4 ships on all modern Apple devices including Macs withApple silicon. In 2015 alone, total shipments of iPhone was estimated at 310 million.[16]
In 2006, theNICTA group commenced a from-scratch design of athird-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 ofCommon Criteria and beyond. From the beginning, development aimed forformal verification of the kernel. To ease meeting the sometimes conflicting requirements of performance and verification, the team used amiddle-out software process starting from an executablespecification written in the languageHaskell.[17]seL4 usescapability-based security access control to enable formal reasoning about object accessibility.
Aformal proof of functional correctness was completed in 2009.[18]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 asdeadlocks,livelocks,buffer overflows, arithmetic exceptions or use ofuninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.[18] The work on seL4 won the 2019ACM SIGOPS Hall of Fame Award.
seL4 takes a novel approach to kernel resource management,[19] exporting the management of kernel resources to user level and subjects them to the samecapability-based access control as user resources. This model, which was also adopted byBarrelfish, simplifies reasoning about isolation properties, and was an enabler for later proofs that seL4 enforces the core security properties of integrity and confidentiality.[20] The NICTA team also proved correctness of the translation from the programming languageC to executablemachine code, taking thecompiler out of thetrusted computing base of seL4.[21]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 soundworst-case execution time (WCET) analysis, a prerequisite for its use in hardreal-time computing.[20]
On 29 July 2014,NICTA andGeneral Dynamics C4 Systems announced that seL4, with end to end proofs, was now released underopen-source licenses.[22]The kernelsource code and proofs arelicensed underGNU General Public License version 2 (GPLv2), and mostlibraries andtools are under theBSD 2-clause. In April 2020, it was announced that the seL4 Foundation was created under the umbrella of theLinux Foundation to accelerate development and deployment of seL4.[23]
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.[24] Specifically, the cost of oneline of code during the development of seL4 was estimated at aroundUS$400, compared toUS$1,000 for traditional high-assurance systems.[25]
Under the Defense Advanced Research Projects Agency (DARPA) High-Assurance Cyber Military Systems (HACMS) program, NICTA together with project partnersRockwell Collins, Galois Inc, theUniversity of Minnesota andBoeing developed a high-assurance drone using seL4, along with other assurance tools and software, with planned technology transfer onto the optionally piloted autonomousBoeing AH-6 Unmanned Little Bird helicopter being developed by Boeing. Final demonstration of the HACMS technology took place in Sterling, VA in April 2017.[26] DARPA also funded severalSmall Business Innovative Research (SBIR) contracts related to seL4 under a program started byJohn Launchbury. Small businesses receiving an seL4-related SBIR included: DornerWorks, Techshot, Wearable Inc, Real Time Innovations, and Critical Technologies.[27]
In October 2023,Nio Inc. announced that their seL4-based SkyOS operating systems will be in mass-produced electric cars from 2024.[28]
In 2023, seL4 won theACM Software System Award.
Osker, an OS written inHaskell, targeted the L4 specification; although this project focused mainly on the use of afunctional programming language for OS development, not on microkernel research.[29]
RedoxOS[30] is a Rust based operating system, that is also inspired by seL4, and uses a micro kernel design.
CodeZero[31] is an L4 microkernel for embedded systems with a focus on virtualization and implementation of native OS services. There is aGPL-licensed version,[32] and a version that was relicensed by B Labs Ltd., acquired byNvidia, as closed source and forked in 2010.[33][34]
F9 microkernel,[35] a BSD-licensed L4 implementation, is dedicated toARM Cortex-M processors for deeply embedded devices with memory protection.
The NOVA OS Virtualization Architecture[36] is a research project with focus on constructing a secure and efficient virtualization environment[37][38]with a small trusted computing base. NOVA consists of a microhypervisor, a user levelhypervisor (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[39] is areal-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[40]) working on WrmOS.
Helios is a microkernel inspired by seL4.[41] It is part of the Ares operating system, supports x86-64 and aarch64 and is still under active development as of February 2023.[42]
{{cite journal}}: CS1 maint: DOI inactive as of November 2024 (link)| Kernels |
| ||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Operating systems |
| ||||||||||||||||||||||||
| Frameworks,kits | |||||||||||||||||||||||||
| Developers | |||||||||||||||||||||||||
| |||||||||||||||||||||||||
