Automatische Überprüfung der Sicherheit von kritischer Software

Vier junge Forscher des INRIA (französisches Forschungsinstitut für Informatik und Automatik) haben ein Stipendium des sehr selektiven Europäischen Forschungsrates (ERC) erhalten, mit dem sie über 5 Jahre und mit einem Budget von 1 bis 1,5 Mio. Euro exploratorische Forschung betreiben können. Xavier Rival, Informatiker und Mitglied des Projektteams „Abstraction“, ist einer der vier Gewinner. Sein Projekt behandelt die Automatische Überprüfung der Sicherheit von kritischer Software.
Ein Fehler in der Software kann katastrophale menschliche und wirtschaftliche Folgen haben, vor allem wenn es sich um kritische Software handelt, die in den Steuersystemen von Flugzeugen, in der Raumfahrt, der Kernenergie, der Medizintechnik und der Automobilindustrie Anwendung findet. Wie kann man sicher sein, dass die Software automatisch fehlerfrei arbeitet? Auf diese komplexe Frage wird Xavier Rival versuchen, eine Antwort zu finden und sich dabei u. a. auf seine erfolgreichen Forschungsarbeiten an der Ecole Polytechnique / ENS und seinen bemerkenswerten Post-Doktoranden-Aufenthalt in Berkeley stützen. Und die Aufgabe ist umso wichtiger, wenn man bedenkt, dass 99% der Unternehmen ihre Software überprüfen, indem sie die Anwendungen oder einen Teil davon einfach mehrere hundert Male hintereinander testen und dann hoffen, dass das Ergebnis reproduzierbar ist.

„Im Abstraction-Team entwickeln wir Methoden zur automatischen Analyse von Codes, die alle Programmausführungen in einer einzigen Berechnung überprüfen können“, so der Forscher. Diese Analysatoren berechnen also die Proben im mathematischen Sinne. Neben den wirtschaftlichen Vorteilen (die industrielle Software kann dadurch an einem Tag getestet werden) ist das Ergebnis absolut zuverlässig. Dieses besondere Interesse an Softwareverifizierungstools wurde nach der Explosion der Ariane 5, die 1996 aufgrund eines Software-Fehlers abstürzte, geweckt.

Astrée – eine Software zur statischen Programmanalyse, die Programme automatisch auf Laufzeitfehler überprüft – wurde seit 2001 vor diesem Hintergrund entwickelt. Xavier Rival hat seit seiner Dissertation an der Entwicklung mitgewirkt.

In den letzten Jahren wurden erhebliche Fortschritte in diesem Bereich erzielt, insbesondere bei Softwareprogrammen für numerische Berechnungen, wie z.B. die, die von Astrée geprüft werden.

Quelle: Pressemitteilung des INRIA – 20.09.2011 – http://www.inria.fr/centre/paris-rocquencourt/actualites/xavier-rival-verifier-automatiquement-la-surete-des-logiciels-critiques

Redakteur: Charles Collet, charles.collet@diplomatie.gouv.fr – http://www.science-allemagne.fr