Scalable translation validation : tools, techniques and framework

Abstract

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 Implementierungen 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.

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 CASM language, 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.