Laufzeitfehler in Embedded-Software finden Die statische Software-Analyse

Was für Atheisten lediglich eine intellektuelle Herausforderung darstellt, ist für Entwickler sicherheitskritischer Software Pflicht: Der Beweis, dass etwas nicht existiert. Das ist nicht unmöglich, wie gerne angenommen wird, erfordert jedoch einigen logischen Aufwand. Im Falle von Laufzeitfehlern in Embedded-Software übernimmt diesen ein Programm zur statischen Analyse.

Bei der Validierung bestimmter Programmeigenschaften in der Luftfahrt-, Automobil- und Medizintechnikindustrie sind statische Analysatoren auf Basis der abstrakten Interpretation zunehmend Stand der Technik. Beispiele hierfür sind der Nachweis der längstmöglichen Ausführungszeit und des maximalen Stackverbrauchs von Tasks [1], die Bestimmung der Genauigkeit von Gleitkommaberechnungen und der Ausschluss des Auftretens von Laufzeitfehlern.

Ein Grund für diesen Erfolg statischer Analysetechniken liegt darin, dass sie auf einer sicheren Überapproximation der konkreten Programmsemantik basieren. Was bedeutet dies nun für eine statische Laufzeitfehleranalyse? Eine sichere statische Laufzeitfehleranalyse kann für eine Anweisung x nur zwei Ergebnisse produzieren: entweder »x wird niemals zu einem Fehler führen« oder »x könnte einen Fehler verursachen«. Im ersten Fall ist die Fehlerfreiheit garantiert, im zweiten Fall liegt entweder ein Fehler vor, oder es handelt sich um einen Fehlalarm. Diese Unschärfe ermöglicht es statischen Analysatoren, selbst für große Softwareprojekte innerhalb akzeptabler Zeit ein Ergebnis zu berechnen. Die Analyseergebnisse sind trotzdem verlässlich, da sich ein wohldefinierter Analysator nur auf der sicheren Seite irren kann: Wenn die Analyse keinen Fehler findet, ist der Nachweis der Fehlerfreiheit geführt und die Abdeckung liegt bei 100%. Die Technik der abstrakten Interpretation ermöglicht es hierbei, die Wohldefiniertheit der Analysen formal zu beweisen; die entsprechenden Beweise wurden für das Analysewerkzeug »Astrée« publiziert (siehe [2]).

Alarm! Fehlalarm!

Treten Fehlermeldungen auf, so ist für jede Meldung genau zu überprüfen, ob es sich um einen echten Fehler handelt. Lässt sich nachweisen, dass es sich bei allen Meldungen um Fehlalarme handelt, ist der Beweis der Abwesenheit von Laufzeitfehlern geführt. Die Prüfung, ob es sich bei allen Meldungen um Fehlalarme handelt, kann manuell durchgeführt werden. Dies ist jedoch fehleranfällig und zeitaufwändig, zumal es komplexe Abhängigkeiten zwischen den Alarmen geben kann. Die Zahl der Fehlalarme beeinflusst daher die Anwendbarkeit eines statischen Analysators wesentlich. Gelingt es dem Analysator, das Ziel von »null Fehlalarmen« zu erreichen, ist der Nachweis der Abwesenheit von Laufzeitfehlern automatisch geführt.

Es stellen sich somit zwei zentrale Anforderungen an einen Analysator: Da jede Fehlermeldung überprüft werden muss, ist es wichtig, dass der Analysator präzise ist, also nur wenige Fehlalarme produziert. Des Weiteren muss der Analysator so parametrisierbar sein, dass Benutzer eine Feinabstimmung der Analyse für das zu analysierende Programm unter Berücksichtigung externer Zusatzinformationen vornehmen können. Nur auf diese Weise lässt sich das Ziel »null Fehlalarme« erreichen.

