L4 microkernel family

Source: Wikipedia, the free encyclopedia.

L4 microkernel family
ARM, MIPS, SPARC, Itanium, RISC-V
Kernel typeMicrokernel
LicenseSource code, proofs: GPLv2
Libraries, tools: BSD 2-clause
Preceded byEumel
Official websiteos.inf.tu-dresden.de/L4

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 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.[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.

There have been various re-implementations of the original L4

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
and its different versions.

L4 is widely deployed. One variant, OKL4 from Open Kernel Labs, shipped in billions of mobile devices.[3][4]

Design paradigm

Specifying the general idea of a microkernel, 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 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

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

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 May 2019) (named L4Linux).

University of New South Wales and NICTA

Development also occurred at the

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, at their new home at NICTA (formerly National ICT Australia, Ltd.), forked L4Ka::Pistachio into a new L4 version named NICTA::L4-embedded. As the name implies, 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 to ensure high real-time responsiveness.[11]

Commercial deployment

In November 2005,

SymbianOS and Android
. OK Labs also acquired the rights to seL4 from NICTA.

OKL4 shipments exceeded 1.5 billion in early 2012,

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

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

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]

On 29 July 2014,

General Dynamics C4 Systems announced that seL4, with end to end proofs, was now released under open-source licenses.[22]
The kernel source code and proofs are licensed under GNU General Public License version 2 (GPLv2), and most libraries and tools are under the 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.[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 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 (

Small Business Innovative Research (SBIR) contracts related to seL4 under a program started by Dr. 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.

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.[28]

RedoxOS[29] is a Rust based operating system, that is also inspired by seL4, and uses a micro kernel design.

CodeZero

GPL-licensed version,[31] and a version that was relicensed by B Labs Ltd., acquired by Nvidia, as closed source and forked in 2010.[32][33]

F9 microkernel,[34] a BSD-licensed L4 implementation, is dedicated to ARM Cortex-M processors for deeply embedded devices with memory protection.

The NOVA OS Virtualization Architecture[35] is a research project with focus on constructing a secure and efficient virtualization environment[36][37] 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[38] 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[39]) working on WrmOS.

Helios is a microkernel inspired by seL4.[40] It is part of the Ares operating system, supports x86-64 and aarch64 and is still under active development as of February 2023.[41]

See also

References

  1. ^ a b Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–188.
  2. ^ a b c Liedtke, Jochen (December 1995). "On µ-Kernel Construction". Proceedings 15th ACM Symposium on Operating Systems Principles (SOSP). pp. 237–250. Archived from the original on 25 October 2015.
  3. ^ "Hypervisor Products: General Dynamics Mission Systems". General Dynamics Mission Systems. Archived from the original on 15 November 2017. Retrieved 26 April 2018.
  4. ^ a b "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. 19 January 2012. Archived from the original on 11 February 2012.
  5. ^ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars (2000). "The Sawmill multiserver approach". ACM SIGOPS European Workshop. Kolding, Denmark. pp. 109–114.
  6. Dresden University of Technology. Archived
    from the original on 7 August 2011. Retrieved 10 August 2011.
  7. ^ 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..."
  8. ^ 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.
  9. S2CID 1121537
    .
  10. ^ van Schaik, Carl; Heiser, Gernot (January 2007). "High-performance microkernels and virtualisation on ARM and segmented architectures". 1st International Workshop on Microkernels for Embedded Systems. Sydney, Australia: NICTA. pp. 11–21. Archived from the original on 1 March 2015. Retrieved 25 October 2015.
  11. S2CID 7430332
    .
  12. ^ "NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions" (Press release). NICTA. 24 November 2005. Archived from the original on 25 August 2006.
  13. ^ "Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. 27 March 2012. Archived from the original on 2 July 2012.
  14. ^ "iOS Security, iOS 12.3" (PDF). Apple Inc. May 2019. Archived (PDF) from the original on 24 June 2020.
  15. ^ Mandt, Tarjei; Solnik, Mathew; Wang, David (31 July 2016). "Demystifying the Secure Enclave Processor" (PDF). BlackHat USA. Las Vegas, Nevada, USA. Archived (PDF) from the original on 21 October 2016.
  16. ^ Elmer-DeWitt, Philip (28 October 2014). "Forecast: Apple will ship 310 million iOS devices in 2015". Fortune. Archived from the original on 27 September 2015. Retrieved 25 October 2015.
  17. ^ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Cock, David; Chakravarty, Manuel M. T. (September 2006). "Running the manual: an approach to high-assurance microkernel development". ACM SIGPLAN Haskell Workshop. Portland, Oregon. pp. 60–71.
  18. ^ a b 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.
  19. ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). Kernel design for isolation and assurance of physical memory. 1st Workshop on Isolation and Integration in Embedded Systems. Glasgow, UK.
    doi:10.1145/1435458. Archived from the original
    on 22 February 2020. Retrieved 22 February 2020.
  20. ^ a b Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal;
    S2CID 4474342
    .
  21. doi:10.1145/2491956.2462183
    .
  22. ^ "Secure operating system developed by NICTA goes open source" (Press release). NICTA. 29 July 2014. Archived from the original on 15 March 2016.
  23. ^ "Security Gets Support of Linux Foundation" (Press release). Linux Foundation. 7 April 2020. Archived from the original on 15 March 2016.
  24. S2CID 4474342. Archived
    (PDF) from the original on 3 August 2014.
  25. ^ Heiser, Gernot (16 January 2015). seL4 Is Free: What Does This Mean for You?. Auckland, New Zealand: Linux.conf.au.
  26. ^ "DARPA selects Rockwell Collins to apply cybersecurity technology to new platforms" (Press release). Rockwell Collins. 24 April 2017. Archived from the original on 11 May 2017.
  27. ^ "DARPA Agency Sponsor Dr. John Launchbury". SBIRSource. 2017. Archived from the original on 29 September 2017. Retrieved 16 May 2017.
  28. ^ Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). ACM SIGPLAN Notices. 40 (9): 116–128.
    ISSN 0362-1340. Archived
    (PDF) from the original on 15 June 2010. Retrieved 24 June 2010.
  29. ^ "RedoxOS". RedoxOS.
  30. Dresden University of Technology
    .
  31. ^ "jserv/codezero: Codezero Microkernel". GitHub. Archived from the original on 15 August 2015. Retrieved 20 October 2020.
  32. ^ "Code Zero : Embedded Hypervisor and OS". Archived from the original on 11 January 2016. Retrieved 25 January 2016.
  33. ^ "B Labs | Mobile Virtualization solutions, Android and Linux virtualization for the ARM architecture". Archived from the original on 2 February 2014. Retrieved 2 February 2014.
  34. ^ "F9 Microkernel". GitHub. Retrieved 20 October 2020.
  35. ^ "NOVA Microhypervisor website". Retrieved 9 January 2021.
  36. ^ 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
    .
  37. ^ 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
    .
  38. ^ "WrmOS". Retrieved 20 October 2020.
  39. ^ "w4linux is paravirtualized Linux kernel working on WrmOS". Retrieved 20 October 2020.
  40. ^ "~sircmpwn/helios – An experimental microkernel – sourcehut git". git.sr.ht. Retrieved 20 February 2023.
  41. ^ "Helios". ares-os.org. Retrieved 20 February 2023.

Further reading

External links
Retrieved from "https://en.wikipedia.org/w/index.php?title=L4_microkernel_family&oldid=1220419492"