Im Flugzeug, im selbstfahrenden Auto oder bei sensiblen Online-Transaktionen: Oft sind wir davon abhängig, dass digitale Syseme korrekt funktionieren. Aber wie lässt sich das garantieren? Daniela Kaufmann vom Institut für Logic and Computation arbeitet an neuen Ideen, um diese Aufgabe zu lösen.
Untersucht man Hardware, Software oder auch ein kryptographisches System durch Ausprobieren aller logischen Möglichkeiten, wird die Aufgabe rasch unüberschaubar aufwändig: Eine astronomische Zahl denkbarer Inputs müsste durchprobiert werden, um die Korrektheit zu garantieren. Daniela Kaufmann will stattdessen das System in algebraische Formeln übersetzen, mit denen man effizient arbeiten kann. So sollen Werkzeuge für die Hardware- und Softwareindustrie entstehen, die mit mathematischer Präzision die Fehlerlosigkeit eines Computersystems beweisen.
Vertrauen ist schlecht, Kontrolle ist nötig
Wenn ein System bei vielen verschiedenen Eingaben bereits korrekt funktioniert hat, heißt das noch lange nicht, dass es auch beim nächsten Mal korrekt arbeiten wird, wenn man einen neuen Input ausprobiert. „Immer wieder findet man überraschende Fehler“, sagt Daniela Kaufmann. „Etwa der berühmte Pentium-Bug, der in den 1990ern dazu führte, dass Pentium-Prozessoren bei ganz bestimmten Divisionen ein falsches Ergebnis lieferten. Oder ein kürzlich entdeckter Bug in einem Linux-Kernel, der bestimmten Usern ermöglichte, sich unberechtigterweise einen Root-Zugriff zu verschaffen.“
In einer Welt, in der oft sogar unser Leben vom korrekten Funktionieren logischer Systeme abhängt, ist das beunruhigend: In kritischen Situationen möchte man einen mathematischen Beweis, dass ein Computersystem garantiert in jeder denkbaren Situation die richtige Antwort liefert.
Die automatische Sicherheitsgarantie
„Was wir brauchen, ist ein Tool, das automatisch die Korrektheit anderer Systeme prüft“, sagt Daniela Kaufmann. „Und das gibt es auch: Sogenannte SMT-Solver können automatisch feststellen, ob eine bestimmte logische Formel eine Lösung hat.“ Man muss also ein logisches System, etwa einen Teil eines Computerchips, in eine logische Formel übersetzen, und dem SMT-Solver die Frage stellen: „Gibt es eine mögliche Situation, in der diese logische Formel die Regeln bricht?“
Das ist allerdings oft extrem aufwändig. „Ein SMT-Solver formuliert die Logik dabei auf Bit-Ebene“, erklärt Daniela Kaufmann. „Wenn zum Beispiel zwei Zahlen miteinander multipliziert werden, dann kann man diese Multiplikation in logische Zusammenhänge zwischen den einzelnen Bits übersetzen, mit denen diese Zahlen codiert sind.“ Aber dadurch wird die recht simple Operation einer Multiplikation in ein recht unübersichtliches System logischer Verknüpfungen auf Bit-Ebene übertragen. Die mathematische Struktur der ursprünglichen Aufgabe wird nicht genutzt.
„Wir zerlegen arithmetische Teile eines Systems nicht vollständig in logische Aussagen über einzelne Bits“, sagt Daniela Kaufmann. „Stattdessen bewahren wir ihre algebraische Struktur und stellen sie als Polynome dar. Wir übersetzen die Logik der Schaltungen in mathematische Ausdrücke, mit denen man nach üblichen Regeln der Algebra rechnen kann.“
Allerdings will sich Daniela Kaufmann hier nicht auf bestehende Algebra-Tools verlassen: Die Algorithmen, die diese Polynome verarbeiten, sollen genau auf dieses Anwendungsgebiet maßgeschneidert werden. „Wichtig ist auch: Mit unserer Methode wird es möglich sein, eine Art Zertifikat auszustellen“, erklärt Kaufmann. „Wenn unsere Methode sagt: Ja, dieser Chip arbeitet korrekt, dann ist das nicht einfach nur ein Urteil, das man glauben muss, sondern man erhält eine überprüfbare mathematische Antwort, die diese Korrektheit beweist.“
Daniela Kaufmann
Daniela Kaufmann studierte Computermathematik an der Johannes Kepler Universität Linz und promovierte dort 2020 mit Auszeichnung im Fach Informatik. Nach mehreren Jahren als Universitätsassistentin in Linz arbeitete sie unter anderem am Software Competence Center Hagenberg und als Postdoc an der TU Wien.
Seit 2024 ist sie dort FWF-ESPRIT-Forschungsgruppenleiterin und leitet das Projekt „CalgSAT“, in dem Methoden der Computeralgebra mit SAT-Solving für automatisiertes mathematisches Schließen verbunden werden. Ihr Forschungsschwerpunkt liegt an der Schnittstelle von symbolischem Rechnen, formaler Verifikation und automatisiertem Schließen – insbesondere bei der Überprüfung arithmetischer Schaltungen, beim Rechnen in endlichen algebraischen Strukturen und bei maschinell kontrollierbaren Beweisen.
Ihre Dissertation wurde mit dem GI-Dissertationspreis und dem Heinz-Zemanek-Preis ausgezeichnet. Mit dem ERC-Grant „POLARIS“ (Advancing Polynomial and Logical Approaches for Trusted Automated Reasoning over Integrated Systems) wird sie nun ihr Team erweitern und ihre theoretischen Ideen in industriell nutzbare Werkzeuge übersetzen.
Rückfragehinweis
Dr. Daniela Kaufmann
Institut für Logic and Computation
Technische Universität Wien
daniela.kaufmann@tuwien.ac.at
Text: Florian Aigner