Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-5938
Main Title: Design and provability of a statically configurable hypervisor
Translated Title: Design und Beweisbarkeit eines statisch konfigurierbaren Hypervisors
Author(s): Nordholz, Jan
Advisor(s): Seifert, Jean-Pierre
Referee(s): Jähnichen, Stefan
Massacci, Fabio
Granting Institution: Technische Universität Berlin
Type: Doctoral Thesis
Language Code: en
Abstract: In this thesis we develop a novel, minimalist design for Type I hypervisors and present a fully working prototype for the ARMv7 and ARMv8 architectures. We introduce its key design paradigm, the Principle of Staticity, elaborate on its consequences for the resulting implementation, and discuss scenarios where not all dynamicity can be eliminated. We also describe, implement, and evaluate the configuration framework necessary to build this specific kind of hypervisor. Even though the compiled hypervisor images are fully static, we show that the framework is powerful enough to support various system-on-chip target platforms, different address translation regimes, and even completely unrelated architectures. We further demonstrate its versatility by extending the framework to even support embedded processors which only contain a memory protection unit. After performing a selection of benchmarks to substantiate the competitiveness of our implementation, we continue by subjecting our hypervisor to an analysis using a specialized form of symbolic model checking. We succeed in deriving integrity properties for the hypervisor as well as among virtual machines with surprisingly little effort, but show that complexity immediately ramps up once dynamic components like a shadow paging unit are added to our design. Finally we demonstrate the extensibility of our design despite our postulated Principle of Staticity. As an optimization example, we introduce the concept of "lightweight VMs" and present a novel use case for a recent feature of the ARM architecture, thereby reducing the switch latency between virtual machines. We conclude with an overview over the published research efforts based on or heavily inspired by our hypervisor and discuss future research questions.
Wir entwickeln in dieser Arbeit ein neuartiges, minimalistisches Design für Type-I-Hypervisors und stellen einen voll funktionsfähigen Prototypen für die ARMv7- und ARMv8-Architektur vor. Wir führen das zugrundeliegende Design-Konzept, das "Prinzip der Statizität", ein, erläutern dessen Konsequenzen für die daraus hervorgehende Implementierung und diskutieren Szenarien, in denen Dynamik nicht vollständig eliminiert werden kann. Daneben beschreiben, implementieren und evaluieren wir auch die zur Erstellung eines solchen Hypervisors notwendige Konfigurationsumgebung. Obwohl die kompilierten Hypervisor-Images völlig statisch sind, zeigen wir, daß die Werkzeuge mächtig genug sind, um Unterstützung für diverse System-on-Chip-Plattformen, unterschiedliche Formen der Adreßübersetzung und sogar völlig unterschiedliche Prozessorarchitekturen zu bieten. Wir zeigen, daß es durch eine Erweiterung sogar möglich ist, sogar Prozessoren zu unterstützen, die nur eine Memory Protection Unit beinhalten. Nach der Durchführung einer Auswahl von Benchmarks, um die Wettbewerbsfähigkeit unserer Implementierung zu untermauern, setzen wir mit der Analyse unseres Hypervisors mit einer speziellen Form der symbolischen Ausführung fort. Wir leiten erfolgreich und mit erstaunlich geringem Aufwand Integritätseigenschaften sowohl für den Hypervisor selbst als auch für die virtuellen Maschinen untereinander ab, zeigen jedoch, daß die Komplexität des Verfahrens sofort stark ansteigt, sobald dynamische Komponenten wie ein Shadow-Paging-Modul zu unserem Design hinzugefügt werden. Schließlich zeigen wir, daß unser Design trotz des Festhaltens am postulierten "Prinzip der Statizität" erweiterbar ist. Als Beispiel für eine Optimierung führen wir das Konzept von "Lightweight VMs" ein und präsentieren eine neuartige Verwendung eines jüngeren Merkmals der ARM-Architektur, wodurch wir die Umschaltzeiten zwischen virtuellen Maschinen reduzieren können. Wir schließen die Arbeit mit einem Überblick über die veröffentlichten Forschungsarbeiten ab, die auf unserem Hypervisor basieren oder stark davon beeinflußt wurden, und diskutieren weiterführende Forschungsprobleme.
URI: http://depositonce.tu-berlin.de/handle/11303/6388
http://dx.doi.org/10.14279/depositonce-5938
Exam Date: 2-Jun-2017
Issue Date: 2017
Date Available: 7-Jun-2017
DDC Class: DDC::000 Informatik, Informationswissenschaft, allgemeine Werke::000 Informatik, Wissen, Systeme::003 Systeme
Subject(s): hypervisor
virtualization
symbolic execution
formal methods
Hypervisor
Virtualisierung
symbolische Ausführung
formale Methoden
Creative Commons License: https://creativecommons.org/licenses/by-sa/4.0/
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
nordholz_jan.pdf1.69 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.