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:
“Talent develops in quiet places, character in the full current of human life.”
—Johann Wolfgang Von Goethe (1749–1832)
“The great question that has never been answered and which I have not get been able to answer, despite my thirty years of research into the feminine soul, is “What does a women want?””
—Sigmund Freud (1856–1939)
“... work is only part of a man’s life; play, family, church, individual and group contacts, educational opportunities, the intelligent exercise of citizenship, all play a part in a well-rounded life. Workers are men and women with potentialities for mental and spiritual development as well as for physical health. We are paying the price today of having too long sidestepped all that this means to the mental, moral, and spiritual health of our nation.”
—Mary Barnett Gilson (1877–?)