Auszug aus dem UnivIS Informationssystem der Universität Kiel - Semester: SS 2001
---

8100   Probleme beim Bau voll korrekter Übersetzer (korr. Übers.)

Dozent
Dr. Wolfgang Goerigk

 
Angaben
 Vorlesung mit Übung, 4 SWS, ECTS-Studium, ECTS-Credits: 6,0, Praktische Informatik

            Zeit und Ort: Di, Do 16:00 - 18:00, Raum CAP 3-I

Voraussetzungen / Organisatorisches
Für Studierende mit Hauptfach Informatik im Hauptstudium.

          Voraussetzungen: Vorlesungen im Grundstudium Informatik

Inhalt
Übersetzer werden als Werkzeuge an zentraler Stelle im Software-Entwicklungsprozess eingesetzt. Die Zuverlässigkeit und Sicherheit von Software hängt auch von der Korrektheit der zur Implementierung herangezogenen Übersetzerprogramme ab. Um korrekte Übersetzer zu entwerfen und schließlich korrekt auf der Maschine zu implementieren - zur Konstruktion voll korrekter Übersetzer - müssen sowohl die Korrektheit der Transformation (Übersetzungskorrektheit) als auch die der Implementierung des Übersetzers auf allen Ebenen bis hinab zum ablaufenden Maschinencode lückenlos nachgewiesen werden. Übersetzungsverifikation blickt bereits auf eine über 30jährige Tradition zurück. Übersetzer führen syntaktische Transformationen von Quell- in Zielprogramme durch, die die Semantiken von Quell- und Zielsprache zu respektieren haben. Adäquate Semantikdefinitionsstile für höhere Quellsprachen und maschinennahe Zielsprachen, verschiedene Korrektheitsbegriffe für Compiler sowie Methoden für den Korrektheitsnachweis (die Übersetzungsverifikation) werden im ersten Teil der Vorlesung studiert, vor allem mit Blick auf praktische Durchführbarkeit der Beweise und praktischen Nutzen der bewiesenen Eigenschaften.

 
Es ist möglich, Programme zu schreiben, die sich selbst reproduzieren, auch Übersetzer, die ihre eigene - z.B. absichtlich durch ein Trojanisches Pferd infizierte - Maschinencodeimplementierung reproduzieren, wenn sie zur Implementierung (zum Bootstrapping) ihres eigenen Quellcodes ausgeführt werden. Solche Programme können in speziellen Situationen oder für spezielle Eingaben, die nur dem Infizierer bekannt sind, katastrophale Auswirkungen haben, sind im Bereich der IT-Sicherheit (engl. security) untragbar. Absichtlich sehr versteckte Fehler werden durch Testen kaum gefunden werden. Wir werden im zweiten Teil einen solchen (sogar im Quellcode verifizierten) Übersetzer kennenlernen, der für alle bis auf zwei Quellprogramme korrekten Zielcode generiert, und der zudem, obwohl er falsch ist, den von Übersetzerbauern hochgeschätzten Wirth'schen strengen Übersetzertest besteht.

Im dritten Teil widmen wir uns der lückenlosen Verifikation der Übersetzerimplementierung, so daß jedweder Fehler, auch absichtliche wie Viren oder Trojanische Pferde, garantiert ausgeschlossen werden kann. Wir werden Methoden zur korrekten Programmkonstruktion und die Technik der a-posteriori-Programmprüfung studieren, mit der große Teile zu verifizierender Programme durch spezielle Überprüfungen abgesichert werden können. Eine spezielle Bootstrap-Technik mit nachträglicher Codeinspektion erlaubt den Nachweis der Korrektheit niederer Übersetzerimplementierungen mit weitgehender maschineller Unterstützung, ohne erneut in Abhängigkeit von unverifizierter Software zu geraten.

Die Vorlesung wendet sich an Hauptfach-Informatikstudenten nach dem Vordiplom. Kenntnisse in Übersetzerbau, Semantik von Programmiersprachen oder Programmverifikation sind von Vorteil, werden aber nicht vorausgesetzt.


Empfohlene Literatur

ECTS-Informationen:
Credits: 6,0

Zusätzliche Informationen
Schlagwörter: Korrekte Übersetzer
Erwartete Teilnehmerzahl: 20

Zugeordnete Lehrveranstaltungen
UE: Übungen zu: Probleme beim Bau voll korrekter Übersetzer
Dozent: Dr. Wolfgang Goerigk

Zeit und Ort: Mi 16:00 - 18:00, Raum SEM-Ü1



Einordnung
 Technische Fakultät
Diplom-Informatik (Dipl.-Inf.)
Hauptstudium
Vorlesungen/Übungen