Software-Ausfall: Logik-Methoden gegen Lücken

Am Krankenhaus Dornbirn mussten nicht dringende Operationen verschoben werden. Am Flughafen Wien fielen die Check-in-Systeme einzelner Airlines aus, sodass die Boardingprozesse manuell abgewickelt werden mussten. Auch international kam es an zahlreichen Flughäfen zu erheblichen Verzögerungen im Flugverkehr. Der 19. Juli des vergangenen Jahres ging als jener Tag in die Geschichte ein, der den IT-Ausfall von Crowdstrike markiert. Damals fielen weltweit Millionen von Computern aus. Der Grund dafür war ein fehlerhaftes Update der Antivirensoftware Crowdstrike.

LEARN gegen Lücken

Wenn es nach Laura Kovacs geht, soll so etwas nicht mehr passieren. Sie ist Professorin an der TU Wien und möchte mit ihrer Forschung zu logik-basierten Methoden solche Ausfälle in Zukunft verhindern. Mit ihrem Team arbeitet sie am Projekt LEARN. Dabei handelt es sich um ein Werkzeug, bzw. eine webbasierte Plattform, die automatisch Fehler in Software finden soll. Um das Werkzeug verwenden zu können, muss man kein Profi sein. Denn Kovacs und ihr Team haben daran gearbeitet, die Einstiegshürden so gering wie möglich zu halten. LEARN könne in zwei Schritten genutzt werden: „Erstens werden Softwareeigenschaften in logische Formeln übersetzt. Zweitens kann LEARN verwendet werden, um sicherzustellen, dass die jeweilige Software sicher ist. LEARN automatisiert diese beiden Schritte“, sagt Kovacs.

Fehler finden

Dafür braucht es sogenannte logikbasierte Methoden. Damit ist etwa gemeint, dass Maschinen selbstständig Beweise finden können. Sie prüfen, ob eine Aussage logisch aus einer anderen Aussage folgt oder, ob eine Aussage immer stimmt oder ob es ein Gegenbeispiel gibt, das bisher niemand entdeckt hat. Das funktioniert, indem man LEARN auf Computerprogramme anwendet. Beispielsweise kann damit untersucht werden, ob die Software Fehler enthält, welche Eigenschaften der Software aus mathematischer Sicht garantiert werden können und ob die Software die korrekte Antwort liefert.

Frei von Fehlern

Ziel von LEARN sei auch, dass die geprüfte Software fehlerfrei ist. Garantieren kann man das nicht. „Die Sicherstellung einer fehlerfreien Software ist extrem schwierig und in den meisten Fällen weder theoretisch noch praktisch möglich. Wir könnten und sollten jedoch die Anzahl der Softwarefehler minimieren, insbesondere die Fehler, die drastische Auswirkungen auf das Leben der Menschen haben würden“, sagt Kovacs.

Hilfe für Unternehmen

Viele Softwarefehler entstehen durch einen Logikfehler in einer Softwareaktualisierung oder durch Änderungen im Code. Entdeckt man diese Fehler rechtzeitig, kann das eine große Unterstützung für Unternehmen sein. „LEARN wird auf diese Weise gewaltige Kosten einsparen können, die für das Korrigieren fehlerhafter Software-Updates immer wieder anfallen“, sagt die TU-Forscherin.

Auf die Probe gestellt

Die Basis für LEARN wurde bereits entwickelt. Dafür hat Kovacs mit ihrem Team am Institut für Logic and Computation der Technischen Universität Wien ein „Proof of Concept-Grant“ erhalten. Das ist ein Stipendium im Wert von 150.000 Euro. Es zählt zu den höchstdotierten Förderungen der europäischen Forschungslandschaft und ist dafür gedacht, ein kommerziell vermarktbares Produkt zu entwickeln. In den nächsten 1,5 Jahren wird LEARN in einer industriellen Umgebung getestet. Zum Beispiel haben Amazon oder Microsoft zugesagt, das System zu testen und zu nutzen. Auf der TU Wien werden die Studierenden auch von LEARN profitieren. Hunderte werden die Möglichkeit haben, mit Hilfe von LEARN ihre Logik und Softwareanalyse-Fähigkeiten zu verbessern.