Hardware-Supported Virtualization for the L4 Microkernel

  • Subject:L4Ka
  • Type:Diploma Thesis
  • Date:29.09.2006
  • Supervisor:

    Prof. Dr. Frank Bellosa, Jan Stoess

  • Graduand:Sebastian Biemüller
  • Links:PDF
  • Abstract:

    Despite the immense popularity virtual machines regained in the last years current virtualization environments force significant compromises to the host system architecture. Hypervisor-based virtual machine environments are missing system construction principles; they only provide the coarse grained abstraction of a virtual machine, preventing small and efficient systems. Hosted virtual machine environments reuse the host's operating system services and thereby massively increase the trusted code base, preventing small, reliable and verifiable systems.

    We propose a novel approach for the construction of virtual machine environments: We divide the virtual machine environment into a necessarily privileged part, and a user-level monitor. The privileged part and microkernels share a common set of goals such as reliability, security, and isolation so that integrating virtual machines and microkernels is a promising approach. In fact, modern microkernels, such as the L4 microkernel, already provide the abstractions and mechanisms necessary to cater for virtual machines. We identify shortcomings of the current kernel with respect to virtual machine support and add a minimalistic set of extensions. As a normal microkernel application, the user-level monitor can interact with services provided by other components to maintain the virtual machine.

    To demonstrate our approach we implemented a prototype virtualization environment on top of the modified microkernel. We successfully run a guest operating system, utilizing all types of services side-by-side with other, native microkernel applications. Our design preserves the performance of the microkernel, especially the mechanism for inter-process communication needed no adaption. Measurements indicate only minimal side-effects caused by the increased hardware-overhead of the worldswitch needed for the virtual machine environments.


      author = {Sebastian Biemueller},
      title = {Hardware-Supported Virtualization for the L4 Microkernel},
      type = {Diploma Thesis},
      address = {System Architecture Group, University of Karlsruhe, Germany},
      month = sep # "~29",
      year = 2006,
      url = {http://i30www.ira.uka.de/teaching/theses/pasttheses/}