SciDok

Eingang zum Volltext in SciDok

Lizenz

Dissertation zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-49649
URL: http://scidok.sulb.uni-saarland.de/volltexte/2012/4964/


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

Gemischte Semantik von niederen und höheren Programmiersprachen und automatische Verifikation eines einfachen Hypervisors

Shadrin, Andrey

pdf-Format:
Dokument 1.pdf (1.863 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Richtigkeit von Ergebnissen , Virtualisierung , Compiler , Programmiersprache , Semantik , Verifikation
Freie Schlagwörter (Deutsch): Macro Assembler , Gemischte Semantik , Optimierende Compiler , Hypervisor , Automatische Verifikation
Freie Schlagwörter (Englisch): macro assembler , mixed semantics , optimizing compiler , hypervisor , automated verification
Institut: Fachrichtung 6.2 - Informatik
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Hauptberichter: Paul, Wolfgang J. (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 27.08.2012
Erstellungsjahr: 2012
Publikationsdatum: 26.09.2012
Kurzfassung auf Englisch: 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.
Kurzfassung auf Deutsch: 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.
Lizenz: Veröffentlichungsvertrag für Dissertationen und Habilitationen

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English