Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
In this thesis we address the challenges of hypervisor verification for multicore processors. As a first contribution we unite different pieces of hypervisor verification theory into a single theory comprising the stack of highly nontrivial computational models used. We consider multicore hypervisors for x8664 architecture written in C. To make code verification in a C verifier possible, we define a reduced hardware model and show that under certain safety conditions it simulates the full model. We introduce an extension of the C semantics, which takes into consideration possible MMU and guest interaction with the memory of a program. We argue that the extended C semantics simulates the hardware machine, which executes compiled hypervisor code, given that the compiler is correct. The second contribution of the thesis is the formal verification of a software TLB and memory virtualization approach, called SPT algorithm. Efficient TLB virtualization is one of the trickiest parts of building correct hypervisors. An SPT algorithm maintains dedicated sets of ‘‘shadow’’ page tables, ensuring memory separation and correct TLB abstraction for every guest. We use our extended C semantics to specify correctness criteria for TLB virtualization and to verify a simple SPT algorithm written in C. The code of the algorithm is formally verified in Microsoft’s VCC automatic verifier, which is ideally suited for proofs performed on top of our semantic stack. ; Die vorliegende Arbeit beschäftigt sich eingehend mit der Verifikation von Hypervisorn und den Herausforderungen, die dabei auftreten. Als ein Hauptergebnis werden erstmalig die verschiedenen Teile der HypervisorVerifikationstheorie zu einer einheitlichen Theorie zusammengefasst, in der mehrere komplexen Rechenmodelle auf einander aufbauen. Als Zielplattform für die Virtualisierung wählten wir eine x86-64 Architektur und betrachten Hypervisoren für Multicore-Prozessoren, die in C implementiert sind. Um Code-Verifikation in einem C-Verifizierer zu ermöglichen, definieren wir ...