[Back]

R Lezuo:
"Scalable Translation Validation Tools, Techniques and Framework";
Supervisor, Reviewer: A. Krall, W. Zimmermann; Inst. für Computersprachen, 2014; oral examination: 2014-06-04.

Today embedded computer systems are often used in safety-critical applications. A malfunction
in such a system (e.g. X-by-wire) often has severe effects, even life-threatening consequences.
Lots of effort is put into certification to assure the correct and safe behavior of safety-critical applications.
Due to the high complexity of modern technical systems, a high-level programming
language like C is commonly used to implement their software.
This makes the compiler a critical component in the certification of safety-critical systems.
Even if the source code is fully certified and error-free an erroneous compiler could introduce
unintended behavior and hence the certification would be in vain. This is one motivation of
research in compiler correctness, a discipline which develops methods to show that the compiler
behaves correctly. One approach, namely translation validation, formally proves that a single,
specific run of the compiler was error-free.
This thesis contributes a framework which allows to apply translation validation from the
source code down to its binary representation. The CASMlanguage, based on the formal method
of Abstract State Machines (ASM), has been developed as part of this thesis to specify the semantics
of the source language and machine code. Using the novel technique of direct symbolic
execution a first-order logic representation is created as the foundation for the formal proofs. To
exploit the common structure found in problems originating from translation validation problems
a specialized prover called vanHelsing has been implemented as part of this thesis. Its
visual proof debugger enables non-domain experts to analyze failing proofs and pinpoint the
causing, erroneous translation.
The detailed evaluation shows that CASM is by far the best performing ASM implementation.
It is efficient enough to synthesize Instruction Set Simulation and Compiled Simulation
tools. The vanHelsing prover performs much better than other state of the art provers on
problems stemming from translation validation. These efficient tools and the high degree of
parallelism in our translation validation framework enable fast validations. The implemented
prototypes for instruction selection, register allocation and VLIW scheduling demonstrate that
validation of real-world applications like bzip2 is possible within a few dozen minutes.
vii

Viele der heute verwendeten eingebetteten Computersysteme übernehmen sicherheitskritische
(safety-critical) Aufgaben. Die Fehlfunktion eines sicherheitskritischen Systems führt per Definition
zu großen Schäden, unter ungünstigen Umständen auch zur Gefahr für Leib und Leben.
Teure Zertifizierungsverfahren werden durchlaufen um das korrekte und sichere Verhalten solcher
Systeme sicherzustellen. Aufgrund der allgemein hohen Komplexität moderner technischer
Systeme wird die Software, auch von sicherheitskritischen Anwendungen, oft in Hochsprachen
wie C implementiert.
Dadurch wird der Übersetzer (compiler) dieser Sprache zertifizierungsrelevant. Selbst wenn
der zugrunde liegende Quellcode der Software bewiesenermaßen fehlerfrei ist kann ein einziger
Übersetzungsfehler ein verändertes Verhalten in der Ausführung bewirken. Dieser würde
jedoch die komplette Zertifizierung obsolet machen, eine Motivationen für Forschung im Gebiet
der Übersetzerkorrektheit (compiler correctness), einer Disziplin welche Techniken und Methoden
erforscht um mit Hilfe formaler Verfahren die Korrektheit von Übersetzern sicherzustellen.
Ein methodisches Vorgehen, die sogenannte Translation Validation, prüft dabei a posteriori die
semantische Äquivalenz des Quellcodes mit dem übersetzten Programm.
Diese Dissertation beschreibt einen strukturellen Ansatz, welcher es ermöglicht, alle Schritte
einer Übersetzung mit der Translation Validation Methode zu verifizieren. Um eine präzise
Beschreibung der Semantik des Quellcodes und der ausführenden Maschine zu erstellen wurde,
basierend auf der Theorie der Abstract State Machine (ASM), eine geeignete Sprache (CASM)
spezifiziert und implementiert. Durch die innovative Technik der direkten symbolischen Ausführung
von ASM kann die Semantikspezifikation konkreter Programme in Prädikatenlogik erster
Stufe dargestellt werden. Diese Darstellung bildet die Grundlage für den formalen Beweis der
Übersetzerkorrektheit. Die sich ergebenden Beweisverpflichtungen weisen eine gemeinsame,
problembezogene Struktur auf. Der im Zuge dieser Arbeit entwickelte vanHelsing Beweiser ist
in Hinblick auf diese Struktur optimiert. Die Möglichkeit nicht bewiesene Probleme grafisch zu
untersuchen bietet, auch ungeübten Anwendern von Theorembeweisern, ein Werkzeug um die
jeweilige Ursache in der Problemdomäne zu identifizieren.
In der ausführlichen empirischen Untersuchung wird gezeigt, dass die CASM Sprache wesentlich
schnellere Programmausführung ermöglicht als andere ASM Implementierungen. Die
Geschwindigkeit ist hoch genug um sowohl Befehlssatz Simulatoren (Instruction Set Simulator)
als auch übersetzende Simulation (compiled simulation) aus den CASM Spezifikationen
der Maschine zu erzeugen. Der vanHelsing Beweiser ist, für Probleme hinsichtlich derer er optimiert
wurde, wesentlich schneller als andere Theorembeweiser. Erst diese effizienten Implemenix
tierungen ermöglichen dass die Laufzeiten, der im Zuge dieser Arbeiten erstellten Prototypen
für Translation Validation (Codeerzeugung, Registerzuteilung und Befehlsanordnung für VLIW
Maschinen), selbst für realistisch große Programme wie z.B.: bzip2, jeweils nur wenige Minuten
betragen.