L4 is a family of second-generation
microkernel
In computer science, a microkernel (often abbreviated as μ-kernel) 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, ...
s, used to implement a variety of types of
operating system
An operating system (OS) is system software that manages computer hardware, software resources, and provides common services for computer programs.
Time-sharing operating systems schedule tasks for efficient use of the system and may also in ...
s (OS), though mostly for
Unix-like
A Unix-like (sometimes referred to as UN*X or *nix) operating system is one that behaves in a manner similar to a Unix system, although not necessarily conforming to or being certified to any version of the Single UNIX Specification. A Unix-li ...
, ''Portable Operating System Interface'' (
POSIX
The Portable Operating System Interface (POSIX) is a family of standards specified by the IEEE Computer Society for maintaining compatibility between operating systems. POSIX defines both the system- and user-level application programming interf ...
) compliant types.
L4, like its predecessor microkernel
L3, was created by
German
German(s) may refer to:
* Germany (of or related to)
** Germania (historical use)
* Germans, citizens of Germany, people of German ancestry, or native speakers of the German language
** For citizens of Germany, see also German nationality law
**Ge ...
computer scientist
A computer scientist is a person who is trained in the academic study of computer science.
Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...
Jochen Liedtke
Jochen Liedtke (26 May 1953 – 10 June 2001) was a German computer scientist, noted for his work on microkernel operating systems, especially in creating the L4 microkernel family.
Vita
Education
In the mid-1970s Liedtke studied for a di ...
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
The Intel 386, originally released as 80386 and later renamed i386, is a 32-bit microprocessor introduced in 1985. The first versions had 275,000 transistors[assembly language
In computer programming, assembly language (or assembler language, or symbolic machine code), often referred to simply as Assembly and commonly abbreviated as ASM or asm, is any low-level programming language with a very strong correspondence be ...]
code in 1993 sparked intense interest in the computer industry. Since its introduction, L4 has been developed to be
cross-platform
In computing, cross-platform software (also called multi-platform software, platform-agnostic software, or platform-independent software) is computer software that is designed to work in several computing platforms. Some cross-platform software r ...
and to improve
security
Security is protection from, or resilience against, potential harm (or other unwanted coercive change) caused by others, by restraining the freedom of others to act. Beneficiaries (technically referents) of security may be of persons and social ...
, isolation, and
robustness
Robustness is the property of being strong and healthy in constitution. When it is transposed into a system, it refers to the ability of tolerating perturbations that might affect the system’s functional body. In the same line ''robustness'' ca ...
.
There have been various re-implementations of the original binary L4
kernel
Kernel may refer to:
Computing
* Kernel (operating system), the central component of most operating systems
* Kernel (image processing), a matrix used for image convolution
* Compute kernel, in GPGPU programming
* Kernel method, in machine learnin ...
application binary interface
In computer software, an application binary interface (ABI) is an interface between two binary program modules. Often, one of these modules is a library or operating system facility, and the other is a program that is being run by a user.
An ' ...
(ABI) and its successors, including ''L4Ka::Pistachio'' (
Karlsruhe Institute of Technology
The Karlsruhe Institute of Technology (KIT; german: Karlsruher Institut für Technologie) is a public research university in Karlsruhe, Germany. The institute is a national research center of the Helmholtz Association.
KIT was created in 2009 w ...
), ''L4/MIPS'' (
University of New South Wales
The University of New South Wales (UNSW), also known as UNSW Sydney, is a public research university based in Sydney, New South Wales, Australia. It is one of the founding members of Group of Eight, a coalition of Australian research-intensive ...
(UNSW)), ''Fiasco'' (
Dresden University of Technology
TU Dresden (for german: Technische Universität Dresden, abbreviated as TUD and often wrongly translated as "Dresden University of Technology") is a public research university, the largest institute of higher education in the city of Dresden, th ...
(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
In computer science, a microkernel (often abbreviated as μ-kernel) 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, ...
family including the L4 kernel
interface
Interface or interfacing may refer to:
Academic journals
* ''Interface'' (journal), by the Electrochemical Society
* '' Interface, Journal of Applied Linguistics'', now merged with ''ITL International Journal of Applied Linguistics''
* '' Int ...
and its different versions.
L4 is widely deployed. One variant, OKL4 from
Open Kernel Labs
Open Kernel Labs (OK 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 headq ...
, shipped in billions of mobile devices.
Design paradigm
Specifying the general idea of a
microkernel
In computer science, a microkernel (often abbreviated as μ-kernel) 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, ...
,
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.
In this spirit, the L4 microkernel provides few basic mechanisms:
address space
In computing, an address space defines a range of discrete addresses, each of which may correspond to a network host, peripheral device, disk sector, a memory cell or other logical or physical entity.
For software programs to save and retrieve st ...
s (abstracting page tables and providing memory protection),
threads and
scheduling
A schedule or a timetable, as a basic time-management tool, consists of a list of times at which possible task (project management), tasks, events, or actions are intended to take place, or of a sequence of events in the chronological order ...
(abstracting execution and providing temporal protection), and
inter-process communication
In computer science, inter-process communication or interprocess communication (IPC) refers specifically to the mechanisms an operating system provides to allow the processes to manage shared data. Typically, applications can use IPC, categori ...
(for controlled communication across isolation boundaries).
An operating system based on a microkernel like L4 provides services as servers in
user space
A modern computer operating system usually segregates virtual memory into user space and kernel space. Primarily, this separation serves to provide memory protection and hardware protection from malicious or errant software behaviour.
Kernel ...
that
monolithic kernel
A monolithic kernel is an operating system architecture where the entire operating system is working in kernel space. The monolithic model differs from other operating system architectures (such as the microkernel architecture) in that it alone ...
s like
Linux
Linux ( or ) is a family of open-source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically packaged as a Linux distribution, which ...
or older generation microkernels include internally. For example, to implement a secure
Unix-like
A Unix-like (sometimes referred to as UN*X or *nix) operating system is one that behaves in a manner similar to a Unix system, although not necessarily conforming to or being certified to any version of the Single UNIX Specification. A Unix-li ...
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
Working set is a concept in computer science which defines the amount of memory that a process requires in a given time interval.
Definition
Peter Denning (1968) defines "the working set of information W(t, \tau) of a process at time t to be the ...
is too large: the IPC code expresses poor spatial locality; that is, it results in too many
cache
Cache, caching, or caché may refer to:
Places United States
* Cache, Idaho, an unincorporated community
* Cache, Illinois, an unincorporated community
* Cache, Oklahoma, a city in Comanche County
* Cache, Utah, Cache County, Utah
* Cache County ...
misses, of which most are in-kernel.
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
Jochen Liedtke (26 May 1953 – 10 June 2001) was a German computer scientist, noted for his work on microkernel operating systems, especially in creating the L4 microkernel family.
Vita
Education
In the mid-1970s Liedtke studied for a di ...
set out to prove that a well designed thinner
inter-process communication
In computer science, inter-process communication or interprocess communication (IPC) refers specifically to the mechanisms an operating system provides to allow the processes to manage shared data. Typically, applications can use IPC, categori ...
(IPC) layer, with careful attention to performance and machine-specific (in contrast to
cross-platform software
In computing, cross-platform software (also called multi-platform software, platform-agnostic software, or platform-independent software) is computer software that is designed to work in several computing platforms. Some cross-platform software r ...
) 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
A modern computer operating system usually segregates virtual memory into user space and kernel space. Primarily, this separation serves to provide memory protection and hardware protection from malicious or errant software behaviour.
Kernel ...
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
An operating system (OS) is system software that manages computer hardware, software resources, and provides common services for computer programs.
Time-sharing operating systems schedule tasks for efficient use of the system and may also in ...
, used for many years for example by
Technischer Überwachungsverein
TÜVs (; short for german: Technischer Überwachungsverein, en, Technical Inspection Association) are internationally active, independent service companies from Germany and Austria that test, inspect and certify technical systems, facilities an ...
(Technical Inspection Association).
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 extract every bit of performance, the whole kernel was written in
assembly language
In computer programming, assembly language (or assembler language, or symbolic machine code), often referred to simply as Assembly and commonly abbreviated as ASM or asm, is any low-level programming language with a very strong correspondence be ...
, and its IPC was 20 times faster than Mach's.
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
The Thomas J. Watson Research Center is the headquarters for IBM Research. The center comprises three sites, with its main laboratory in Yorktown Heights, New York, U.S., 38 miles (61 km) north of New York City, Albany, New York and wit ...
Liedtke and his colleagues continued research on L4 and microkernel based systems in general, especially the Sawmill OS.
L4Ka::Hazelnut
In 1999, Liedtke took over the Systems Architecture Group at the
University of Karlsruhe
The Karlsruhe Institute of Technology (KIT; german: Karlsruher Institut für Technologie) is a public research university in Karlsruhe, Germany. The institute is a national research center of the Helmholtz Association.
KIT was created in 2009 w ...
, 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++
C++ (pronounced "C plus plus") is a high-level general-purpose programming language created by Danish computer scientist Bjarne Stroustrup as an extension of the C programming language, or "C with Classes". The language has expanded significan ...
version of the kernel that ran on
IA-32
IA-32 (short for "Intel Architecture, 32-bit", commonly called i386) is the 32-bit version of the x86 instruction set architecture, designed by Intel and first implemented in the 80386 microprocessor in 1985. IA-32 is the first incarnation of ...
- and
ARM
In human anatomy, the arm refers to the upper limb in common usage, although academically the term specifically means the upper arm between the glenohumeral joint (shoulder joint) and the elbow joint. The distal part of the upper limb between th ...
-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
In computing, interrupt latency refers to the delay between the start of an Interrupt Request (IRQ) and the start of the respective Interrupt Service Routine (ISR). For many operating systems, devices are serviced as soon as the device's interrup ...
. This was considered necessary because L4/Fiasco is used as the basis of DROPS, a hard
real-time computing
Real-time computing (RTC) is the computer science term for hardware and software systems subject to a "real-time constraint", for example from event to system response. Real-time programs must guarantee response within specified time constrai ...
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
An application programming interface (API) is a way for two or more computer programs to communicate with each other. It is a type of software interface, offering a service to other pieces of software. A document or standard that describes how ...
) 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.
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 In computing, an alien thread in a multi-processor
Multiprocessing is the use of two or more central processing units (CPUs) within a single computer system. The term also refers to the ability of a system to support more than one processor or th ...
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 ) (named
L4Linux).
University of New South Wales and NICTA
Development also occurred at the
University of New South Wales
The University of New South Wales (UNSW), also known as UNSW Sydney, is a public research university based in Sydney, New South Wales, Australia. It is one of the founding members of Group of Eight, a coalition of Australian research-intensive ...
(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
Itanium ( ) is a discontinued family of 64-bit Intel microprocessors that implement the Intel Itanium architecture (formerly called IA-64). Launched in June 2001, Intel marketed the processors for enterprise servers and high-performance computin ...
architecture).
The group has also demonstrated that
device driver
In computing, a device driver is a computer program that operates or controls a particular type of device that is attached to a computer or automaton. A driver provides a software interface to hardware devices, enabling operating systems and ot ...
s can perform equally well at user-level as in-kernel,
and developed
Wombat
Wombats are short-legged, muscular quadrupedal marsupials that are native to Australia. They are about in length with small, stubby tails and weigh between . All three of the extant species are members of the family Vombatidae. They are adap ...
, a highly portable version of
Linux
Linux ( or ) is a family of open-source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically packaged as a Linux distribution, which ...
on L4 that runs on
x86
x86 (also known as 80x86 or the 8086 family) is a family of complex instruction set computer (CISC) instruction set architectures initially developed by Intel based on the Intel 8086 microprocessor and its 8088 variant. The 8086 was introd ...
,
ARM
In human anatomy, the arm refers to the upper limb in common usage, although academically the term specifically means the upper arm between the glenohumeral joint (shoulder joint) and the elbow joint. The distal part of the upper limb between th ...
, and
MIPS processors. On
XScale
XScale is a microarchitecture for central processing units initially designed by Intel implementing the ARM architecture (version 5) instruction set. XScale comprises several distinct families: IXP, IXC, IOP, PXA and CE (see more below), with some ...
processors, Wombat context-switching costs are up to 50 times lower than in native Linux.
Later the UNSW group, at their new home at
NICTA
NICTA (formerly named National ICT Australia Ltd) was Australia's Information and Communications Technology (ICT) Research Centre of Excellence and is now known as CSIRO's Data61. The term "Centre of Excellence" is common marketing terminology u ...
(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 system
An embedded system is a computer system—a combination of a computer processor, computer memory, and input/output peripheral devices—that has a dedicated function within a larger mechanical or electronic system. It is ''embedded'' as ...
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 to ensure high real-time responsiveness.
Commercial deployment
In November 2005,
NICTA
NICTA (formerly named National ICT Australia Ltd) was Australia's Information and Communications Technology (ICT) Research Centre of Excellence and is now known as CSIRO's Data61. The term "Centre of Excellence" is common marketing terminology u ...
announced that
Qualcomm
Qualcomm () is an American multinational corporation headquartered in San Diego, California, and incorporated in Delaware. It creates semiconductors, software, and services related to wireless technology. It owns patents critical to the 5G, 4 ...
was deploying NICTA's L4 version on their ''
Mobile Station Modem
Snapdragon is a suite of system on a chip (SoC) semiconductor products for mobile devices designed and marketed by Qualcomm Technologies Inc. The Snapdragon's central processing unit (CPU) uses the ARM architecture. A single SoC may include mu ...
'' chipsets. This led to the use of L4 in
mobile phone
A mobile phone, cellular phone, cell phone, cellphone, handphone, hand phone or pocket phone, sometimes shortened to simply mobile, cell, or just phone, is a portable telephone that can make and receive calls over a radio frequency link whil ...
handsets on sale from late 2006. In August 2006, ERTOS leader and UNSW professor
Gernot Heiser
Gernot Heiser (born 1957) is a Scientia Professor and the John Lions
John Lions (19 January 1937 – 5 December 1998) was an Australian computer scientist. He is best known as the author of ''Lions' Commentary on UNIX 6th Edition, with ...
spun out a company named
Open Kernel Labs
Open Kernel Labs (OK 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 headq ...
(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
Capability-based security is a concept in the design of secure computing systems, one of the existing security models. A capability (known in some systems as a key) is a communicable, unforgeable token of authority. It refers to a value that refer ...
. 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 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,
mostly on Qualcomm wireless modem chips. Other deployments include
automotive infotainment
In-car entertainment (ICE), or in-vehicle infotainment (IVI), is a collection of hardware and software in automobiles that provides audio or video entertainment. In car entertainment originated with car audio systems that consisted of radios and c ...
systems.
Apple A series
Apple silicon is a series of system on a chip (SoC) and system in a package (SiP) processors designed by Apple Inc., mainly using the ARM architecture. It is the basis of most new Mac computers as well as iPhone, iPad, iPod Touch, Apple T ...
processors beginning with the
A7 contain a Secure Enclave
coprocessor
A coprocessor is a computer processor used to supplement the functions of the primary processor (the CPU). Operations performed by the coprocessor may be floating-point arithmetic, graphics, signal processing, string processing, cryptography o ...
running an L4 operating system
based on the L4-embedded kernel developed at
NICTA
NICTA (formerly named National ICT Australia Ltd) was Australia's Information and Communications Technology (ICT) Research Centre of Excellence and is now known as CSIRO's Data61. The term "Centre of Excellence" is common marketing terminology u ...
in 2006.
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.
High assurance: seL4
In 2006, the
NICTA
NICTA (formerly named National ICT Australia Ltd) was Australia's Information and Communications Technology (ICT) Research Centre of Excellence and is now known as CSIRO's Data61. The term "Centre of Excellence" is common marketing terminology u ...
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
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
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
In computing, executable code, an executable file, or an executable program, sometimes simply referred to as an executable or binary, causes a computer "to perform indicated tasks according to encoded instructions", as opposed to a data file ...
written in
Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...
.
seL4 uses
capability-based security
Capability-based security is a concept in the design of secure computing systems, one of the existing security models. A capability (known in some systems as a key) is a communicable, unforgeable token of authority. It refers to a value that refer ...
access control to enable formal reasoning about object accessibility.
A
formal proof
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the seque ...
of functional correctness was completed in 2009.
[
]
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
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a lo ...
s,
livelock
In concurrent computing, deadlock is any situation in which no member of some group of entities can proceed because each waits for another member, including itself, to take action, such as sending a message or, more commonly, releasing a loc ...
s,
buffer overflow
In information security and programming, a buffer overflow, or buffer overrun, is an anomaly whereby a program, while writing data to a buffer, overruns the buffer's boundary and overwrites adjacent memory locations.
Buffers are areas of memory ...
s, arithmetic exceptions or use of
uninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.
seL4 takes a novel approach to kernel resource management,
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.
The NICTA team also proved correctness of the translation from the programming language
C to executable
machine code
In computer programming, machine code is any low-level programming language, consisting of machine language instructions, which are used to control a computer's central processing unit (CPU). Each instruction causes the CPU to perform a very ...
, taking the
compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...
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 The worst-case execution time (WCET) of a computational task is the maximum length of time the task could take to execute on a specific hardware platform.
What it is used for
Worst case execution time is typically used in reliable real-time sys ...
(WCET) analysis, a prerequisite for its use in hard
real-time computing
Real-time computing (RTC) is the computer science term for hardware and software systems subject to a "real-time constraint", for example from event to system response. Real-time programs must guarantee response within specified time constrai ...
.
On 29 July 2014,
NICTA
NICTA (formerly named National ICT Australia Ltd) was Australia's Information and Communications Technology (ICT) Research Centre of Excellence and is now known as CSIRO's Data61. The term "Centre of Excellence" is common marketing terminology u ...
and
General Dynamics C4 Systems
General Dynamics Mission Systems is a business unit of American defense and aerospace company General Dynamics. General Dynamics Mission Systems integrates secure communication and information systems and technology. General Dynamics Mission Syst ...
announced that seL4, with end to end proofs, was now released under
open-source license
An open-source license is a type of license for computer software and other products that allows the source code, blueprint or design to be used, modified and/or shared under defined terms and conditions. This allows end users and commercial compa ...
s.
The kernel
source code
In computing, source code, or simply code, is any collection of code, with or without comments, written using a human-readable programming language, usually as plain text. The source code of a program is specially designed to facilitate the wo ...
and proofs are
licensed
A license (or licence) is an official permission or permit to do, use, or own something (as well as the document of that permission or permit).
A license is granted by a party (licensor) to another party (licensee) as an element of an agreeme ...
under
GNU General Public License version 2
The GNU General Public License (GNU GPL or simply GPL) is a series of widely used free software licenses that guarantee end users the Four Freedoms (Free software), four freedoms to run, study, share, and modify the software. The license was th ...
(GPLv2), and most
libraries
A library is a collection of materials, books or media that are accessible for use and not just for display purposes. A library provides physical (hard copies) or digital access (soft copies) materials, and may be a physical location or a vir ...
and
tools
A tool is an object that can extend an individual's ability to modify features of the surrounding environment or help them accomplish a particular task. Although many animals use simple tools, only human beings, whose use of stone tools dates ba ...
are under the
BSD 2-clause
BSD licenses are a family of permissive free software licenses, imposing minimal restrictions on the use and distribution of covered software. This is in contrast to copyleft licenses, which have share-alike requirements. The original BSD li ...
. In April 2020, it was announced that the seL4 Foundation was created under the umbrella of the
Linux Foundation
The Linux Foundation (LF) is a non-profit technology consortium founded in 2000 as a merger between Open Source Development Labs and the Free Standards Group to standardize Linux, support its growth, and promote its commercial adoption. Additi ...
to accelerate development and deployment of seL4.
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. Specifically, the cost of one
line of code
Source lines of code (SLOC), also known as lines of code (LOC), is a software metric used to measure the size of a computer program by counting the number of lines in the text of the program's source code. SLOC is typically used to predict the a ...
during the development of seL4 was estimated at around , compared to for traditional high-assurance systems.
Under the Defense Advanced Research Projects Agency (
DARPA
The Defense Advanced Research Projects Agency (DARPA) is a research and development agency of the United States Department of Defense responsible for the development of emerging technologies for use by the military.
Originally known as the Adv ...
) High-Assurance Cyber Military Systems (HACMS) program, NICTA together with project partners
Rockwell Collins
Rockwell Collins was a multinational corporation headquartered in Cedar Rapids, Iowa, providing avionics and information technology systems and services to government agencies and aircraft manufacturers. It was formed when the Collins Radio Comp ...
, Galois Inc, the
University of Minnesota
The University of Minnesota, formally the University of Minnesota, Twin Cities, (UMN Twin Cities, the U of M, or Minnesota) is a public university, public Land-grant university, land-grant research university in the Minneapolis–Saint Paul, Tw ...
and
Boeing
The Boeing Company () is an American multinational corporation that designs, manufactures, and sells airplanes, rotorcraft, rockets, satellites, telecommunications equipment, and missiles worldwide. The company also provides leasing and product ...
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
The Boeing AH-6 is a series of light helicopter gunships based on the MH-6 Little Bird and MD 500 family. Developed by Boeing Rotorcraft Systems, these include the Unmanned Little Bird (ULB) demonstrator, the A/MH-6X Mission Enhanced Little Bir ...
Unmanned Little Bird helicopter being developed by Boeing. Final demonstration of the HACMS technology took place in Sterling, VA in April 2017.
DARPA also funded several
Small Business Innovative Research
The Small Business Innovation Research (or SBIR) program is a U.S. government funding program, coordinated by the Small Business Administration, intended to help certain small businesses conduct research and development (R&D). Funding takes the f ...
(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.
[
]
Other research and development
Osker, an OS written in
Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...
, targeted the L4 specification; although this project focused mainly on the use of a
functional programming
In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declar ...
language for OS development, not on microkernel research.
CodeZero is an L4 microkernel for embedded systems with a focus on virtualization and implementation of native OS services. There is a
GPL
The GNU General Public License (GNU GPL or simply GPL) is a series of widely used free software licenses that guarantee end users the four freedoms to run, study, share, and modify the software. The license was the first copyleft for general u ...
-licensed version, and a version that was relicensed by B Labs Ltd., acquired by
Nvidia
Nvidia CorporationOfficially written as NVIDIA and stylized in its logo as VIDIA with the lowercase "n" the same height as the uppercase "VIDIA"; formerly stylized as VIDIA with a large italicized lowercase "n" on products from the mid 1990s to ...
, as closed source and forked in 2010.
F9 microkernel, a BSD-licensed L4 implementation, is dedicated to
ARM Cortex-M
The ARM Cortex-M is a group of 32-bit RISC ARM processor cores licensed by Arm Holdings. These cores are optimized for low-cost and energy-efficient integrated circuits, which have been embedded in tens of billions of consumer devices. Thou ...
processors for deeply embedded devices with memory protection.
The NOVA OS Virtualization Architecture is a research project with focus on constructing a secure and efficient virtualization environment
with a small trusted computing base. NOVA consists of a microhypervisor, a user level
hypervisor
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 calle ...
(
virtual machine
In computing, a virtual machine (VM) is the virtualization/emulation of a computer system. Virtual machines are based on computer architectures and provide functionality of a physical computer. Their implementations may involve specialized hardw ...
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 is a
real-time operating system
A real-time operating system (RTOS) is an operating system (OS) for real-time applications that processes data and events that have critically defined time constraints. An RTOS is distinct from a time-sharing operating system, such as Unix, which m ...
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
) working on WrmOS.
See also
*
PikeOS
PikeOS is a commercial, hard real-time operating system (RTOS) that offers a separation kernel based hypervisor with multiple logical partition types for many other operating systems (OS), each called a GuestOS, and applications. It enables user ...
References
Further reading
*
* (on L4 kernel and compiler)
*
* Evolution of L4 design and implementation approaches
External links
*
* , seL4
The L4 microkernel family overview of L4 implementations, documentation, projects
Official TUD:OS WikiL4Ka Implementations L4Ka::Pistachio and L4Ka::Hazelnut
UNSW Implementations for
DEC Alpha
Alpha (original name Alpha AXP) is a 64-bit reduced instruction set computer (RISC) instruction set architecture (ISA) developed by Digital Equipment Corporation (DEC). Alpha was designed to replace 32-bit VAX complex instruction set computers ...
and
MIPS architecture
MIPS (Microprocessor without Interlocked Pipelined Stages) is a family of reduced instruction set computer (RISC) instruction set architectures (ISA)Price, Charles (September 1995). ''MIPS IV Instruction Set'' (Revision 3.2), MIPS Technologies, ...
* : Commercial L4 version from
*
Trustworthy Systems Group at CSIRO's Data61 Present home of the former NICTA group that developed seL4
Genode Operating System Framework An offspring of the L4 community
{{Object-capability security
Capability systems
Microkernels
Assembly language software