ELITE NETZWERK BAYERN

English  Sprachen Icon  |  Gebärdensprache  |  Leichte Sprache  |  Kontakt


Forschungsarbeit

Von Raketen und Mars-Robotern:  
Fehlerfreier Code durch mehrstufige Programmanalyse

Von Jan Michael Auer (08.06.2016)

4. Juni 1996, Space Center Guyanais in Französisch-Guayana. Die Ariane5-Rakete V88 startet zum Erstflug ihrer Serie. Nach 37 Sekunden stellt sich die Rakete quer und sprengt sich selbst. Als Ursache werden mehrere Software- und Entwicklungsfehler gefunden. Ein Überlauf einer Variablen geht als einer der teuersten Softwarefehler in die Geschichte ein. Der heutige Stand der Forschung versucht solche Fehler zum Großteil zu vermeiden. Die zwei komplementären Technologien der statischen Code-Analyse und der Laufzeit-Verifikation können jeweils für sich eine bestimmte Klasse an Programmfehlern erkennen und vor potentiellen Auswirkungen warnen. „Statische Laufzeit-Verifikation“ soll nun eine Brücke zwischen beiden Technologien liefern.

Programmierer schreiben Quelltexte in einer oder mehreren Programmiersprachen. Diese Sprachen setzen sich – analog zur deutschen Sprache – aus einem Alphabet mit Wörtern zusammen, die eine bestimmte semantische Bedeutung tragen. Auch in der Informatik gibt es dabei Rechtschreib-, Grammatik- und semantische Fehler: So wie ein vergessenes Satzzeichen die Bedeutung mancher Sätze radikal ändert, kann ein falscher Operator ein Computerprogramm unausführbar machen. Viele dieser Fehler lassen sich heutzutage durch Überprüfungsroutinen bereits während der Entwicklung vermeiden – ähnlich zu Rechtschreib- und Grammatikprüfungen in gängigen Textverarbeitungsprogrammen.

Statische Code-Analyse funktioniert ähnlich solcher Prüfprogramme. Der Quelltext wird schrittweise unterschiedlichen formalen Prüfungen unterzogen, die jeweils nach einer bestimmten Art von Fehlern suchen. Das können zum Beispiel Typumwandlungen von Variablen und Divisionen durch Null sein oder globale Speicherprobleme. Ausgeführt wird das Programm dazu nicht. Stattdessen bedient sich die Statische Code-Analyse Techniken wie der abstrakten Interpretation oder formalen Verifikation. Bei komplexen Programmen erreichen diese jedoch ihre Grenzen. Die vielen potentiellen Ausführungspfade und Eingabemöglichkeiten führen zu einer sogenannten Zustandsexplosion.

Die Laufzeit-Verifikation hingegen überwacht das Programm während seiner Ausführung. Sie überprüft daher nur die auftretenden Eingabedaten und Programmpfade. So kann die Komplexität des Softwaretestens erfolgreich gestrafft werden. Das Problem der Zustandsexplosion tritt in diesem Fall nicht mehr auf. Die Information über Fehlerzustände zur Laufzeit ist hilfreich für eine sichere Ausführung kritischer Systeme. Das Programm erhält dadurch die Chance, auf den Fehler zu reagieren oder ihn überhaupt zu vermeiden. Laufzeit-Verifikation trägt zum Beispiel zur Überwachung von Mars-Missionen der NASA bei. Formale Korrektheit in allen Ausführungspfaden gewährleistet sie durch diese selektive Sicht jedoch nicht.

Bisweilen wurden diese Technologien nur für sich betrachtet. Nun soll eine formale Verbindung der beiden – die sogenannte „Statische Laufzeit-Verifikation“ – Synergieeffekte zwischen den Ansätzen heben und so ein neues Qualitätslevel unter den Software-Testverfahren erreichen.

Abb. 1[Bildunterschrift / Subline]: Abb. 1: Der Ablauf der „Statischen Laufzeit-Verifikation“. Ausgehend von einer formalen Fehlerspezifikation wird der Quelltext eines Programms untersucht, instrumentiert und während der Ausführung überwacht.

Die neue Analyse umfasst drei Stufen: Identifikation, Instrumentierung und Überwachung. Zuerst wird mittels statischer Code-Analyse der Quelltext auf Fehlerkandidaten untersucht und diese markiert. Durch die Unschärfe dieser Analyse befinden sich unter den Kandidaten auch „Fehlalarme“. Anschließend werden an diesen Stellen Überwachungswerkzeuge installiert. So wie in einem Stromkreis beispielsweise ein Spannungsmessgerät eingebracht wird, kontrolliert man hier die Veränderungen einer Variablen oder wie oft eine bestimmte Routine durchlaufen wird. Diese „Ereignis-Instrumentierung“ findet mittels Umformungen im Quelltext oder direkt in der kompilierten Maschinensprache statt. Zuletzt überwachen Monitore die erstellten „Instrumente“, während das Programm läuft. Tritt ein Fehler auf, melden sie ihn an das Programm oder protokollieren ihn.

Die experimentelle Durchführung solcher Testverfahren wurde mit „Goanna“, einem modernen Tool für statische Analyse, und der LLVM-Compiler-Infrastruktur für die Instrumentierung realisiert. Formeln in erweiterter linearer Temporallogik (LTL) spezifizieren außerdem die korrekte Programmausführung und werden automatisch in Zustandsmaschinen zur Überwachung übersetzt. In einer ersten Evaluation erzielt dieses Verfahren Fehlererkennungsraten von über 85% für die unterstützten Fehlerkategorien. Pro instrumentiertem Ereignis waren dazu zusätzlich 3µs an Rechenzeit notwendig.

Abb. 2[Bildunterschrift / Subline]: Abb. 2: Eine Hierarchie an automatisch generierten Zustandsmaschinen, die das Programm zur Laufzeit auf Fehler überwachen. Wird ein ungültiger Zustand erreicht, kann das Programm wiederhergestellt oder sicher beendet werden.

Es zeigen sich viele Anwendungsfälle für Statische Laufzeit-Verifikation, bei denen die Überwachungsperformance steigt und auf automatisiertem Wege mehr Fehler während Entwicklung, Testung und Produktivbetrieb gefunden werden. Einerseits muss das Programm dank der zusätzlichen statischen Analyse an weniger Stellen instrumentiert werden, was den Einfluss auf das Laufzeitverhalten dementsprechend verringert. Andererseits verhilft das Verfahren während der Entwicklung zu höheren Erkennungsraten. Das senkt die Kosten der Fehlerbehebung drastisch: Laut Standish-Report können Fehler während der Entwicklung sogar mit einem Zehntel der Kosten behoben werden, die sonst in einem Produktivsystem anfallen würden.


Jan Michael Auer
* 1993

Wissenschaftlicher Werdegang
  • 2013
  • Bachelor of Science in Software Engineering, FH Hagenberg, Österreich
  • 2014-2015
  • Forschungsassistent, Oracle Corporation, Belmont (CA), USA
  • 2015
  • Forschungsassistent, National ICT Australia, Sydney, Australien
  • Master with honours in Software Engineering, Universität Augsburg, Deutschland