SW_GruVe: Keine Chance für den Fehlerteufel

27 Januar 2022

Am Forschungsinstitut CODE laufen derzeit über 30 Projekte aus verschiedenen Forschungsgebieten in den Bereichen IT-Sicherheit, Quantentechnologien und Smart Data. Im Interview erklären die beteiligten Forscherinnen und Forscher ihre Arbeit sowie mögliche praktische Anwendungsfälle. Heute: Prof. Dr. Gunnar Teege über das Projekt „SW_GruVe“.

Herr Prof. Teege, worum geht es genau im Projekt „SW_GruVe“, und wofür steht die Abkürzung?

Das „GruVe“ steht für „Grundlagen für formale Verifikation“, das „SW“ für „Software“. Es geht um formale Programmverifikation, dabei werden mathematische Beweise erstellt, die zeigen, dass ein Programm das tut, was es soll. Im Projekt erweitern wir existierende Grundlagen und wenden sie in der Praxis an. Ziel ist es, die Entwicklung von Software sicherer zu machen und leider allgegenwärtige Programmierfehler zu vermeiden.

Formale Programmverifikation kann also dazu beitragen, menschliche Programmierfehler zu erkennen?

Ja, die Mathematik ist da gnadenlos. Wenn der Beweis rechnergestützt erstellt und geprüft wird, ist das Programm garantiert fehlerfrei. Dazu verwendet man sogenannte Beweisassistenten, in unserem Projekt ist das das an der Technischen Universität München entwickelte System „Isabelle“. Solche Systeme werden inzwischen in vielen Bereichen eingesetzt, um mathematische Beweise zu erstellen, ohne dabei Fehler zu machen. Denn natürlich hilft der Beweis nur, wenn er auch selbst korrekt ist.

Warum ist die formale Programmverifikation bisher noch so aufwändig und wird nicht standardisiert eingesetzt?

Wer schon mal einen mathematischen Beweis auf dem Papier erstellt hat, weiß, wie mühsam es sein kann, die vielen kleinen Schritte zusammenzusetzen und dabei nicht in die Irre zu laufen. Bei berühmten Problemen der Mathematik hat das teilweise Jahrhunderte gedauert. Auch „Isabelle“ findet den Beweis nicht automatisch. Man muss die Schritte vorgeben; das System vollzieht sie dann nach und prüft, ob sie eine geschlossene Kette zum gewünschten Ziel bilden. Und wenn das Programm fehlerhaft ist, gibt es diese Kette nicht, dann kann man es beliebig lange probieren. Es ist nicht immer einfach, aus diesen Versuchen auch zu erkennen, wo der Fehler steckt. All dies erfordert viel Übung und Spezialkenntnisse, die die wenigsten Softwareentwickler haben. Aber wenn man es mal geschafft hat, einen Beweis zu erstellen, kann man sicher sein, dass keine Fehler mehr enthalten sein können. Das ist etwas, das man auch mit den besten Testverfahren nie erreichen kann.

"Wenn man es mal geschafft hat, einen Beweis zu erstellen, kann man sicher sein, dass keine Fehler mehr enthalten sein können. Das ist etwas, das man auch mit den besten Testverfahren nie erreichen kann." 

Welchen Lösungsansatz verfolgt Ihr Projekt und welche Rolle spielen unterschiedliche Programmiersprachen dabei?

Wir versuchen, den Automatisierungsgrad bei der Beweisfindung zu erhöhen. Ein Ansatz, den wir dazu verwenden, ist die automatische Übersetzung in eine andere Programmiersprache, in der potenzielle Fehlermöglichkeiten automatisch erkennbar sind. Vermeidet man diese, kann man vollautomatisch beweisen, dass beide Programme das Gleiche tun. Auf diese Weise eliminieren wir die berüchtigten Fehlerquellen beim Umgang mit Zeigern, also Objekten in Programmiersprachen, die eine Speicheradresse zwischenspeichern. Wir verwenden dazu die Programmiersprache Cogent, die von einer Gruppe an der australischen University of New South Wales entwickelt wurde.

Ein weiterer Ansatz ist die Erstellung einer umfangreichen Bibliothek aus Beweisregeln zusammen mit einer „Anleitung“, wie man diese Regeln auf typische Programmteile anwendet. Damit unterstützen wir die Erstellung der Beweise für die nach Cogent übersetzten Programme. Cogent ist eine funktionale Programmiersprache, das macht die Beweise einfacher als beispielsweise für C-Programme.

Sie arbeiten eng mit verschiedenen Partnern aus der Industrie zusammen. Welche Vorteile bringt das für Ihre Arbeit, und wie genau trägt Ihre Forschung schon jetzt dazu bei, Software sicherer zu machen?

Die Idee der formalen Programmverifikation und viele Methoden dazu existieren seit Jahrzehnten. Im Projekt ist es uns wichtig, sie in die praktische Umsetzung zu bringen. Dazu reicht es nicht, sie auf akademische „Spielbeispiele“ anzuwenden, sondern wir lassen uns durch industrielle Aufgabenstellungen leiten. Diese liefern uns die Industriepartner.

"Im Projekt ist es uns wichtig, die Idee der formalen Programmverifikation in die praktische Umsetzung zu bringen."

In SW_GruVe sind das die durch den Partner Hensoldt Cyber als Teil des Projekts entwickelten Komponenten eines hochsicheren Betriebssystems für den kommerziellen Einsatz. Zumindest diese Komponenten macht das Projekt sicher, viel wichtiger sind aber die entstehenden Werkzeuge und Methoden, mit denen sich zukünftig fehlerfreie Software mit geringerem Aufwand als bisher entwickeln lässt.

Prof. Dr. Gunnar Teege ist seit 2001 Professor am Institut für Technische Informatik der Fakultät für Informatik der UniBw M. Seine Forschungsinteressen liegen u.a. in den Bereichen Formale Verifikation von Betriebssystem-Komponenten, Virtualisierung von Rechnerkomponenten, Rechnerunterstützung in der Hochschullehre und Militärische Kommunikationssysteme. Als assoziierter CODE-Professor führt er regelmäßig Projekte über das Forschungsinstitut durch.

Ansprechpersonen:

Prof. Dr. Gunnar Teege
Institut für Technische Informatik
Universität der Bundeswehr München
Tel.: +49 89 6004 3353
E-Mail: gunnar.teege@unibw.de 

Lisa Scherbaum
Referentin für Öffentlichkeitsarbeit
Forschungsinstitut CODE
Universität der Bundeswehr München
Tel.: +49 89 6004 7307
E-Mail: lisa.scherbaum@unibw.de

_{Bild: © AdobeStock / peach_fotolia}