Design und Beweisbarkeit eines statisch konfigurierbaren Hypervisors

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