Bei der Programmierung von Software passieren häufig Fehler. Damit die nicht zu ungewollten Abstürzen führen oder Sicherheitslücken eröffnen, testen Entwickler:innen Programme vor der Veröffentlichung oft mithilfe von sogenannten Fuzzern systematisch auf Schwachstellen. „Diese Tools produzieren massenhaft Zufallseingaben, um zu testen, wie sich Programme im Echtbetrieb schlagen. Eingaben zu produzieren, mit denen sich auch die tieferen Programmfunktionen testen lassen, ist allerdings schwierig“, erklärt Steinhöfel.
Woran liegt das? Die Datensprachen, die Computer sprechen und in denen mögliche Programm-Eingaben formuliert sind, ähneln in ihrem Grundaufbau den natürlichen Sprachen der Menschen. Und so spielt neben der Grammatik eben auch die Semantik, also die Bedeutung, eine Rolle. Den Unterschied hat der amerikanische Linguist Noam Chomsky in den 1950er-Jahren an einem Beispiel verdeutlicht: „Farblose grüne Ideen schlafen wütend.“ Die grammatikalische Struktur dieses Satzes ist einwandfrei, semantisch ist er allerdings inkorrekt. Sprich: Der Satzbau passt, auf der Bedeutungsebene ist das aber völliger Blödsinn.
Das Problem mit der Semantik-Ebene
Wenn ein Fuzzer also eine solche grammatikalisch zwar korrekte Eingabe produziert, sie aber keine für das zu testende Programm sinnvolle Aussage enthält, dann wird diese Eingabe direkt vom sogenannten Parser aussortiert. Der Parser ist ein Unter-Programm, das eingehende Eingaben in ihre Bestandteile zerlegt und prüft, ob sie für das Programm verständlich sind. Ist das der Fall, bereitet der Parser die Eingabe in ein zur Weiterverarbeitung geeignetes Format um. Wenn aber nicht, spuckt er eine Fehlermeldung aus und beschäftigt sich gar nicht weiter mit ihr. „Mit solchen Eingaben lässt sich also im Prinzip nur testen, wie gut der Parser ist, aber nicht, ob das Programm ansonsten stabil läuft“, sagt Steinhöfel. Es seien zwar durchaus Fuzzer im Einsatz, die klügere Eingaben produzieren und so um den Parser herumkommen. „Oft geht es aber spätestens danach nicht mehr weiter, weil dann kompliziertere Eigenschaften auf der Semantik-Ebene folgen.“
Neue Spezifikationssprache als Antwort
Die von Steinhöfel entwickelte Spezifikationssprache ISLa kann hier zum Gamechanger werden. „Wir können mit ISLa Eingaben mit einer nie dagewesenen Präzision verstehen und die Programme damit tief und gründlich testen.“ Der Schlüssel liegt laut dem Forscher in einem sehr allgemeinen Formalismus, der Forschenden und Entwickler:innen nahezu jedes Programm zugänglich macht. „Allerdings brauchen wir dafür die Eingabebeschreibung. Die können wir manuell schreiben oder aus einem bestehenden Programm heraus lernen.“ Das sei allerdings kompliziert und oft nur annäherungsweise möglich. „Es wird in der Praxis daher immer Programme geben, die zu groß oder zu kompliziert sind und sich nicht vollständig verstehen lassen. Aber wir können immer besser werden.“ ISLa ist dafür ein mächtiges Werkzeug und kann nicht nur Eingaben generieren, sondern diese auch prüfen, reparieren und mutieren. Zudem lassen sich damit laut Steinhöfel auch die Ausgaben des Programms beschreiben. „Wenn wir die Ein- und die Ausgaben beschreiben können, können wir das Verhalten des ganzen Programmes beschreiben. Und damit können wir wirklich viel tun: Wir können sagen, wie ein Programm sich verhalten soll, wir können analysieren, wie sich ein Programm verhält und wir können auch erzwingen, dass es sich verhält, wie wir es wollen. Kurzum: Wenn du die Ein- und Ausgaben kontrollierst, kontrollierst du die Programme.“ Auch Andreas Zeller, mit dem er eng zusammengearbeitet hat, unterstreicht, wie wichtig Steinhöfels Forschungsarbeit ist: „ISLa eröffnet ganze Welten für das Testen von Systemen.“
Von der Theorie in die Praxis
In der näheren Zukunft wird Steinhöfel sich damit beschäftigen, auf dem durch ISLa bereitgestellten Fundament praxisnahe Ansätze zum Testen relevanter Softwaresysteme zu entwickeln. Unter anderem wird er sich dabei mit dem Lernen komplexer Ein- und Ausgabebeschreibungen beschäftigen und sich zustandsbasierten Programmen wie zum Beispiel Datenbanken und Servern zuwenden. Zudem will er testen, ob eine Kombination mit bereits etablierten Testansätzen möglich ist.
Der gebürtige Pfälzer ist derzeit PostDoc am CISPA. Zuvor hat er an der TU Darmstadt studiert und promoviert. „Ohne genau zu wissen, wo das enden würde, arbeite ich schon seit 2021 auf ISLa hin.“ Und der Stolz auf das, was ihm damit gelungen ist, ist dem 34-Jährigen anzumerken.
Mehr Infos zum mit einem ERC Grant geförderten Projekt „S3 – Semantics of Software Systems“, bei dem die Spezifikationssprache ISLa eine wichtige Rolle spielt, gibt es hier.
