Formal framework for proof generating optimizers [Elektronische Ressource] / von Marek Jerzy Gawkowski

Description

Formal Framework forProof Generating OptimizersVom Fachbereich Informatikder Universität Kaiserslauternzur Verleihung des akademischen GradesDoktor der Naturwissenschaften (Dr. rer. nat.)genehmigte DissertationvonMarek Jerzy GawkowskiNovember 25, 2008Termin der wissenschaftlichen Aussprache: 20.04.2009Dekan: Prof. Dr. Karsten BernsVorsitzender des Prüfungsausschusses: Prof. Dr. Karsten Berns1. Berichterstatter: Prof. Dr. Arnd Poetzsch-He!ter2. Berich Prof. Dr. Klaus SchneiderD 386VZusammenfassung. Ein Softwaresystem wird meistens entweder in einer Spezifikations- oder einerhöheren Programmiersprache geschrieben. Dessen Laufzeitverhalten wird jedoch durch den Maschinen-code, der das Ergebnis der Übersetzung seiner Beschreibung in einer höheren Quellsprache ist, bestimmt.Für ein unkritisches Softwaresystem mag es ausreichen, dieses auf die Abwesenheit der Fehler durch Über-prüfungvonTestläufenzutesten.FüreinsicherheitskritischesSoftwaresystemkommenjedocherschwerendzwei Faktoren hinzu. Erstens, der Software-Producer, der dieses Softw implementiert hat, mussformal nachweisen, dass sein Maschinencode die formale Spezifikation, die vom Software-Consumer aus-gestelltwirdundseineSafety-Policy beschreibt,erfüllt.Zweitens,dieQuellsprachenbeschreibungdesSoft-waresystemsistdasErgebnisderAnwendungderstatischenAnalyseundformalerMethoden,welchedieseBeschreibung in Richtung E!zienz und Korrektheit optimieren.

Sujets

• Informatik

Informations

• Publié par: technische_universitat_kaiserslautern
• Publié le: 01 janvier 2008
• Nombre de lectures: 26
• Langue: Deutsch
• Poids de l'ouvrage: 2 Mo

Extrait

