Statische Quellcodeanalyse

AbsInt bietet zwei statische Analysatoren zur Prüfung von Codierrichtlinien und zum Erkennen kritischer Programmierfehler auf C-Code Ebene: RuleChecker und Astrée.


Astrée

Astrée ist ein sicherer statischer Analysator zum Nachweis der Abwesenheit von Laufzeitfehlern und weiterer kritischer Programmfehler. Astrée basiert auf abstrakter Interpretation, einer beweisbar korrekten formalen Methode. Werden keine Fehler gemeldet, stellt dies eine Garantie dar, dass es keine Fehler aus den betrachteten Fehlerklassen gibt. Offene Schnittstellen und volle Batchmode-Unterstützung ermöglichen den Einsatz von Astrée in Automatisierungsumgebungen zur kontinuierlichen Verifikation. Toolkopplungen sind verfügbar, z.B. zu dSPACE TargetLink, die eine nahtlose Integration in existierende Entwicklungsumgebungen ermöglichen. Die Konfiguration von OSEK/AUTOSAR-Systemen kann automatisch aus der OIL/ARXML-Spezifikation ermittelt werden. Durch Einsatz des sogenannten Qualification Support Kits und der "Qualification Software Life Cycle Data"-Berichte kann Astrée automatisch nach allen gängigen Sicherheitsnormen (z.B. ISO 26262 oder DO-178B/C) qualifiziert werden.

Astrée meldet Programmfehler durch nach C-Standard (ISO/IEC 9899:1999 (E)) unspezifiziertes und undefiniertes Verhalten, Programmfehler durch inkorrektes nebenläufiges Verhalten, Verletzungen von benutzerspezifizierten Programmierrichtlinien und berechnet Programmeigenschaften, die für die funktionale Sicherheit relevant sind.

Astrée meldet:

• Division durch 0 in ganzzahliger Arithmetik und Gleitkommaarithmetik

• Feldgrenzenverletzungen

• Ungültige Zeigermanipulationen und -zugriffe (NULL-Zeiger, uninitialisierte Zeiger, hängende Zeiger)

• Datenwettläufe (konkurrierende Zugriffe auf dieselbe Speicherzelle durch zwei nebenläufige Threads)

• Inkonsistentes Locking (Lock-/Unlock-Probleme)

• Ungültige Aufrufe von Betriebssystemdiensten (z.B. Aufruf von TerminateTask() für eine OSEK-Task, die nicht-freigegebene Ressourcen hält)

• Überläufe in ganzzahliger Arithmetik und Gleitkommaarithmetik

• Lesezugriffe auf uninitialisierte Variablen

• Unerreichbaren Code

• Verletzungen optionaler benutzerdefinierter Assertions zum Nachweis beliebiger Laufzeiteigenschaften

• nicht-terminierende Schleifen

• Spectre-Verwundbarkeiten (V1, V1.1, SplitSpectre)

Astrée verfügt über ein konfigurierbares Taint-Analyse-Modul, mit dem sich z.B. die Auswirkungen fehlerhafter oder manipulierter Eingabewerte nachvollziehen lassen. Astrée beinhaltet RuleChecker zur Prüfung von Codierrichtlinien und zur Berechnung von Code Metriken (MISRA C:2004, MISRA C:2012, HIS-Metriken, …)



RuleChecker

Sicherheitskritische Software muss nach strengen Codierrichtlinien entwickelt werden, um eine hohe Codequalität sicherzustellen und das Risiko von Programmierfehlern und Sicherheitslücken zu reduzieren.

RuleChecker ist ein statischer Analysator zur Prüfung von Codierrichtlinien und zur Berchnung von Codemtriken für sicherheitskritische C-Programme. RuleChecker ist schnell, leicht zu benutzen und kann automatisiert ausgeführt werden, beispielsweise in Systemen zur kontinuierlichen Integration. Zahlreiche Ergebnisansichten und graphische Visualisierungen ermöglichen eine effiziente Ergebnisauswertung.

RuleChecker unterstützt:

- MISRA C:2004
- MISRA C:2012 incl. Amendment 1
- MISRA C++:2008
- ISO/IEC TS 17961:2013
- SEI CERT Secure C
- MITRE Common Weakness Enumeration (CWE)
- Adaptive Autosar C++ Coding Guidelines.

RuleChecker kann mit dem sicheren statischen Analysator Astrée gekoppelt werden, um unerkannte Fehler auszuschließen und Fehlalarme bzgl. semantischer Regeln zu minimieren.

RuleChecker kann im Batch-Modus ausgeführt werden und in Systemen zur kontinuierlichen Integration verwendet werden. Ein Jenkins-Plugin ist verfügbar.

RuleChecker kann automatisch gemäß aller aktuellen Sicherheitsnormen qualifiziert werden, darunter ISO-26262, DO-178B/C, IEC-61508, EN-50128, usw.