Von Überweisungen über die Abfrage des Kontostands bis hin zu Umbuchungen müssen Online-Banking-Programme viel können. Lange bevor Programmierer:innen für die Software die entsprechenden Algorithmen zur Verarbeitung von Eingaben schreiben, definieren sie, welche Funktionalitäten das Programm haben soll. Dazu bedienen sie sich verschiedener Spezifikationssprachen, mit denen sie die Eigenschaften von Programmen auf einer höheren Ebene beschreiben können. „Im Fall einer Banking-App muss zum Beispiel definiert werden, dass Nutzer:innen keine geheimen Informationen, wie zum Beispiel den Kontostand der anderen Nutzer:innen, erfahren“, erklärt Raven Beutner. Diese Geheimhaltungseigenschaft wird von Forscher:innen „Nicht-Interferenz“ genannt. Dass ein Banking-Programm diese Eigenschaft bei allen Ausführungen aufweist, darf nicht nur angenommen werden, sondern muss auch bewiesen werden können.
„Wir schauen uns deshalb an, wie ein Programm verschiedene Eingaben von Nutzer:innen verarbeitet und wie es sich während des Programmablaufs verhält“, erklärt Beutner. „Zum Nachweis vieler Programm-Eigenschaften reicht es, sich einen einzelnen Programmablauf oder zumindest eine begrenzte Zahl von Abläufen anzusehen. Das geht heute mithilfe von Algorithmen und Tools in vielen Fällen schon automatisch.“ Schwieriger wird es allerdings bei sogenannten Hypereigenschaften, zu denen auch die oben erwähnte Nicht-Interferenz zählt. „Das ist eine andere Klasse von Eigenschaften. Um sie zu beweisen, müssen wir mehrere Programmabläufe analysieren und miteinander vergleichen.“ Die Forschung hat in diesem Punkt in den vergangenen Jahren zwar Fortschritte gemacht, aber für viele Hypereigenschaften reichen laut Beutner bestehende Methoden noch nicht für eine automatische Prüfung aus. „In unserem Paper stellen wir eine neue Technik zum Prüfen von neuen Klassen solcher Eigenschaften vor.“
Mit der neuen Methode, die Beutner aufbauend auf der Arbeit von und in Kooperation mit CISPA-Faculty Prof. Bernd Finkbeiner entwickelt hat, sollen in Zukunft auch komplexere Hypereigenschaften automatisch geprüft werden können. Dieser neue methodische Ansatz zahlt auf das von Bernd Finkbeiner und seinem Team initiierte Projekt HYPER ein, für das Finkbeiner mit einem Advanced Grant der Europäischen Forschungskommission ausgezeichnet wurde. Erklärtes Ziel dieses Projekts ist es, künftig auch vielschichtige gesellschaftliche Konzepte wie Gerechtigkeit, Erklärbarkeit und Privatsphäre mathematisch formalisieren zu können und in Programmen automatisiert nachzuweisen.
„Mit unserem Ansatz haben wir einen guten ersten Schritt für die automatische Verifikation auch komplexer Hypereigenschaften gemacht. Aber noch ist viel Forschung nötig, um Bernds Vision umzusetzen“, sagt Beutner. So sei etwa die Implementierung des neuen Ansatzes, also die praktische Umsetzung in echten Systemen, noch prototypartig und damit nicht praxisreif. „Wir haben eben noch viel zu tun. Aber unser Papier ist ein erster Schritt dahin, eine noch breitere Klasse von Eigenschaften automatisch verifizieren zu können. Dass wir dafür einen Distinguished Paper Award bekommen haben, freut mich natürlich sehr. "
