Schnelle und sichere statische Analyse

Astrée ist eine Software zur statischen Analyse, die C- und C++-Programme automatisch auf Lauf­zeit­fehler und Regel­verletzungen überprüft.

Astrée-Screenshot
Astrée-Screenshot

Astrée wird vorrangig zur Analyse von sicherheits­kritischen ein­gebetteten Anwendungen eingesetzt, insbe­sondere in den Be­reichen Luft- und Raumfahrt, Transport, Medizin­technik und Nuklear­anlagen. Grundsätzlich kann es aber ganz beliebige Programme analysieren, ob handgeschrieben oder automatisch erzeugt, mit komplexer Speicher­nutzung, dyna­mischer Speicher­allokation und Rekursion.

Features

Wer benutzt Astrée?

Seit 2003 wird Astrée von Airbus France zur Analyse der Flug­steuerungs­software verschiedener Flugzeug­modelle eingesetzt, darunter des A380.

Die Bosch Automotive Steering (vormals ZF Lenksysteme) ersetzte 2018 ihre alte Software durch Astrée und RuleChecker und profitiert seitdem von den viel schnelleren Analysen, der deutlich höheren Zuverlässigkeit und den wesentlich geringeren Support-Kosten.

Framatome setzt Astrée zur Verifikation sicherheitskritischer Software ihrer Leittechnik-Systemplattform TELEPERM XS ein, welche u. a. für Reaktor­schutz und Reaktor­regelung verwendet wird.

Der Automobilzulieferer Helbako setzt Astrée in der Entwicklung von Steuerungs­software ein, um die Einhaltung von MISRA-Standards und die Abwesenheit von Laufzeitfehlern nachzuweisen.

ESA logo

Anfang 2008 verifizierte Astrée die Ab­we­senheit von Laufzeitfehlern in der C-Version der Andocksoftware des Welt­raumfrachters „Jules Verne“, des ersten automati­schen Transferfahrzeugs der ESA. Die Ana­lyse er­folgte vollautomatisch. Am 3. April 2008 dockte der Frachter erfolgreich an der Inter­nationalen Raumstation ISS an.

Ebm-papst, der weltweit führende Hersteller von Elektromotoren und Venti­latoren für Klima­anlagen und Kühl­systeme, setzt Astrée zur fort­laufenden automa­tischen Verifi­zierung sicher­heits­kritischer Kontroll­software ein.

MTU Friedrichshafen setzt Astrée zum Beweis der Korrekt­heit der Kontroll­software von Notstrom­aggregaten in Kraft­werken ein. Zusammen mit dem dazu­gehörigen Qualifizierungspaket ist Astrée Teil des Zerti­fizie­rungs­prozesses nach IEC 60880.

Welche Laufzeiteigenschaften überprüft Astrée?

Astrée überprüft durch statische Analyse, ob die C- bzw. C++-Sprache korrekt eingesetzt wurde, und sucht nach Laufzeit­fehlern in allen möglichen Ausführungs­szenarien unter allen möglichen Bedingungen. Dabei meldet es jeden Gebrauch der Sprache, der laut den inter­natio­nalen ISO/IEC-Normen ein undefiniertes Verhalten aufweist, sowie jeden Verstoß gegen hardware­spezifische Einschrän­kungen der Imple­mentierung.

Im einzelnen meldet Astrée:

Gleitkommaberechnungen werden von Astrée präzise und sicher behandelt. Alle möglichen Run­dungsfehler, sowie alle Kumulativ­effekte, werden stets berücksichtigt. Gleiches gilt für die Werte −∞, +∞ und NaN in allen Berechnungen und Vergleichen.

Jetzt auch für C++ und gemischten Code

Seit 2020 kann die Analyse auch auf C++-Code angewendet werden, sowie auf gemischten C- und C++-Code. Unterstützt werden alle modernen Varianten der C++-Sprache, einschließlich C++17.

