Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-26397
Titel: Mixed low- and high level programming language semantics and automated verification of a small hypervisor
Sonstige Titel: Gemischte Semantik von niederen und höheren Programmiersprachen und automatische Verifikation eines einfachen Hypervisors
Verfasser: Shadrin, Andrey
Sprache: Englisch
Erscheinungsjahr: 2012
SWD-Schlagwörter: Richtigkeit von Ergebnissen
Virtualisierung
Compiler
Programmiersprache
Semantik
Verifikation
Freie Schlagwörter: Macro Assembler
Gemischte Semantik
Optimierende Compiler
Hypervisor
Automatische Verifikation
macro assembler
mixed semantics
optimizing compiler
hypervisor
automated verification
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-49649
hdl:20.500.11880/26453
http://dx.doi.org/10.22028/D291-26397
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 27-Aug-2012
SciDok-Publikation: 26-Sep-2012
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Sh12.pdf1,86 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.