Foto: Prof. Andrey Rybalchenko, TU München
Davor, dass das bunte Windrad sich endlos dreht, sind selbst Spitzenforscher nicht sicher. Informatik-Professor Andrey Rybalchenko von der TU München saß erst vor wenigen Wochen wieder vor seinem Mac und wartete vergeblich darauf, dass der Rechner nach einem Mausklick den nächsten Arbeitsschritt abschließt. Dem 32-Jährigen könnte es durch seine Forschungsarbeit allerdings gelingen, dass solche Situationen künftig nicht mehr vorkommen.
Er lässt damit nicht nur gestresste Büroangestellte aufatmen, sondern hat auch einen Ausweg aus einem langjährigen Problem der Informatik gefunden. Rybalchenko erhält dafür am 22. September auf der Technik-Konferenz "EmTech@MIT" im amerikanischen Cambridge/Massachusetts die Auszeichnung "TR35". Die Technology Review, das Magazin des Massachusetts Institute of Technology (MIT), ehrt damit jedes Jahr 35 Wissenschaftler bis 35 Jahre. Das Schaffen der "jungen Innovatoren" habe das Potenzial, die Welt zu verändern, so die Begründung für den Preis.
Software-Fehlern ungeschützt ausgesetzt
Die Welt verändern durch weniger Fehler in Computer-Programmen - was zunächst hochtrabend klingt, erklärt der junge TU-Professor so: Die menschliche Zivilisation sei abhängig von Software. Ob im Auto-Airbag oder in Steuerungssystemen für Flugzeuge: "Unser Leben ist Software-Fehlern ungeschützt ausgesetzt", schreibt Rybalchenko.
Wer im Büro mit dem Rechner arbeitet, für den hat das Problem indes meist keine so dramatischen Konsequenzen: Nach dem Klick auf eine Schaltfläche oder dem Druck auf die Eingabetaste fängt beim Windows-PC die Sanduhr, beim Mac das Windrad an zu rotieren und hört nicht mehr auf. Mitten in einem Arbeitsschritt ist der Computer wie eingefroren. Der eine seufzt, der andere flucht - Informatiker wie Rybalchenko nennen das Ereignis trocken "Verletzung der Lebendigkeitseigenschaften".
Neuer Ausweg aus einem alten Informatik-Problem
Das Problem galt in seiner Zunft lange als besonders tückisch. Anders als bei Fehlern, die zu einem völligen Absturz führen, läuft bei einer Verletzung der Lebendigkeitseigenschaften das Programm weiter - es nimmt aber keine neuen Befehle an und tut nichts Sinnvolles. Für Software-Tester ist mit dieser Art von Bugs besonders schwer umzugehen. "Woher sollen sie wissen, ob sie noch eine Minute warten sollen oder ob nie eine Antwort kommt?" erläutert Andrey Rybalchenko.
Für Informatiker steckte zudem eine besondere akademische Herausforderung in dem Problem. In den 1930er Jahren hatte der Informatik-Pionier Alan Turing es als sogenanntes "Halteproblem" beschrieben und gezeigt, dass es nicht grundsätzlich lösbar sei. Für alle möglichen Eingaben zu beweisen, dass ein Programm sinnvoll reagiert, schien unmöglich.
Andrey Rybalchenko entdeckte nun zusammen mit dem Freiburger Informatik-Professor Andreas Podelski ein neues Prinzip namens "Transitionsinvarianten". Damit sei es möglich, in automatischen Verfahren die Lebendigkeitseigenschaften von Software zu beweisen, erklärt Rybalchenko. Der Kniff der beiden Wissenschaftler: Sie schafften es, den aus vielen Teilgebieten der Informatik bekannten Ansatz "Teile und herrsche" auch auf die Lebendigkeitseigenschaften anzuwenden. Das große Problem wird in viele kleine und lösbare Probleme zerlegt. Die einzelnen Ergebnisse werden anschließend wieder zusammengesetzt.
Tool an Windows-Treibern getestet
Andrey Rybalchenko setzte die Transitionsinvarianten anschließend in die Praxis um. Im Sommer 2005 arbeitete er drei Monate lang bei Microsoft Research im englischen Cambridge. Dort begann er ein Verifikations-Tool zu entwickeln, dem er den Namen Terminator gab. Mit Byron Cook von Microsoft testete der Informatiker den Terminator an Windows-Gerätetreibern. Immer wenn sie angefordert wurden, reagierten die Abfertigungsroutinen der Treiber nachweisbar auf das Betriebssystem. Die Versuche zeigten, dass die bisher als unmöglich geltenden automatischen Testverfahren von Lebendigkeitseigenschaften sich doch durchführen lassen.
Bei Microsoft arbeitet man jetzt auf Grundlage von Rybalchenkos Erkenntnissen weiter. Ansätze des Terminators könnten einfließen in künftige Versionen des Static Driver Verifiers (SDV). Dieses Werkzeug sucht nach Fehlern im Code von Windows-Treibern. Ob und wann die Projektarbeit in einen neuen SDV münden wird, sei derzeit nicht abzusehen, lässt Byron Cook aus Cambridge ausrichten. Er schickt hinterher: Andrey Rybalchenko sei ein fantastischer Wissenschaftler und Dozent. "Er besitzt die wunderbare Gabe, reale Probleme mit tiefschürfender mathematischer Theorie zu verbinden."
32-jähriger Informatik-Professor will Software sicherer machen
Andrey Rybalchenko, dessen Lebenslauf samt Publikationsliste trotz seines jugendlichen Alters schon elf Seiten lang ist, denkt inzwischen ebenfalls weiter, wie seine Entdeckung genutzt werden könnte. Nicht genug damit, dass ein Werkzeug wie der Terminator die Qualität von Software verbessere, dadurch weniger Fehler aufträten und Firmen viel Geld sparten. Verifikations-Methoden seien auch gut geeignet, um die Sicherheit von Programmen zu erhöhen. "Man könnte damit nachweisen, ob eine Software bei beliebigen Eingaben immer im Rahmen des Erlaubten reagiert oder ob Exploits möglich sind", erklärt der Professor für Theoretische Informatik.
Berufen hat ihn die Technische Universität München Anfang des Jahres. Vorher leitete er eine Forschungsgruppe für Verifikation am Max-Planck-Institut für Software-Systeme in Saarbrücken und Kaiserslautern. Studiert hat der in Russland aufgewachsene Rybalchenko zunächst in Voronezh in seinem Geburtsland, später an der Universität des Saarlandes. Rybalchenko ist der zweite Informatiker in Folge aus Saarbrücken, der in die Reihe der "TR 35" aufgenommen wurde. Voriges Jahr erhielt der Informatiker Michael Backes die Auszeichnung, der weiterhin in Saarbrücken lehrt und forscht.
Radfahren und Surfen als Ausgleich
Andrey Rybalchenko radelt unterdessen fast jeden Morgen von seiner Wohnung in München-Schwabing die gut 15 Kilometer Richtung Norden zum Sitz seiner Fakultät nach Garching - und widmet sich nach Turings Halteproblem auch wieder Grundlagen seines Fachs. "Gerade bereite ich eine Einführungsvorlesung für nächstes Semester vor", erzählt er. 2003 stand er an der Uni in Saarbrücken zum ersten Mal vor Studenten und hielt ein Programmier-Tutorium. "Nach fünf Jahren in Forschungslabors jetzt wieder zu lehren, macht großen Spaß", sagt er.
Wenn er den Kopf völlig von Informatik frei bekommen will, begibt sich Andrey Rybalchenko zum Windsurfen aufs Wasser. Er sagt: "Das ist ein fantastisches Gefühl, als ob man fliegt." - Und das ganz ohne die Gefahr, wegen eines Software-Fehlers abzustürzen.