L4 is a family of second-generation microkernels, used to implement a variety of types of operating systems (OS), though mostly for Unix-like, Portable Operating System Interface (POSIX) compliant types.
L4, like its predecessor microkernel L3, was created by Germancomputer 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 Intel i386-specific assembly language code in 1993 created attention by being 20 times faster than Mach.[1] The follow-up publication two years later[2] 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 and to improve security, isolation, and robustness.
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 and 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 kernels 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 included inside the kernel.
History
The poor performance of first-generation microkernels, such as Mach, led a number of developers to re-examine the entire microkernel concept in the mid-1990s. The asynchronous in-kernel-buffering 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] 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 cache 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).
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]
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.[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, 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.[5]
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-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,[6] 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 two-clause BSD license.[7]
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 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 May2019[update]) (named L4Linux).
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).[8] The group has also demonstrated that device drivers can perform equally well at user-level as in-kernel,[9] and developed Wombat, a highly portable version of Linux on L4 that runs on x86, ARM, and MIPS processors. On XScale processors, Wombat context-switching costs are up to 50 times lower than in native Linux.[10]
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 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]
Commercial deployment
In November 2005, NICTA announced[12] 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 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. OK Labs also acquired the rights to seL4 from NICTA.
OKL4 shipments exceeded 1.5 billion in early 2012,[4] mostly on Qualcomm wireless modem chips. Other deployments include automotive infotainment systems.[13]
Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system[14] called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.[15] 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.[16]
High assurance: seL4
In 2006, the NICTA group commenced a from-scratch design of a 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.[17] seL4 uses capability-based security access control to enable formal reasoning about object accessibility.
A formal 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 as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised 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 2019 ACM 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 same capability-based access control as user resources. This model, which was also adopted by Barrelfish, 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 language C to executable machine code, taking the compiler out of the trusted 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 sound worst-case execution time (WCET) analysis, a prerequisite for its use in hard real-time computing.[20]
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 one line of code during the development of seL4 was estimated at around US$400, compared to US$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 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.[26] 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.[27]
In October 2023, Nio Inc. announced that their seL4-based SkyOS operating systems will be in mass-produced electric cars from 2024.[28]
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.[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 a GPL-licensed version,[32] and a version that was relicensed by B Labs Ltd., acquired by Nvidia, as closed source and forked in 2010.[33][34]
F9 microkernel,[35] a BSD-licensed L4 implementation, is dedicated to ARM 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 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[39] 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[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]
GNU Hurd is a collection of microkernel servers written as part of GNU, for the GNU Mach microkernel. It has been under development since 1990 by the GNU Project of the Free Software Foundation, designed as a replacement for the Unix kernel, and released as free software under the GNU General Public License. When the Linux kernel proved to be a viable solution, development of GNU Hurd slowed, at times alternating between stasis and renewed activity and interest.
In computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system (OS). These mechanisms include low-level address space management, thread management, and inter-process communication (IPC).
Mach is a kernel developed at Carnegie Mellon University by Richard Rashid and Avie Tevanian to support operating system research, primarily distributed and parallel computing. Mach is often considered one of the earliest examples of a microkernel. However, not all versions of Mach are microkernels. Mach's derivatives are the basis of the operating system kernel in GNU Hurd and of Apple's XNU kernel used in macOS, iOS, iPadOS, tvOS, and watchOS.
The trusted computing base (TCB) of a computer system is the set of all hardware, firmware, and/or software components that are critical to its security, in the sense that bugs or vulnerabilities occurring inside the TCB might jeopardize the security properties of the entire system. By contrast, parts of a computer system that lie outside the TCB must not be able to misbehave in a way that would leak any more privileges than are granted to them in accordance to the system's security policy.
The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.
Capability-based security is a concept in the design of secure computing systems, one of the existing security models. A capability is a communicable, unforgeable token of authority. It refers to a value that references an object along with an associated set of access rights. A user program on a capability-based operating system must use a capability to access an object. Capability-based security refers to the principle of designing user programs such that they directly share capabilities with each other according to the principle of least privilege, and to the operating system infrastructure necessary to make such transactions efficient and secure. Capability-based security is to be contrasted with an approach that uses traditional UNIX permissions and Access Control Lists.
XNU is the computer operating system (OS) kernel developed at Apple Inc. since December 1996 for use in the Mac OS X operating system and released as free and open-source software as part of the Darwin OS, which, in addition to being the basis for macOS, is also the basis for Apple TV Software, iOS, iPadOS, watchOS, visionOS, and tvOS.
A hypervisor, also known as a virtual machine monitor (VMM) or virtualizer, is a type of computer software, firmware or hardware that creates and runs virtual machines. A computer on which a hypervisor runs one or more virtual machines is called a host machine, and each virtual machine is called a guest machine. The hypervisor presents the guest operating systems with a virtual operating platform and manages the execution of the guest operating systems. Unlike an emulator, the guest executes most instructions on the native hardware. Multiple instances of a variety of operating systems may share the virtualized hardware resources: for example, Linux, Windows, and macOS instances can all run on a single physical x86 machine. This contrasts with operating-system–level virtualization, where all instances must share a single kernel, though the guest operating systems can differ in user space, such as different Linux distributions with the same kernel.
Jochen Liedtke was a German computer scientist, noted for his work on microkernel operating systems, especially in creating the L4 microkernel family.
In computer science, a single address space operating system is an operating system that provides only one globally shared address space for all processes. In a single address space operating system, numerically identical logical addresses in different processes all refer to exactly the same byte of data.
A hybrid kernel is an operating system kernel architecture that attempts to combine aspects and benefits of microkernel and monolithic kernel architectures used in operating systems.
PikeOS is a commercial hard real-time operating system (RTOS) which features a separation kernel-based hypervisor. This hypervisor supports multiple logical partition types for various operating systems (OS) and applications, each referred to as a GuestOS. PikeOS is engineered to support the creation of certifiable smart devices for the Internet of Things (IoT), ensuring compliance with industry standards for quality, safety, and security across various sectors. In instances where memory management units (MMU) are not present but memory protection units (MPU) are available on controller-based systems, PikeOS for MPU is designed for critical real-time applications and provides up-to-standard safety and security.
Independent Group of Unix-Alikes and Networking Activists (IGUANA) are developers of the Wombat system.
Gernot Heiser is a Scientia Professor and the John Lions Chair for operating systems at UNSW Sydney, where he leads the Trustworthy Systems group (TS).
The kernel is a computer program at the core of a computer's operating system and generally has complete control over everything in the system. The kernel is also responsible for preventing and mitigating conflicts between different processes. It is the portion of the operating system code that is always resident in memory and facilitates interactions between hardware and software components. A full kernel controls all hardware resources via device drivers, arbitrates conflicts between processes concerning such resources, and optimizes the utilization of common resources e.g. CPU & cache usage, file systems, and network sockets. On most systems, the kernel is one of the first programs loaded on startup. It handles the rest of startup as well as memory, peripherals, and input/output (I/O) requests from software, translating them into data-processing instructions for the central processing unit.
Open Kernel Labs is a privately owned company that develops microkernel-based hypervisors and operating systems for embedded systems. The company was founded in 2006 by Steve Subar and Gernot Heiser as a spinout from NICTA. It was headquartered in Chicago, while research and development was located in Sydney, Australia. The company was acquired by General Dynamics in September 2012.
The REX Operating System is a real-time operating system (RTOS) developed by Qualcomm for the ARM processor based mobile phone Dual-Mode Subscriber Station (DMSS) or Advanced Mode Subscriber Software (AMSS) development. As of 2007, most Korean cell phones ran on REX.
In computing, Wombat is an operating system, a high-performance virtualised Linux embedded operating system marketed by Open Kernel Labs, a spin-off of National ICT Australia's Embedded, Real Time, Operating System Program.
Genode is a free and open-source software operating system (OS) framework consisting of a microkernel abstraction layer and a set of user space components. The framework is notable as one of the few open-source operating systems not derived from a proprietary OS, such as Unix. The characteristic design philosophy is that a small trusted computing base is of primary concern in a security-oriented OS.
↑ 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..."
↑ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium: A system implementor's tale". USENIX Annual Technical Conference. Annaheim, CA, USA. pp.264–278. Archived from the original on 17 February 2007.
↑ Ruocco, Sergio (October 2008). "A Real-Time Programmer's Tour of General-Purpose L4 Microkernels". EURASIP Journal on Embedded Systems. 2008: 1–14. doi:10.1155/2008/234710 (inactive 29 June 2024). S2CID7430332.{{cite journal}}: CS1 maint: DOI inactive as of June 2024 (link)
1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel"(PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA. Archived(PDF) from the original on 28 July 2011.
↑ Steinberg, Udo; Kauer, Bernhard (April 2010). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems. Paris, France.
↑ Steinberg, Udo; Kauer, Bernhard (April 2010). "Towards a Scalable Multiprocessor User-level Environment". IIDS'10: Workshop on Isolation and Integration for Dependable Systems. Paris, France.
Liedtke, Jochen; Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar (22 October 2000). "Stub-Code Performance is Becoming Important". Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), San Diego, CA, October 2000. Archived from the original(PDF) on 5 September 2006. Retrieved 5 September 2006. (on L4 kernel and compiler)
Cheng, Guanghui; McGuire, Nicholas. L4/Fiasco/L4Linux Kickstart(PDF). Distributed & Embedded Systems Lab (Report). Lanzhou University. Archived from the original(PDF) on 27 March 2012.
This page is based on this Wikipedia article Text is available under the CC BY-SA 4.0 license; additional terms may apply. Images, videos and audio are available under their respective licenses.
