Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-82962
URL: http://www.freidok.uni-freiburg.de/volltexte/8296/


Maus, Stefan

Verification of hypervisor subroutines written in Assembler

Verifikation von Hypervisorunterrutinen, geschrieben in Assembler

Dokument1.pdf (739 KB) (md5sum: 6b84e2c5dd80189007a4a20722a4cb7c)

Kurzfassung in Englisch

We present a methodology for the specification and verification of functional specifications of programs written in Assembler. We have evaluated the methodology in an industrial setting, the verification of the Microsoft Hypervisor.

Many industrial software projects are written in a high-level language like C. For performance reasons or for direct hardware access, some of the routines are implemented in Assembler. Our goal is the automatic modular verification of functional specifications for C programs with subroutines in Assembler. This goal entails the need for checking an Assembler procedure against its functional specification. The specification of the Assembler program is used also in the specification of the C code that calls the Assembler program as a subroutine. Therefore, we need to translate back and forth between specifications for C code and specifications for Assembler code.

The particular context of our work is the verification of the Microsoft Hypervisor where the static checker VCC is used to verify the part of the code written in C. VCC uses modular reasoning and comes with its own annotation language for functional specifications for C programs. The functional specifications for the Assembler routines in the Microsoft Hypervisor are given in the form of specifications for the C routines that call them.

In this thesis, we introduce the tool Vx86 and the corresponding methodology to verify Assembler code against functional specifications of the form described above. In our approach, we use Vx86 to translate the Assembler code into C code. We give the translation of each Assembler instruction into a short piece of C code. Some instructions of x86 are complex in that their behavior depends on the internal processor state such as flag or control registers. The high-level semantics of C does not, however, foresee such low-level featuers. In order to account for the processor state in the high-level semantics, we introduce a C structure that contains the complete processor state. The modification of this C structure during the execution of the C code simulates the modification of the internal processor state during the execution of the Assembler instructions. Since we can refer to this C structure in the annotation language, we can specify the functional correctness of Assembler routines also if the functional correctness refers to the hardware directly.

Our tool Vx86, integrated with VCC, leads to a methodology for the verification of functional specifications of programs written in Assembler and, thus, the pervasive verification of mixed programs such as the Microsoft Hypervisor which are written in C and Assembler. In this methodology, the program has to be annotated manually with modular specifications, e.g., pre- and postconditions and loop invariants. The verification of the code against these specifications is then fully automatic. We have used the methodology and the tool Vx86 in order to verify all subroutines of the Microsoft Hypervisor which are written in Assembler.


Kurzfassung in Deutsch

Wir stellen eine neue Methode zur Spezifikation und Verifikation von funktionalen Spezifikationen von Assembler-Programmen vor. Wir haben diese Methode in einem industriellen Kontext evaluiert, nämlich der Verifikation des Microsoft Hypervisor.

Viele industrielle Softwareprojekte sind in Hochsprachen wie C geschrieben. Aus Geschwindigkeitsgründen oder für direkten Hardwarezugriff werden einige Routinen in Assembler implementiert. Unser Ziel ist eine automatische, modulare Verifikation funktionaler Spezifikationen für C-Programme mit Unterroutinen in Assembler. Dies erfordert das Überprüfen einer Assembler-Prozedur gegen ihre funktionale Spezifikation. Die Spezifikation der Assembler-Prozedur wird auch benutzt für die Spezifikation des C-Codes, der die Assembler-Prozedur als Unterroutine aufruft. Dazu müssen C-Code Spezifikationen und Assembler-Code Spezifikationen in beiden Richtungen ineinander übersetzt werden.

Der besondere Kontext unserer Arbeit ist die Verifikation des Microsoft Hypervisor, wobei der Static Checker VCC für die Verifikation der Code Teile benutzt wird, die in C geschrieben sind. VCC ermöglicht modulare Beweise und führt eine eigene Annotationssprache für die funktionale Spezifikation von C-Programmen ein. Die funktionale Spezifikation von Assembler-Routinen im Microsoft Hypervisor werden in Form von Spezifikationen für deren Aufrufe im C-Programm bereit gestellt.

In dieser Arbeit führen wir das Werkzeug Vx86 und eine darauf beruhende Methode ein, um Assembler-Code gegen funktionale Spezifikationen der oben beschrieben Form zu verifizieren. In unserer Methode benutzen wir Vx86 um Assembler-Code in C-Code zu übersetzen. Wir präsentieren die Übersetzung jeder einzelnen Assembler-Instruktion in ein kurzes C-Code Fragment. Einige Instruktionen des x86 sind komplex in dem Sinne, dass ihr Verhalten von dem internen Prozessorzustand abhängt, wie den Flag- oder Kontrollregistern.
Die Hochsprachen-Semantik von C sieht allerdings keine solchen systemnahen Features vor. Um in der Hochsprachen-Semantik auf den Prozessorzustand Bezug nehmen zu können, führen wir eine C-Struktur ein, die den kompletten Prozessorzustand abbildet. Die Veränderungen an dieser C-Struktur während der Ausführung des C-Codes simuliert die Veränderungen des internen Prozessorzustandes bei der Ausführung der Assembler-Befehle. Da wir in der Annota- tionssprache Bezug auf diese C-Struktur nehmen können, können wir auch die funktionale Korrektheit von Assembler-Routinen spezifizieren, wenn sich die funktionale Korrektheit direkt auf die Hardware bezieht.

Unser Werkzeug Vx86 führt, zusammen mit VCC, zu einer Methode der Verifikation von funktionalen Spezifikationen von Prozeduren, die in Assembler geschrieben sind, und führt damit zur durchgängigen Verifikation von gemischten Programmen wie dem Microsoft Hypervisor, die in C und Assembler geschrieben sind. Für diese Methode muss das Programm manuell mit modularen Spezifikationen annotiert werden, z.B. mit Vor- und Nachbedingungen oder Schleifeninvarianten. Die Verifikation des Codes gegen diese Spezifikationen erfolgt dann vollautomatisch. Wir haben die Methode und das Werkzeug Vx86 benutzt, um alle Unterroutinen des Microsoft Hypervisor, die in Assembler geschrieben sind, zu verifizieren.


SWD-Schlagwörter: Assembler
Freie Schlagwörter (englisch): Hypervisor , Verification
CCS Klassifikation D.2.1 Requ
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Podelski, Andreas (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 29.08.2011
Erstellungsjahr: 2011
Publikationsdatum: 28.09.2011
Indexliste