Astrée ist eine Software zur statischen Analyse, die C- und C++-Programme automatisch auf Laufzeitfehler und Regelverletzungen überprüft.
Astrée wird vorrangig zur Analyse von sicherheitskritischen eingebetteten Anwendungen eingesetzt, insbesondere in den Bereichen Luft- und Raumfahrt, Transport, Medizintechnik und Nuklearanlagen. Grundsätzlich kann es aber ganz beliebige Programme analysieren, ob handgeschrieben oder automatisch erzeugt, mit komplexer Speichernutzung, dynamischer Speicherallokation und Rekursion.
Features
- Außerordentlich schnelle und präzise Analysen, darunter:
- Laufzeitfehleranalyse
- Interferenzanalyse
- Taint-Analyse
- Erkennung von Spectre-Verwundbarkeiten
- Signalfluß-, Datenfluß- und Kontrollflußanalyse
- Analyse der Kontrollkopplung und der Komponenteninterferenz
- Benutzerdefinierte Cybersecurity-Analysen
- Analyse von funktionalen Programmeigenschaften
- Regelüberprüfung für MISRA, CERT, CWE, AUTOSAR u. a.
- Analyse von vielfältigen Codemetriken
- Erkennung von totem Code
- Unterstützung für C, C++ und gemischten Code
- Automatisch erzeugte Berichte zur Dokumentation und Zertifizierung
- Qualifizierungskits für DO-178B/C, ISO 26262, EN-50128 und andere Standards
- Ausgereifte Benutzeroberfläche mit graphischen und textuellen Ansichten der Analyseergebnisse und der Benutzerkommentare, des Quellcodes, des Kontrollflusses, uvm.
- Batchmode zur nahtlosen Integration in bestehende Toolchains
- Plugins für TargetLink, Jenkins, μVision, JSON und Eclipse
- Node-locked-, Floating- und Cloud-Betrieb
- Regelmäßige Updates
Wer benutzt Astrée?
Seit 2003 wird Astrée von Airbus France zur Analyse der Flugsteuerungssoftware verschiedener Flugzeugmodelle 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 Reaktorschutz und Reaktorregelung verwendet wird.
Der Automobilzulieferer Helbako setzt Astrée in der Entwicklung von Steuerungssoftware ein, um die Einhaltung von MISRA-Standards und die Abwesenheit von Laufzeitfehlern nachzuweisen.
Anfang 2008 verifizierte Astrée die Abwesenheit von Laufzeitfehlern in der C-Version der Andocksoftware des Weltraumfrachters „Jules Verne“, des ersten automatischen Transferfahrzeugs der ESA. Die Analyse erfolgte vollautomatisch. Am 3. April 2008 dockte der Frachter erfolgreich an der Internationalen Raumstation ISS an.
Ebm-papst, der weltweit führende Hersteller von Elektromotoren und Ventilatoren für Klimaanlagen und Kühlsysteme, setzt Astrée zur fortlaufenden automatischen Verifizierung sicherheitskritischer Kontrollsoftware ein.
MTU Friedrichshafen setzt Astrée zum Beweis der Korrektheit der Kontrollsoftware von Notstromaggregaten in Kraftwerken ein. Zusammen mit dem dazugehörigen Qualifizierungspaket ist Astrée Teil des Zertifizierungsprozesses 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 Laufzeitfehlern in allen möglichen Ausführungsszenarien unter allen möglichen Bedingungen. Dabei meldet es jeden Gebrauch der Sprache, der laut den internationalen ISO/IEC-Normen ein undefiniertes Verhalten aufweist, sowie jeden Verstoß gegen hardwarespezifische Einschränkungen der Implementierung.
Im einzelnen meldet Astrée:
- Division durch Null,
- Feldzugriffe außerhalb der gültigen Feldgrenzen,
- ungültige Zeigermanipulationen und -dereferenzierungen
(
NULL-Zeiger, uninitialisierte und hängende Zeiger), - ganzzahlige arithmetische Überläufe und Gleitkommaüberläufe,
- Lesezugriffe auf uninitialisierte Variablen,
- Datenwettläufe (konkurrierende Lese-/Schreib- oder Schreib-/Schreibzugriffe auf dieselbe Speicherstelle durch zwei Threads ohne passende Mutex-Sperre),
- inkonsistentes Locking,
- ungültige OS-Aufrufe (z. B. ungültige OSEK-Aufrufe von
TerminateTask), - Spectre- und SplitSpectre-Verwundbarkeiten,
- Verstöße gegen optionale benutzerdefinierte Annahmen zur Überprüfung
von sonstigen Laufzeiteigenschaften (ähnlich der „
assert“-Diagnostik), - toten Code.
Gleitkommaberechnungen
werden von Astrée präzise und sicher behandelt. Alle möglichen
Rundungsfehler, sowie alle Kumulativeffekte, 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 sicherheitskritischer eingebetteter Software und weist somit entsprechende Restriktionen auf. Im Astrée-Benutzerhandbuch 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 konfigurierbar, jede Regel und sogar einzelne Aspekte vieler Regeln können individuell hinzugeschaltet werden.
Das Tool berechnet auch vielfältige Code-Metriken (z. B. Comment-Dichte oder zyklomatische Komplexität) und kann um Ihre hauseigenen 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 eigenständiger MISRA-Checker kann dies bieten, und keine Testumgebung kann für die vollständige Daten- und Kontrollflußabdeckung sorgen, die von der statischen Analyse garantiert wird.
Individuell anpassungsfähig
- Dank ausgereifter Annotationsmechanismen können Sie Astrée zusätzliches Wissen zur Verfügung stellen, z. B. um die Ausführungsumgebung zu beschreiben oder die Präzision der Analyse zielgenau für bestimmte Schleifen oder Datenstrukturen zu steuern.
- Dank detaillierter Fehlermeldungen und einer intuitiven Benutzeroberfläche können Sie die Ursache für jeden potentiellen Laufzeitfehler leicht erkennen. Echte Fehler können dann behoben, Fehlalarme durch Kalibrierung minimiert werden. Damit ermöglicht Astrée schnelle und zuverlässige Analysen mit wenigen bis gar keinen Fehlalarmen.
- Der Analysator läuft sowohl im GUI- als auch im Batch-Mode.
- Einfache Integration mit TargetLink, Jenkins und Eclipse wird aktiv unterstützt.
Tool-Qualifizierung
Ihr Einsatz von Astrée kann nach DO-178B/C, ISO 26262, IEC 61508 und anderen Sicherheitsstandards qualifiziert werden. Wir bieten Qualification-Support-Kits an, die den Qualifizierungsprozeß wesentlich vereinfachen und automatisieren.
Der Konkurrenz zehn Jahre voraus
Astrée ist:
sicher
Die meisten Tools auf dem Markt berücksichtigen nicht alle möglichen Laufzeitfehler. Viele melden ganz bewußt nur die wahrscheinlichsten. Diese Tools eignen sich höchstens zum Testen, also zum gelegentlichen Finden einiger Bugs.
Für die Verifikation, also zum Nachweis der Abwesenheit jeglicher Laufzeitfehler, sind solche Bugfinder weder gedacht noch geeignet. Zum Erfüllen der aktuellen Sicherheitsstandards 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 verschweigen. Beides ist absolut unerläßlich zur Verifikation sicherheitskritischer 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 annotieren.
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 (typischerweise 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 industrielle Anwendungen problemlos bewältigen.
Beispielsweise benötigt Astrée zur Analyse von Flugsteuerungssoftware 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 Programmiersprache geschriebenen Anwendungen. Sie können nur in dieser Programmiersprache ausdrückbare Programmeigenschaften berücksichtigen.
Domainspezifische statische Analysatoren schränken die Anwendungsklasse ein, um spezifische Programmstrukturen ausnutzen zu können.
Astrée hingegen ist spezialisierbar und kann an die jeweilige Anwendungsklasse angepaßt werden, um deren spezifische Eigenschaften zu berücksichtigen, was zur Durchführung komplexer Beweise unerläßlich ist. Beispielsweise berücksichtigt Astrée bei Control/Command-Programmen die logischen und funktionalen Eigenschaften der Control-and-Command-Theorie.
parametrisierbar
Bei der statischen Programmanalyse gilt es stets, zwischen Analysepräzision und Rechenaufwand abzuwägen. Sehr präzise Analysatoren sind in aller Regel sehr langsam, sehr schnelle Analysatoren – 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 verwendete Abstraktionsgrad kann individuell an die Struktur Ihres Programms angepaßt werden.
modular
Astrée besteht aus verschiedenen Modulen, den sogenannten abstrakten Domains. Diese Module können so aktiviert und parametrisiert werden, daß anwendungsspezifische Analysatoren entstehen, die vollständig an eine bestimmte Anwendungsklasse oder spezifische Benutzeranforderungen 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 Fehlalarmen zur Anzahl der C-Basisoperationen im analysierten Code liegt typischerweise 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 Operationen bedeutet sie 1000 Fehlalarme.
Im Gegensatz dazu ist Astrée dank seiner Modularität und Anpassungsfähigkeit außerordentlich präzise. Oft ist es sogar in der Lage, mit nur wenigen Zusatzeinstellungen 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 Flugsteuerungssoftware durch Airbus.
aktuell
Astrée wird ständig weiterentwickelt, auch und gerade im Hinblick auf die neuesten Forschungsergebnisse 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 statischen Programmanalyse sind.
Sie finden kein Konkurrenzprodukt, das nicht weit hinterherhinkt. 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.
