L4 microkernel family

L4 is a family of second-generation microkernels, generally used to implement Unix-like operating systems, but also used in a variety of other systems.

L4, like its predecessor L3 was created by German computer scientist Jochen Liedtke as a response to the poor performance of earlier microkernel-based operating systems. 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 sparked off intense interest in the computer industry. Since its introduction, L4 has been developed for platform independence and also in improving security, isolation, and robustness.

There have been various re-implementations of the original binary L4 kernel interface (ABI) and its successors, including L4Ka::Pistachio (Uni Karlsruhe), L4/MIPS (UNSW) and Fiasco (TU Dresden). For this reason, the name L4 has been generalized and no longer only refers to 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.[1]

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, in order 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. 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 IPC layer, with careful attention to performance and machine-specific (as opposed to platform independent) design could yield massive real-world performance improvements. Instead of Mach's complex IPC system, his L3 microkernel simply passed the message without any additional 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 necessary 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 TÜV SÜD.

L4 family tree

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 with high performance in mind. In order to wring out every bit of performance the entire kernel was written in assembly language, and its IPC was 20 times faster than Mach's.[3] 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.[4]

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 (Dresden University of Technology) started to develop their own C++ implementation of the L4 kernel interface, called L4/Fiasco. In contrast to L4Ka::Hazelnut, which does not allow concurrency in the kernel at all 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,[5] a hard real-time capable operating system, also developed at the TU Dresden. However, the complexities of a fully preemptible design resulted in 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.

Platform independence

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 platform-independent 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 radical changes to previous 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 as well as portability. It was released under the two-clause BSD license.

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 (FiascoUX) is able to run as a user-level application on top of 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. Furthermore, Fiasco contains mechanisms for controlling communication rights as well as kernel-level resource consumption. On top of Fiasco a collection of basic user level services are developed (called L4Env) that amongst others are used to para-virtualise current Linux version (2.6.x) (called L4Linux).

University of New South Wales and NICTA

Development also took place 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 retroactively named L4/x86. Like Liedtke's original kernels, the UNSW kernels (written in a mixture 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 favour of producing highly tuned ports of L4Ka::Pistachio, including the fastest-ever reported implementation of message passing (36 cycles on the Itanium architecture).[6] The group has also demonstrated that user-level device drivers can perform as well as in-kernel drivers,[7] and developed Wombat, a highly portable version of Linux on L4 that runs on x86, ARM and MIPS processors. On XScale processors, Wombat demonstrates context-switching costs that are up to 30 times lower than in native Linux.[8]

Later the UNSW group, at their new home at NICTA, forked L4Ka::Pistachio into a new L4 version called NICTA::L4-embedded. As the name implies, this was aimed at use in commercial embedded systems, and consequently the implementation trade-offs favoured small memory footprints and aimed to reduce complexity. The API was modified to keep almost all system calls short enough so they do not require preemption points in order to ensure high real-time responsiveness.[9]

Commercial deployment

In November 2005, NICTA announced[10] 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 called 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 Version 2.1, released in April 2008, was the first generally available version of L4 which featured capability-based security. OKL4 3.0, released in October 2008, was the last open-source version of OKL4. More recent versions are closed source and based on a rewrite to support a native hypervisor variant called the OKL4 Microvisor. OK Labs also distributed a paravirtualized Linux called OK:Linux, a descendant of Wombat, as well as 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,[1] mostly on Qualcomm wireless modem chips. Other deployments include automotive infotainment systems.[11]

The Apple A7 chip contains a Secure Enclave processor running an L4 operating system,[12] based on the L4 version used in NICTA's Darbat project. This implies that L4 is now shipping on all iOS devices, the total shipment of which is estimated at 310 million for the year 2015.[13]

High assurance: seL4

In 2006 the NICTA group commenced a from-scratch design of a third-generation microkernel, called 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 Haskell.[14] seL4 uses capability-based access control to enable formal reasoning about object accessibility.

A formal proof of functional correctness was completed in 2009.[15] 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.[15]

seL4 takes a novel approach to kernel resource management,[16] 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.[17] The NICTA team also proved correctness of the translation from C to executable machine code, taking the compiler out of the trusted computing base of seL4. 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 systems.[17]

On 29 July 2014, NICTA and General Dynamics C4 Systems announced that seL4, with end to end proofs, was now released under open source licenses.[18] The kernel source and proofs are under GPLv2, and most libraries and tools are under the 2-clause BSD license.

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.[19] 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.[20]

Under the DARPA High-Assurance Cyber Military Systems (HACMS) program, NICTA together with project partners Rockwell Collins, Galois Inc, the University of Minnesota and Boeing are developing a high-assurance drone based on seL4, with planned technology transfer onto the optionally piloted autonomous Unmanned Little Bird helicopter under development by Boeing.

Other research and development

Osker, an OS written in Haskell, targeted the L4 specification; although this project focused on the use of a functional programming language for OS development, not on microkernel research per se.[21]

