Towards the pervasive formal verification of multi-core operating systems and hypervisors implemented in C

Abstract

This thesis deals with a semantic model stack for verification of functional correctness of multi-core hypervisors or operating systems. In contrast to implementations based on single-core architectures, there are additional features and resulting challenges for verifying correctness properties in the multi-core case, e.g. weak memory models (store buffers), or an inter processor interrupt mechanism. The Verisoft XT project had the goal of verifying correctness of the Microsoft Hyper-V hypervisor and achieved great code verification results using the concurrent C verification tool VCC developed by our project partners during the project. A sound mathematical theory to support code verification was not established. To remedy this shortcoming, we sketch a model stack for a simplified multi-core architecture based on a simplified MIPS model for system programmers and illustrate on a high level of abstraction how to obtain a simulation between neighboring models. A hardware model for this architecture is formalized at a detailed level of abstraction of the model stack. In addition, this thesis provides operational semantics for a quite simple intermediate language for C as well as an extension of this semantics with specification (ghost) state and code which can serve as a basis for arguing the soundness of VCC. Due to the powerful nature of specification code, a simulation between annotated and original program is not trivial. Thus, we give a pencil and paper proof.

Die Arbeit befasst sich mit einem semantischen Modell-Stack für die Verifikation der Korrektheit von Multi-Core Hypervisoren oder Betriebssystemen. Im Gegensatz zu auf Implementierungen auf Single-Core Architekturen stellen sich im Multi-Core Fall zusätzliche Herausforderungen für die Verifikation von Korrektheitseigenschaften, z.B. durch schwache Speichermodelle, Speicherzugriffsmodi welche in begrenztem Rahmen kompatibel sind, Cache-Konsistenz-Protokolle welche (bei korrekter Benutzung der Speicherzugriffsmodi) ein einheitliches Bild des Speichers für alle Maschinen garantieren, oder die Nutzung eines Inter-Prozessor-Interrupt Mechanismus (sowohl zum Starten der Maschine nach Reset als auch zum Zweck der Kommunikation zwischen Programmcode der auf verschiedenen Prozessoren ausgeführt wird). Im Verisoft Projekt (gefördert durch bmbf, 2003-2007) wurde die Korrektheit eines Betriebssystemes welches auf einem sequentiellen VAMP Prozessor mit nebenläufigen Devices ausgeführt wird durchgängig formal verifiziert -- von Gatterebene der Hardwarekonstruktion bis hin zur korrekten Ausführung des Betriebssystemes auf eben dieser Hardware. Das Nachfolgerprojekt Verisoft XT (2007-2010), welches unter anderem zum Ziel hatte die Korrektheit des Microsoft Hyper-V Hypervisors zu verifizieren, erreichte unter Benutzung des Verifikationstools VCC (welches im VerisoftXT Projekt durch den Projektpartner Microsoft Research entwickelt wurde) hervorragende Resultate im Bereich der Codeverifikation. Die Erstellung einer durchgängigen mathematischen Theorie um diese Resultate zu untermauern wurde jedoch vernachlässigt. Um diesen Mangel zu beheben, skizzieren wir in der Dissertation einen Modell-Stack für eine Multi-Core Architektur basierend auf einem vereinfachten MIPS-Modell für Systemprogrammierer und illustrieren wie eine Simulation zwischen benachbarten Modellen erreicht wird. Teilweise ist die Erweiterung sequentieller Resultate auf die Multi-Core Architektur möglich indem man durch geeignete Software-Bedingungen (z.B. Zugriffsbeschränkungen für den gemeinsamen Speicher der Prozessoren gegeben durch ein Ownership-Modell) die Ausführungsreihenfolgen der nebenläufigen Maschine gerade soweit sequentialisiert dass eine Anwendung der alten Resultate möglich wird. In der Dissertation wird ein formales Hardwaremodell für die Multi-Core-MIPS-Architektur auf einer detaillierten Abstraktionsebene präsentiert. Zusätzlich enthält die Arbeit die operationale Semantik einer für die Hypervisor- und Betriebssystemverifikation geeignete Zwischensprache für C und deren Erweiterung um Spezifikationszustand und -code. Die um Spezifikationszustand und -code erweiterte Zwischensprache kann als Basis für einen Korrektheitsbeweis des Tools VCC dienen. Da aufgrund der mächtigen Spezifikationssprache von VCC (welche es z.B. erlaubt Spezifikationscode zu schreiben der nicht terminiert) eine Simulation zwischen annotiertem und originalem Programm nicht trivial ist, führen wir den Beweis auf Papier.