Die C++-Analyse basiert auf derselben Technologie wie die C-Analyse, richtet sich also nach wie vor in erster Linie an Entwickler sicher­heits­kritischer eingebetteter Software und weist somit entsprechende Restriktionen auf. Im Astrée-Benutzer­handbuch finden Sie dazu weitere Details und Empfehlungen.

MISRA und mehr

Mit dem nahtlos integrierten RuleChecker können Sie Ihre Software auf die Einhaltung von MISRA-, CWE-, ISO/IEC-, SEI-CERT und AUTOSAR-Regeln überprüfen. Die Checks sind frei kon­figurierbar, jede Regel und sogar einzelne Aspekte vieler Regeln können individuell hinzu­geschaltet werden.

Das Tool berechnet auch vielfältige Code-Metriken (z. B. Comment-Dichte oder zyklomatische Komplexität) und kann um Ihre haus­eigenen Regeln erweitert werden.

Benutzt man RuleChecker in Verbund mit Astrées sicherer semantischer Analyse, kann man False-Negatives garantiert ausschließen, und False-Positives für semantische Regeln auf ein Minimum reduzieren. Kein eigen­ständiger MISRA-Checker kann dies bieten, und keine Testumgebung kann für die vollständige Daten- und Kontroll­flußabdeckung sorgen, die von der statischen Analyse garantiert wird.

Individuell anpassungsfähig

Tool-Qualifizierung

Ihr Einsatz von Astrée kann nach DO-178B/C, ISO 26262, IEC 61508 und anderen Sicherheits­standards qualifiziert werden. Wir bieten Qualification-Support-Kits an, die den Qualifizierungsprozeß wesentlich ver­einfachen und automatisieren.

Der Konkurrenz zehn Jahre voraus

