TY  - THES
T1  - Mixed low- and high level programming language semantics and automated verification of a small hypervisor
A1  - Shadrin,Andrey
Y1  - 2012/09/26
N2  - 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.
KW  - Richtigkeit von Ergebnissen
KW  - Virtualisierung
KW  - Compiler
KW  - Programmiersprache
KW  - Semantik
KW  - Verifikation
CY  - Saarbrücken
PB  - Universitäts- und Landesbibliothek
AD  - Postfach 151141, 66041 Saarbrücken
UR  - http://scidok.sulb.uni-saarland.de/volltexte/2012/4964
ER  -