Das Analysewerkzeug Astrée (siehe Kasten »Astrée vs. Laufzeitfehler«) wurde gezielt mit Blick auf diese Anforderungen zum Nachweis der Abwesenheit von Laufzeitfehlern in C-Programmen nach ISO/IEC9899:1999 (E) (C99-Standard) entwickelt. Akzeptiert werden strukturierte C-Programme mit komplexem Speicherverhalten, jedoch ohne dynamische Speicherallokation oder unbeschränkte Rekursionen. Hierzu zählen viele eingebettete Steuerungsprogramme im Bereich der Kernenergie, Medizintechnik, Automobilelektronik, sowie Luft- und Raumfahrt. Gemeldete Fehlersituationen sind: Verletzung von Feldgrenzen, ganzzahlige Division durch Null, Überläufe und ungültige Operationen auf Gleitkommazahlen (die zu den IEEE-Werten »Inf« und »NaN« führen), Wrap-arounds bei ganzzahliger Arithmetik (meist im Fall von Überläufen), Typkonversionen, die zu Wrap-arounds führen (wenn der Zieltyp zu klein für den Wert ist), und Verletzungen benutzerdefinierter C-Assertions im Programm.

Außerdem kann Astrée unerreichbaren Code anzeigen und vor möglicherweise nicht terminierendem Code warnen. Aufgrund einer großen Anzahl effizienter Analysedomains erzielt Astrée eine hohe Analysepräzision und erzeugt nur wenige Fehlalarme [5]. So erfasst beispielsweise die »Oktagon«-Domain Relationen zwischen Variablen der Form x±y<=const, Gleitkommaberechnungen modelliert die Software unter Berücksichtigung von Rundungsfehlern präzise, sie erkennt digitale Filter und approximiert diese möglichst genau.

Parametrisierung

Durch Aktivierung der für einen bestimmten Anwendungsbereich relevanten Analysedomains lässt sich Astrée für eine bestimmte Programmfamilie spezialisieren; auch neue, abstrakte Domains lassen sich einbinden. In einem weiteren Schritt kann der Benutzer Astrée durch gezielte Parametrisierung an ein bestimmtes Programm aus der jeweiligen Programmklasse anpassen. Zum einen sind dies Annotationen beziehungsweise Optionen, mit denen sich die abstrakte Domain parametrisieren lässt und die Präzision der Analyse für bestimmte Programmkonstrukte beeinflusst werden kann. So kann der Benutzer beispielsweise individuell die Präzision der Analyse von Schleifen oder Arrays kontrollieren.

Damit kann er kritische Programmteile mit einer höheren Präzision analysieren als unkritische und somit Effizienz gewinnen. Zum anderen gibt es spezielle Annotationen zur Bereitstellung externer Informationen an Astrée, etwa durch Angabe von Wertebereichen für volatile Variablen. Diese Annotationen machen alle externen Annahmen explizit, die für eine korrekte Programmausführung erfüllt sein müssen. Ein weiteres wichtiges Entwicklungsziel von Astrée war die Nachvollziehbarkeit der Alarme, also der gemeldeten potenziellen Laufzeitfehler. Durch eine detaillierte Angaben über die Ursache eines Alarms (siehe Bild 1) sowie eine interaktive Exploration der berechneten Wertebereiche von Variablen kann der Benutzer die Analyseergebnisse genau nachvollziehen. Somit kann er potenzielle Laufzeitfehler korrigieren beziehungsweise die Parametrisierung anpassen, um Fehlalarme zu vermeiden.

Die Erfahrung zeigt, dass diese Parametrisierung sehr stabil ist und während der Weiterentwicklung der zu analysierenden Software nur selten geändert werden muss. Praktische Erfahrungen mit industriellen Softwareprojekten aus dem Luft- und Raumfahrtbereich belegen, dass sich mit Astrée nicht nur Laufzeitfehler finden lassen, sondern sich auch deren Abwesenheit nachweisen lässt. In [6] wird ein Beispielprojekt aus dem Luftfahrtbereich näher beschrieben: Es besteht aus 200 000 Zeilen präprozessierten C-Codes, führt viele Gleitkommaberechnungen aus und beinhaltet digitale Filter. Die Analysedauer für das Gesamtprogramm beträgt auf einem 2,6-GHz-PC mit 16 GByte RAM etwa sechs Stunden. Der erste Analyselauf ergab 467 Alarme; die Zahl der Alarme konnte auf Null reduziert werden.(mc)