CodeZero is an L4 microkernel targeting embedded systems with a focus on virtualization and implementation of native OS services. There is a GPL-licensed version,[22] and a version that was relicensed by the developers as closed source and forked in 2010.[23]

F9 microkernel, a BSD-licensed L4 implementation, is built from scratch for deeply embedded devices with performance on ARM Cortex-M3/M4 processors, power consumption, and memory protection in mind.

Fiasco.OC is a third generation microkernel, which evolved from its predecessor L4/Fiasco. Fiasco.OC is capability based, supports multi-core systems and hardware assisted virtualization.[24] The completely redesigned user-land environment running on top of Fiasco.OC is called L4 Runtime Environment (L4Re). It provides the framework to build multi-component systems, including a client/server communication framework, common service functionality, a virtual file-system infrastructure and popular libraries such as a C library, libstdc++ and pthreads. The platform also offers L4Linux, the multi-architecture virtualized Linux system. L4Re and Fiasco.OC run on x86 (IA-32 and AMD64), ARM and PowerPC (WiP), and supersede the previous system with L4Env and L4/Fiasco.

The NOVA OS Virtualization Architecture is a research project with focus on constructing a secure and efficient virtualization environment[25][26] with a small trusted computing base. NOVA consists of a microhypervisor, a user level virtual-machine monitor, and an unprivileged componentised multi-server user environment running on top of it called NUL. NOVA runs on x86-based multi-core systems.

References

  1. 1 2 "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (Press release). Open Kernel Labs. January 19, 2012. Archived from the original on February 11, 2012.
  2. 1 2 Liedtke, Jochen (December 1995). "On µ-Kernel Construction". Proc. 15th ACM Symposium on Operating Systems Principles (SOSP). pp. 237–250. Archived from the original on October 25, 2015.
  3. ↑ Liedtke, Jochen (December 1993). "Improving IPC by kernel design". 14th ACM Symposium on Operating System Principles. Asheville, NC, USA. pp. 175–88.
  4. ↑ 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.
  5. ↑ http://os.inf.tu-dresden.de/drops/overview.html
  6. ↑ 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. Cite uses deprecated parameter |coauthors= (help)
  7. ↑ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). "User-level device drivers: achieved performance". Journal of Computer Science and Technology 20 (5): 654–664. doi:10.1007/s11390-005-0654-4. Cite uses deprecated parameter |coauthors= (help)
  8. ↑ 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 2015-03-01. Retrieved 2015-10-25.
  9. ↑ Ruocco, Sergio (October 2008). "A Real-Time Programmer's Tour of General-Purpose L4 Microkernels". EURASIP Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications 2008: 1–14. doi:10.1155/2008/234710.
  10. ↑ "NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions" (Press release). NICTA. November 24, 2005. Archived from the original on August 25, 2006.
  11. ↑ "Open Kernel Labs Automotive Virtualization Selected by Bosch for Infotainment Systems" (Press release). Open Kernel Labs. March 27, 2012. Archived from the original on July 2, 2012.
  12. ↑ "iOS Security" (PDF).
  13. ↑ Elmer-DeWitt, Philip (October 28, 2014). "Forecast: Apple will ship 310 million iOS devices in 2015". Fortune. Archived from the original on October 25, 2015. Retrieved October 25, 2015.
  14. ↑ 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.
  15. 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.
  16. ↑ 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.
  17. 1 2 Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (February 2014). "Comprehensive Formal Verification of an OS Microkernel". ACM Transactions on Computer Systems 32 (1): 2:1–2:70. doi:10.1145/2560537.
  18. ↑ "Secure operating system developed by NICTA goes open source" (Press release). NICTA. July 29, 2014.
  19. ↑ Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Comprehensive formal verification of an OS microkernel" (PDF). ACM Transactions on Computer Systems 32: 64. doi:10.1145/2560537.
  20. ↑ seL4 Is Free – What Does This Mean For You? on YouTube
  21. ↑ Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "A principled approach to operating system construction in Haskell" (PDF). Proceedings of the tenth ACM SIGPLAN international conference on Functional programming 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Retrieved 2010-06-24.
  22. ↑ "jserv/codezero: Codezero Microkernel". Retrieved 2016-01-25.
  23. ↑ http://l4dev.org/
  24. ↑ Peter, Michael; Schild, Henning; Lackorzynski, Adam; Warg, Alexander (March 2009). "Virtual Machines Jailed - Virtualization in Systems with Small Trusted Computing Bases". VTDS'09: Workshop on Virtualization Technology for Dependable Systems. Nuremberg, Germany.
  25. ↑ Steinberg, Udo; Bernhard, Kauer (April 2010). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems. Paris, France.
  26. ↑ Steinberg, Udo; Bernhard, Kauer (April 2010). "Towards a Scalable Multiprocessor User-level Environment". IIDS'10: Workshop on Isolation and Integration for Dependable Systems. Paris, France.

Further reading

External links

This article is issued from Wikipedia - version of the Tuesday, January 26, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.