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:
“This is no argument against teaching manners to the young. On the contrary, it is a fine old tradition that ought to be resurrected from its current mothballs and put to work...In fact, children are much more comfortable when they know the guide rules for handling the social amenities. It’s no more fun for a child to be introduced to a strange adult and have no idea what to say or do than it is for a grownup to go to a formal dinner and have no idea what fork to use.”
—Leontine Young (20th century)
“... research is never completed ... Around the corner lurks another possibility of interview, another book to read, a courthouse to explore, a document to verify.”
—Catherine Drinker Bowen (1897–1973)
“I hope I may claim in the present work to have made it probable that the laws of arithmetic are analytic judgments and consequently a priori. Arithmetic thus becomes simply a development of logic, and every proposition of arithmetic a law of logic, albeit a derivative one. To apply arithmetic in the physical sciences is to bring logic to bear on observed facts; calculation becomes deduction.”
—Gottlob Frege (1848–1925)