Formal Framework for
Proof Generating Optimizers
Vom Fachbereich Informatik
der Universität Kaiserslautern
zur Verleihung des akademischen Grades
Doktor der Naturwissenschaften (Dr. rer. nat.)
genehmigte Dissertation
von
Marek Jerzy Gawkowski
November 25, 2008
Termin der wissenschaftlichen Aussprache: 20.04.2009
Dekan: Prof. Dr. Karsten Berns
Vorsitzender des Prüfungsausschusses: Prof. Dr. Karsten Berns
1. Berichterstatter: Prof. Dr. Arnd Poetzsch-Heffter
2. Berich Prof. Dr. Klaus Schneider
D 386V
Zusammenfassung. Ein Softwaresystem wird meistens entweder in einer Spezifikations- oder einer
höheren Programmiersprache geschrieben. Dessen Laufzeitverhalten wird jedoch durch den Maschinen-
code, der das Ergebnis der Übersetzung seiner Beschreibung in einer höheren Quellsprache ist, bestimmt.
Für ein unkritisches Softwaresystem mag es ausreichen, dieses auf die Abwesenheit der Fehler durch Über-
prüfungvonTestläufenzutesten.FüreinsicherheitskritischesSoftwaresystemkommenjedocherschwerend
zwei Faktoren hinzu. Erstens, der Software-Producer, der dieses Softw implementiert hat, muss
formal nachweisen, dass sein Maschinencode die formale Spezifikation, die vom Software-Consumer aus-
gestelltwirdundseineSafety-Policy beschreibt,erfüllt.Zweitens,dieQuellsprachenbeschreibungdesSoft-
waresystemsistdasErgebnisderAnwendungderstatischenAnalyseundformalerMethoden,welchediese
Beschreibung in Richtung Effizienz und Korrektheit optimieren. Demnach ist das Ziel der Erstellung der
formal nachweisbaren Übersetzungskorrektheit ausschlaggebend für den Erfolg bei der Implementierung
eines sicherheitskritischen Softwaresystems.
In dieser Dissertation schlage ich einen Ansatz zu zertifizierenden Übersetzern vor, der die Formalis-
menundTechnikenausdenBereichendermathematischenLogikundProgrammiersprachenanwendet,um
das letztgennante Ziel zu erreichen. Ich nenne den Ansatz foundational translation validation (FTV). Ein
Compilerhersteller,derdiesenAnsatzverfolgt,implementierteinFTV-System,dasnebendemÜbersetzer-
programmauseinemSpezifikations-undVerifikationsframework (SVF)besteht.DasSVFwirdinderLogik
höherer Stufe (HOL) implementiert und seine wichtigste Komponente ist ein Übersetzungsvertrag, der die
Formalisierungen der Quell- und Zielsprache sowie eines zweistelligen Übersetzungskorrektheitsprädikates
corrTrans(S,T) über die Quellprogramme S und die Zielprogramme T enthält. Die Formalisierungen der
Sprachen werden als sog. tiefe Einbettungen in HOL realisiert. Durch Verwendung von tiefen Einbet-
tungen erreicht man, dass ganze Programme in diesen Sprachen als HOL-Konstanten deklariert werden
können. Die Definition von corrTrans drückt formal aus, was es heißt, dass T die korrekte Übersetzung
von S ist, und verwendet explizit die Definitionen der Programmsemantiken der Quell- und Zielsprachen,
die vom Übersetzungsvertrag festgelegt werden. Im Anschluss an die Übersetzung des Quellprogramms
übersetzt der Übersetzerprogramm das Quell- und das Zielprogramm in ihre textuellen Repräsentationen
als HOL-Konstanten S und T und generiert einen Korrektheitsbeweis für die Gültigkeit des der Aussage
corrTrans(S,T).IchnenneeinÜbersetzerprogramm,dasdenFTV-Ansatzverfolgt,einbeweisgenerierender
Übersetzer und ein Beweisskript, das den Korrektheitsbeweis enthällt, ein Übersetzungszertifikat.
DieIdee,dassProgrammeinKorrektheitsbeweisenalslogischeKonstanterepräsentiertwerdenkönnen,
istnichtneuundwurdevondemfoundationalproof-carryingcode-Ansatzübernommen.AndereMerkmale
des Ansatzes, die neuartig sind, und ihn von anderen Ansätzen zu zertifizierenden Übersetzern, wie proof-
carrying code (PCC) und translation validation (TV), unterscheiden, sind die folgenden:
Die Anwesenheit eines expliziten und formalen Übersetzungsvertrags: Die Ansätze PCC und TV sehen
weder die Formalisierungen des Übersetzungsvertrags noch die Verwendung von Theorembeweisern
zum Zwecke der Verifikation der Übersetzungen vor. Stattdessen werden zum Zwecke der Überset-
zungsverifikation dedizierte Übersetzungsvalidierungswerkzeuge verwendet. Dabei werden die oper-
ationalen Semantiken der Quell- und Zielsprache sowie ein sogenanntes Übersetzungskorrektheits-
kriterium mit Mitteln der Implementierungssprachen dieser Werkzeuge kodiert und in diese eingebet-
tet.
Die Repräsentation der Programme in Korrektheitsbeweisen als logische Konstanten: ImRahmenderAn-
sätze PCC and TV werden die Programme in ihre semantische Abstraktionen übersetzt. Diese Ab-
straktionen werden den Übersetzungsvalidierungswerkzeugen als Eingaben übergeben.
Zertifizierung von Programmtransformationsketten: Im Gegensatz zu dem TV-Ansatz, der auf die Zerti-
fizierung von einzelnen Programmtransformationen spezialisiert ist, ermöglicht der FTV-Ansatz die
Zertifizierung von ganzen Ketten von Programmtransformationen. Dies rührt von der Tatsache her,
dass die Definitionen der Programmsemantikfunktionen im Übersetzungsvertrag die Programme in
Elemente der Menge, die durch eine transitive Relation "≤" partiell geordnet sind, abbilden.
Diese Dissertation erläutert den FTV-Ansatz anhand eines FTV-Systems, das im Rahmen der Dok-
torarbeit implementiert wurde. Das System besteht aus einem Übersetzer-Frontend, das seine Opti-
mierungsphase zertifiziert und einem SVF, das mit dem Theorembeweiser Isabelle/HOL implementiert
wurde. Der Schwerpunkt dieser Dissertation liegt auf der Beschreibung des SVF und seiner Techniken der
Übersetzungsverifikation.VI
Summary. Most software systems are described in high-level model or programming languages. Their
runtimebehavior,however,isdeterminedbythecompiledcode.Foruncriticalsoftware,itmaybesufficient
to test the runtime behavior of the code. For safety-critical software, there is an additional aggravating
factor resulting from the fact that the code must satisfy the formal specification which reflects the safety
policy of the software consumer and that the software producer is obliged to demonstrate that the code
is correct with respect to the specification using formal verification techniques. In this scenario, it is of
greatimportancethatstaticanalysesandformalmethodscanbeappliedonthesourcecodelevel,because
this level is more abstract and better suited for such techniques. However, the results of the analyses and
the verification can only be carried over to the machine code level, if we can establish the correctness of
the translation. Thus, compilation is a crucial step in the development of software systems and formally
verified translation correctness is essential to close the formalization chain from high-level formal methods
to the machine-code level.
In this thesis, I propose an approach to certifying compilers which achieves the aim of closing the
formalization chain from high-level formal methods to the machine-code level by applying techniques
from mathematical logic and programming language semantics. I propose an approach called foundational
translation validation (FTV) in which the software producer implements an FTV system comprising
a compiler and a specification and verification framework (SVF) which is implemented in higher-order
logic (HOL). The most important part of the SVF is an explicit translation contract which comprises
the formalizations of the source and the target languages of the compiler and the formalization of a
binary translation correctness predicate corrTrans(S,T) for source programs S and target programs T.
The formalizations of the languages are realized as deep embeddings in HOL. This enables one to declare
the whole program in a formalized language as a HOL constant. The predicate formally specifies when T
is considered to be a correct translation of S. Its definition is explicitly based on the program semantics
definitions provided by the contract. Subsequent to the translation, the compiler translates
the source and the target programs into their syntactic representations as HOL constants, S and T, and
generatesaproofof corrTrans(S,T).WecallacompilerwhichfollowstheFTVapproachaproof generating
compiler.
Our approach borrows the idea of representing programs in correctness proofs as logic constants from
thefoundationalproof-carryingcode(FPCC)approach.Novelfeaturesthatdistinquishourapproachfrom
further approaches to certifying compilers, such as proof-carrying code (PCC) and translation validation
(TV) are the following:
The presence of an explicit translation contract formalized in HOL: TheapproachesPCCandTVdonot
formalize a translation contract explicitly. Instead of this, they incorporate operational semantics and
translation correctness criterion in translation validation tools on the programming language level.
Representation of programs in correctness proofs as logic constants: The approaches PCC and the TV
translate programs into their representations as semantic abstractions that serve as inputs for trans-
lation validation tools.
Certification of program transformation chains: Unlike the TV approach, which certifies single pro