Astrée ist:

  • sicher

    Die meisten Tools auf dem Markt berück­sichtigen nicht alle möglichen Laufzeit­fehler. Viele melden ganz bewußt nur die wahr­scheinlichsten. Diese Tools eignen sich höchstens zum Testen, also zum gelegent­lichen Finden einiger Bugs.

    Für die Verifikation, also zum Nachweis der Abwesenheit jeglicher Lauf­zeitfehler, sind solche Bugfinder weder gedacht noch geeignet. Zum Erfül­len der aktuellen Sicherheits­standards wie ISO 26262, DO-178B/C, IEC-61508 oder EN-50128 reicht das gelegentliche Finden einiger Bugs nicht.

    Astrée-Analysen sind hingegen sicher. Das Tool berücksichtigt stets alle möglichen Laufzeitfehler, und wird niemals einen davon ver­schwei­gen. Beides ist absolut unerläßlich zur Verifi­kation sicherheits­kritischer Software. Zugleich ist Astrée in der Lage, nur wenige bis gar keine Fehlalarme zu produzieren.

  • automatisch

    Für manche Analysatoren – z. B. solche, die sich auf Computerbeweise verlassen – müssen Sie Ihre Programme mit vielen Induktionsinvarianten anno­tieren.

    Astrée verlangt in aller Regel nur sehr wenige Annotationen. Bestimmte Arten von Programmen kann es sogar vollautomatisch untersuchen, ohne jede Hilfestellung vom Benutzer.

  • schnell

    Andere statische Analysatoren benötigen sehr viel Zeit (typischer­weise mehrere Stunden zum Analysieren von 10 000 Codezeilen) oder verbrauchen extrem viel Speicher. Manche terminieren erst nach Tagen mit einem Speicherüberlauf. Manche terminieren gar nicht.

    Im Gegensatz dazu ist Astrée äußerst effizient und kann große in­dustrielle Anwendungen problemlos bewältigen.

    Beispielsweise benö­tigt Astrée zur Analyse von Flug­steuerungs­software mit 132 000 Zeilen C-Code selbst auf einem Single-Core-2,8-GHz-PC lediglich 80 Minuten. Schnellere Rechner liefern entsprechend schnellere Ergebnisse. Multicore-Hardware und verteilte Verarbeitung werden unterstützt.

  • anpassungsfähig

    Universelle statische Analysatoren unterstützen alle in der jeweiligen Programmier­sprache geschrie­benen Anwendungen. Sie können nur in dieser Programmier­sprache ausdrückbare Programm­eigenschaften be­rücksichtigen.

    Domain­spezifische statische Analysatoren schränken die Anwendungs­klasse ein, um spezifische Programm­strukturen aus­nutzen zu können.

    Astrée hingegen ist spezialisierbar und kann an die jeweilige Anwendungs­klasse angepaßt werden, um deren spezifische Eigen­schaften zu berück­sichtigen, was zur Durch­führung komplexer Beweise unerläßlich ist. Beispiels­weise berück­sichtigt Astrée bei Control/Command-Programmen die logischen und funktionalen Eigen­schaften der Control-and-Command-Theorie.

  • parametrisierbar

    Bei der statischen Programmanalyse gilt es stets, zwischen Analyse­präzision und Rechenaufwand abzu­wägen. Sehr präzise Analysatoren sind in aller Regel sehr langsam, sehr schnelle Analy­satoren – sehr ungenau.

    Astrée hingegen ist parametrisierbar – die Feinabstimmung von Prä­zision und Rechenaufwand kann von Ihnen frei gewählt werden. Der für die Analyse ver­wendete Abstraktions­grad kann indivi­duell an die Struktur Ihres Programms ange­paßt werden.

  • modular

    Astrée besteht aus verschiedenen Modulen, den sogenannten abstrak­ten Domains. Diese Module können so akti­viert und parametri­siert wer­den, daß anwendungs­spezifische Analysatoren entstehen, die voll­stän­dig an eine be­stimmte Anwendungs­klasse oder spezi­fische Be­nutzer­anforderungen angepaßt sind.

    Zur besseren Unterstützung spezifischer Anwendungsklassen kann Astrée durch die Einführung zusätzlicher Module erweitert werden, die die Präzision der Analyse noch weiter erhöhen.

  • Präzise

    Universal-Analysatoren erlauben nur sehr geringe Präzision im Hinblick auf Fehlalarme. Das Verhältnis von Fehl­alarmen zur Anzahl der C-Basisoperationen im analy­sier­ten Code liegt typischer­weise bei 10–20 %.

    Spezialisierte Analysatoren erreichen bessere Zahlen, 10 % oder weniger. Leider ist im Produktionseinsatz auf industriellen Anwendungen selbst eine Rate von nur 1 % vollkommen inakzeptabel: bei 100 000 Ope­ratio­nen bedeutet sie 1000 Fehlalarme.

    Im Gegensatz dazu ist Astrée dank seiner Modularität und Anpassungs­fähigkeit außerordentlich präzise. Oft ist es sogar in der Lage, mit nur wenigen Zusatz­einstellungen oder von sich aus genau null Fehlalarme zu erzeugen. Dies wurde immer wieder von der Industrie unter Beweis gestellt, z. B. bei der Analyse primärer Flugsteuerungs­software durch Airbus.

  • aktuell

    Astrée wird ständig weiterentwickelt, auch und gerade im Hinblick auf die neuesten Forschungs­ergebnisse in der theoretischen Informatik. Wir profitieren seit Jahrzehnten von engster Zusammenarbeit mit Forschungsgruppen in Deutschland, Frankreich und Schweden, die weltweit führend auf dem Gebiet der stati­schen Programm­analyse sind.

    Sie finden kein Konkurrenzprodukt, das nicht weit hinterher­hinkt. Viele sind ganz stehengeblieben, oder nehmen seit Jahren nur noch kosmetische Änderungen vor.

    Wir veröffentlichen alle sechs Monate ein Produktupdate. Jeder Kunde, egal mit welcher Lizenz, bekommt mindestens ein Update völlig kostenlos und automatisch zugeschickt. Und unsere Kundenbetreuung hört sich Ihre Wünsche und Verbesserungsvorschläge nicht bloß an, sondern sorgt auch dafür, daß sie umgesetzt werden.


Jetzt testen

Testen Sie Astrée kostenlos an Ihrem eigenen Code.