Optimierende Compiler: Vertrauen ist gut, Verifikation ist besser!

Nicht nur die Rufe nach sicheren Informationssystemen werden immer
lauter, auch die Forschungsaktivitäten in diesem Bereich nehmen
beständig zu. Um wirklich sichere Informationssysteme zu
entwerfen und
zu implementieren, müssen viele einzelne Problemstellungen gelöst
werden. Ein wichtiger Aspekt untersucht die Sicherheit und
Korrektheit
von den bei Entwurf und Implementierung eingesetzten
Werkzeugen. Compiler sind ein solches Werkzeug. Sie transformieren
Programme in menschenlesbarer Notation in ausführbaren Code und
erfüllen damit eine zentrale Aufgabe bei der Konstruktion von
Softwaresystemen. Auch wenn wir typischerweise darauf vertrauen,
dass
Compiler korrekt arbeiten, so haben sie doch ihre Fehler,
insbesondere
optimierende Compiler. In diesem Artikel stelle ich die
Forschungsarbeiten meiner Arbeitsgruppe zur Verifikation
optimierender
Compiler dar und zeige dabei nicht nur beispielhaft typische
Probleme,
Lösungsansätze und Methoden von Forschungsarbeiten im Bereich
Sicherheit auf, sondern diskutiere auch, welche weiterführenden
Herausforderungen und Visionen sich daraus ergeben.