|
Klosterneuburg/Wien (prd) - Um die Sicherheit von Computerprogrammen und Hardware zu erhöhen, braucht es
mathematische Analysemethoden. Dank eines Forscherteams um Krishnendu Chatterjee in einem vom Wissenschaftsfonds
FWF finanzierten Projekt werden diese Methoden in Zukunft deutlich schneller sein.
Sicherheitslücke in Programm entdeckt, Update dringend empfohlen. Schlagzeilen wie diese erreichen uns derzeit
wöchentlich. Oft wird schon zum Verkaufsstart eines neuen Programms ein umfangreiches Update angeboten, das
Kinderkrankheiten behebt. Das bringt vielerlei Probleme, öffentliche Institutionen aber auch Unternehmen leiden
unter der Unsicherheit und sind immer wieder Hacker-Angriffen ausgesetzt. In immer mehr sensiblen Bereichen wird
Software eingesetzt, deren Versagen im Extremfall sogar lebensgefährlich wäre. Nicht alle Bereiche sind
gleichermaßen betroffen, viele Computersysteme laufen wie das sprichwörtliche Schweizer Uhrwerk, vor
allem Hardware ist in der Regel sehr verlässlich, eher auf der Software-Seite gibt es Probleme.
Mathematik verbessert Computersysteme
Bei komplexen Programmen ist es tatsächlich schwierig, jede kleine Eventualität zu berücksichtigen.
Zwar gibt es Computermethoden für Software-Tests, jedoch wuchs die Komplexität der Programme in den vergangenen
Jahren stetig, während die Leistungsfähigkeit der Testmethoden hinterherhinkte, insbesondere was ihre
Geschwindigkeit angeht - ein guter Anlass, hier in Grundlagenforschung zu investieren. Der Computerwissenschafter
Krishnendu Chatterjee beschäftigte sich in einem vom Wissenschaftsfonds FWF finanzierten und kürzlich
abgeschlossenen Projekt mit der Analyse von Computersystemen mittels mathematischer Methoden. Damit, so die Hoffnung,
sollten grundlegende Verbesserungen in dem Sektor möglich sein.
Graphentheorie
"Dieses Gebiet hat eine lange Tradition", sagt Chatterjee. "Es gibt seit langer Zeit Versuche,
eine formale Basis zu finden, um korrekte Systeme zu designen. Fundamentale Arbeiten in diesem Bereich stammen
aus den Sechzigerjahren und gehen etwa auf Alonzo Church zurück, eine der Gründerfiguren der Computerwissenschaften."
Für die mathematische Analyse von Computersystemen wird die sogenannte "Graphentheorie" genutzt.
Ihr Gegenstand sind Objekte, die man sich als Netzwerke aus miteinander verbundenen Punkten oder Knoten vorstellen
kann. Computersysteme lassen sich mathematisch als Graphen darstellen: Ein Knoten steht für einen bestimmten
Zustand, in dem sich das System befindet, eine Kante steht für einen Übergang zwischen zwei Zuständen.
Zum Beispiel befindet sich ein Computer, der gerade diesen Artikel anzeigt, in einem definierten Zustand, der als
Knoten dargestellt wird. Beim Klicken auf einen Link wechselt das System in einen neuen Zustand, dieser Wechsel
wird als Kante dargestellt.
Verbesserte Graphen-Algorithmen
Dieser Rahmen ist besonders geeignet für die Prüfung von Computersystemen. Chatterjee interessierte sich
dafür, wie schnell diese Algorithmen zur Überprüfung (der Fachausdruck lautet "Verifikation")
von Computersystemen funktionieren. "Computersysteme werden immer komplexer", sagt Chatterjee. "In
manchen Bereichen steckte die Entwicklung in der Verifikation seit den Neunzigern fest. Ein neuer Aspekt dieses
Projekts war, aktuelle Zugänge aus der Graphentheorie zu verwenden, um die Algorithmen zu verbessern. Das
war eine völlig neue Richtung." Chatterjee hebt die Zusammenarbeit mit seiner Projektpartnerin Monika
Henzinger von der Universität Wien hervor, die Expertin für Graphentheorie ist. "Für mich war
das ein intensiver Lernprozess. Es war sehr interessant zu sehen, wie die Methoden der Graphen-Algorithmen adaptiert
und erweitert werden müssen, um wirklich bessere Algorithmen für die Probleme zu bekommen, die wir untersucht
haben."
Grenzen, Bedingungen, Erfolge
Hier war das Projekt sehr erfolgreich: Es gelang, mehrere seit den Neunzigerjahren bestehende Schranken für
die Geschwindigkeit bestimmter Verifikationsalgorithmen zu durchbrechen, etwa im Bereich sogenannter "Markov
Decision Processes". Das sind Modelle, die mehrere Auswahlmöglichkeiten und ein Zufallselement beinhalten.
"Ein Beispiel ist die Entwicklung von Robotern", erklärt Chatterjee. "Ein Roboter interagiert
mit einer Umgebung, in der es Unsicherheit gibt, und er hat Auswahlmöglichkeiten, kann etwa nach links oder
rechts gehen. 'Markov Decision Processes' sind ein Modell dafür." Für viele Anwendungen ist die
Beantwortung der Frage zentral, welche Ereignisse in so einem Modell mit absoluter Sicherheit eintreten. "Der
bisher effizienteste Algorithmus dafür war aus 1995 und hatte quadratische Komplexität", sagt Chatterjee.
Damit ist gemeint, dass die Laufzeit des Algorithmus mit der Größe des untersuchten Systems quadratisch
steigt - ein doppelt so großes System braucht also die vierfache Laufzeit. "In unserem Projekt konnten
wir diese Grenze mit Graph-algorithmischen Techniken überwinden."
Chatterjee ist mit dem Erfolg des Projekts sehr zufrieden. "Auch unsere beiden Studenten Sebastian Krinninger
und Marthin Chmelik schlugen sich ausgezeichnet, beide erhielten Preise für ihre Dissertationen", sagt
Chatterjee. Er betont, dass es sich trotz der Brisanz des Themas um ein reines Grundlagenprojekt handelte. "Unsere
erste Arbeit war sehr theoretisch. Nun versuchen wir, Grenzen oder Bedingungen aufzuzeigen, wie schwierig es sein
wird, unsere Algorithmen weiter zu verbessern. Auf der anderen Seite wollen wir sehen, wie sich diese Zugänge
in der Praxis umsetzen lassen."
Zur Person
Krishnendu Chatterjee (https://ist.ac.at/research/research-groups/chatterjee-group/)
ist Professor am IST Austria (Institute for Science and Technology, https://ist.ac.at/)
in Klosterneuburg. Er interessiert sich besonders für die Verifikation von Computersystemen und Spieltheorie.
|
