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)
“One of the most important findings to come out of our research is that being where you want to be is good for you. We found a very strong correlation between preferring the role you are in and well-being. The homemaker who is at home because she likes that “job,” because it meets her own desires and needs, tends to feel good about her life. The woman at work who wants to be there also rates high in well-being.”
—Grace Baruch (20th century)
“The man, or the boy, in his development is psychologically deterred from incorporating serving characteristics by an easily observable fact: there are already people around who are clearly meant to serve and they are girls and women. To perform the activities these people are doing is to risk being, and being thought of, and thinking of oneself, as a woman. This has been made a terrifying prospect and has been made to constitute a major threat to masculine identity.”
—Jean Baker Miller (20th century)