Current Research and Development
The NICTA group now focuses on the use of L4 as the basis for highly secure and reliable systems. At the core of this approach is a new L4 kernel, called seL4, aimed at satisfying security requirements such as those of Common Criteria. The seL4 API is represented by an executable specification written in Haskell.
seL4 is a third-generation microkernel which 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. It has been formally verified, which means that there is a (machine-checked) mathematical proof that the implementation is consistent with the specification. This provides a guarantee that the kernel 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.
The NICTA group is also developing frameworks for building componentised systems on top of L4.
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.
Codezero, a GPL L4 microkernel targeting embedded systems is also under development, with a focus on virtualization and implementation of native OS services.
The Operating Systems Group TUD:OS of TU Dresden develops third generation microkernel-based operating systems. The component based user-level environment L4Re and the microkernel Fiasco.OC as well as the NOVA microhypervisor, together with its user-level environment NUL are the results of this ongoing research.
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. 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 (IA32 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 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.
Read more about this topic: L4 Microkernel Family
Famous quotes containing the words current, research and/or development:
“Natural Man, in our current version, is a disgruntled adolescent.”
—Mason Cooley (b. 1927)
“Our science has become terrible, our research dangerous, our findings deadly. We physicists have to make peace with reality. Reality is not as strong as we are. We will ruin reality.”
—Friedrich Dürrenmatt (1921–1990)
“Information about child development enhances parents’ capacity to respond appropriately to their children. Informed parents are better equipped to problem-solve, more confident of their decisions, and more likely to respond sensitively to their children’s developmental needs.”
—L. P. Wandersman (20th century)