Mixed low- and high level programming language semantics and automated verification of a small hypervisor

Abstract

Hypervisors are system software programs that virtualize the architecture they run on and are usually implemented in a mix of (macro) assembly and a high-level language like C. To verify such a software, assembly parts as well as C parts should be verified, where reasoning about those parts is done in different semantics. At the end, both semantics should be brought together in an overall correctness theorem of such a software program. The formal integration of correctness results accomplished in distinct semantics is challenging but inevitable for systems verification.

This thesis is split into two parts. In the first one, we will present the mixed semantics of C and macro assembly. This semantics can handle mixed-language implementations where the execution context is changed by an external function call from assembly to C and vice versa. Also, we state a step-by-step simulation theorem between mixed programs and the compiled and assembled code. In the second part, we present the correctness of a small hypervisor, called Baby Hypervisor (BHV), described by the mixed semantics. BHV virtualizes a 32-bit RISC architecture. The BHV functional verification was shown using Microsoft's VCC, an automatic verifier for C with contracts. For making macro assembly feasible with VCC the original macro assembly is translated to C code simulating processor. This is called the simulation approach.

Hypervisor sind Software-Systemprogramme, die eine Hardwarearchitektur virtualisieren, eine Umgebung für die virtuelle Maschinen schaffen und gemischte Implementierungen in C- und Makroassemblerprogrammiersprachen haben. Um solche Programme zu verifizieren, müssen Assembler- sowie C-Portionen des Quellcodes verifiziert werden, wobei die Verifikation beider Teile in den verschiedenen Semantiken erfolgt. Schließlich sollten beide Semantiken zusammen in einen umfassenden Korrektheitssatz gebracht werden. Die Aufgabe der formalen Integration der Korrektheitsergebnisse aus verschiedenen semantischen Ebenen ist anspruchsvoll aber unvermeidlich für die Systemverifikation.

Diese Arbeit ist in zwei Teile aufgeteilt. Im ersten Teil stellen wir die gemischte Semantik von C- und Makroassemblerprogrammiersprache vor. Diese Semantik kann die gemischte Implementierung beschreiben, in der der Ausführungskontext von einem externen Funktionsaufruf von Assembler nach C und umgekehrt wechselt. Außerdem formulieren wir einen Schritt-für-Schritt-Simulationssatz zwischen den gemischten Programmen und dem übersetzten Quellcode. Im zweiten Teil präsentieren wir die Korrekheit eines kleinen Hypervisors, genannt Baby Hypervisor (BHV), der in der gemischten Semantik beschrieben wird. BHV virtualisiert eine 32-Bit RISC-Architektur. Die funktionale Verifikation des BHVs wurde mit Hilfe des Microsoft-VCCs, eines automatischen C-Beweisers, durchgeführt. Um eine Verifikation des Makroassembler-Quellcodes mit Hilfe des VCC zu ermöglichen, wird der Quellcode in C-Quellcode, der den Prozessor simuliert, übersetzt. Dies wird simulation approach genannt.