AbsInt Angewandte Informatik GmbH

Nie wieder Stacküberlauf.

StackAnalyzer bestimmt automatisch den maximalen Stackverbrauch von eingebetteten Anwendungen für jeden Programmpunkt. Diese Information ist von entscheidender Bedeutung für die Speicherdimensionierung von eingebetteten Systemen. Die Analyseergebnisse werden im Aufruf- und Kontrollflußgraphen anschaulich dargestellt.

Features
 

• Ausführliche und genaue Angaben zum User-Stack und System-Stack.
• Stackanalyse auf allen Hierarchie-Ebenen: Prozeduren, Basisblöcke, Assembler-Instruktionen.
• Frei wählbare Startpunkte für die Analyse.
• Kritische Programmteile werden farblich hervorgehoben (siehe Screenshots).

Warum brauchen Sie StackAnalyzer?

Der Bedarf an freien Stackzellen muß vom Entwickler im voraus festgelegt werden. Wird der Bedarf unterschätzt, führt das zu gravierenden Laufzeitfehlern wegen Stacküberlaufs („stack overflow“). Die genaue Fehlerquelle ist dann oft schwer zu finden. Überschätzt man hingegen den Stackbedarf, um „auf der sicheren Seite“ zu sein, so verschwendet man kostbaren Speicher.

• StackAnalyzer berechnet automatisch und exakt den Stackbedarf Ihrer Software.
• StackAnalyzer reduziert den Entwicklungsaufwand und hilft, Laufzeitfehler wegen Stacküberlaufs zu vermeiden.
• Die Analyse spiegelt vorgenommene Programmänderungen und/oder -optimierungen unmittelbar wider.

CompCert ist ein formal verifizierter optimierender C-Compiler. Sein Einsatzbereich liegt in der Compilierung sicherheitskritischer C-Software, die hohen Zuverlässigkeitsanforderungen genügen muss. CompCert akzeptiert ISO C99 Programme und produziert Maschinencode für PowerPC (32-bit/64-bit hybrid), ARM, IA32 (x86 32-bit), AMD64 (x86 64-bit) und RISC-V.
 
Was ist das besondere an CompCert?
CompCert wurde durch maschinenunterstützte mathematische Beweise als korrekt bewiesen. Der Beweis zeigt, dass der vom Compiler produzierte Maschinencode dasselbe Verhalten aufweist, wie es die Semantik des C-Quellprogramms vorgibt. CompCert ist der erste kommerziell erhältliche formal verifizierte Compiler und bietet einen bislang unerreichten Vertrauensgrad in die Korrektheit des Übersetzungsprozesses.
 
Der formale Beweis deckt alle Transformationen vom abstrakten Syntaxbaum bis zum erzeugten Assembly-Code ab. Zum Präprozessieren und zur Erzeugung von Objektdateien und ausführbaren Dateien, werden externe Präprozessoren, Assembler, Linker und C-Bibliotheken verwendet. Diese Phasen sind somit unverifiziert, aber technisch wenig anspruchsvoll und aus Implementierungssicht robust, so dass sie gut durch traditionelle Qualifizierungskits abgedeckt werden können.
 
Die hohe Zuverlässigkeit von CompCert konnten schon anhand einer Entwicklungsversion von CompCert im Jahre 2011 in einer Studie von Regehr, Yang et al. nachgewiesen werden: “The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.”
 
Vorteile von CompCert:
* Kosten zum Aufspüren und Umgehen oder Beheben von Compilerfehlern und Auslieferung von Patches an die Endkunden des eingebetteten Systems können vermieden werden.
* Der Testaufwand zum Nachweis, dass bereits auf höheren Ebenen überprüfte Eigenschaften auch auf Maschinencode-Ebene gelten, kann reduziert werden, da dies automatisch aus dem Korrektheitsbeweis von CompCert folgt.
* In Bereichen, in denen bislang aus Sicherheitsgründen Compileroptimierungen ganz oder teilweise abgeschaltet wurden, können erstmals Compileroptimierungen eingesetzt werden.
* Auf typischen eingebetteten Prozessoren läuft der von CompCert generierte Code doppelt so schnell wie von GCC ohne Optimierungen erzeugter Code, und er ist nur 20% langsamer als GCC bei Optimierungsstufe 3. (Details über den verwendeten Benchmark-Mix, der diesen Zahlen zugrunde liegt, sind auf Nachfrage erhältlich.)

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.

Damit ein Echtzeitsystem stets korrekt funktioniert, muss sichergestellt werden, dass alle Tasks innerhalb von fest vorgegebenen Zeiten beendet werden. Dazu muss die längstmögliche Ausführungszeit der Tasks (engl. worst-case execution time, oder kurz WCET) bestimmt werden. AbsInt liefert drei Softwarewerkzeuge zur WCET-Analyse, die auf unterschiedliche Anwendungsszenarien zugeschnitten sind. Alle drei unterstützen Batch-Mode Ausführung und können in Systemen zur kontinuierlichen Integration eingesetzt werden.

aiT WCET Analyzer - Statische Laufzeitgarantien

aiT berechnet durch statische Analyse präzise obere Schranken der längstmöglichen Ausführungszeit von Tasks für zeitvorhersagbare Single- und Multicore-Prozessoren. aiT analysiert direkt ausführbare Binärdateien und berücksichtigt das Cache- und Pipeline-Verhalten des Zielprozessors.

aiT basiert auf der Technik der Abstrakten Interpretation, einer formalen Methode für semantik-basierte statische Analyse, die Soundness-Beweise ermöglicht: Es gibt keine Programmausführung, bei der die berechnete Laufzeitschranke überschritten wird.

Eine graphische Benutzeroberfläche visualisiert den kritischen Programmpfad und ermöglicht unter anderem die interaktive Untersuchung aller Cache- und Pipelinezustände an beliebigen Programmpunkten.

aiT ist für eine Vielzahl von Mikroprozessoren verfügbar, von einfachen Prozessoren wie dem Infineon C16x bis hin zu komplexen superskalaren Prozessoren wie Freescale MPC755, MPC7448 und Multicore-Prozessoren wie Freescale MPC5777M und Infineon AURIX TC27x.

TimeWeaver - Nicht-invasive Hybride WCET-Analyse

TimeWeaver kombiniert statische Pfadanalyse mit Echtzeit-Tracing auf Instruktionsebene zur Berechnungen von Abschätzungen der längstmöglichen Ausführungszeit. TimeWeaver unterstützt viele moderne Hochleistungsprozessoren, z.B. alle PowerPC Boards mit Nexus Program Trace Messages (IEEE-ISTO 5001, Class 2 und höher) oder ARM mit zyklengenauen ETM-Traces.

TimeWeaver analysiert alle möglichen Programmpfade und berechnet den längsten Pfad basierend auf den Ausführungszeiten von Trace-Segmenten der ermittelten Echtzeit-Traces. Die Trace-Information beinhaltet Interferenz-Effekte, z.B. durch Zugriffe auf gemeinsam genutzte Ressourcen von verschiedenen Cores, und wird nicht durch Probe Effects verzerrt, da keine Code-Instrumentierung benötigt wird. Die berechneten Zeitschranken erfüllen Anforderungen von Sicherheitsnormen wie der ISO-26262.

Die Analyseergebnisse beinhalten die berechnete Laufzeitschranke mit dem zeitkritischen Pfad sowie Informationen über die erreichte Trace-Abdeckung. Sie liefern einen wertvollen Beitrag zum Nachweis der Systemsicherheit, zur Optimierung der Trace-Abdeckung und zur Optimierung der Worst-Case Performance.

TimingProfiler - Abschätzung der längstmöglichen Ausführungszeit in frühen Entwicklungsphasen

TimingProfiler hilft Entwicklern beim Aufspüren von Programmteilen mit unzufriedenstellenden Ausführungszeiten und dient zur entwicklungsbegleitenden Überwachung des Timingverhaltens, insbesondere bei modellbasierter Entwicklung. TimingProfiler kann eingesetzt werden, sobald ausführbarer Code vorliegt – also bereits sehr früh in der Entwicklung, wenn Messungen an der Hardware zu kostspielig oder unmöglich sind. Die Analyse ist rein statisch. Weder Zugriff auf die physikalische Hardware noch Code-Instrumentierung werden benötigt.

TimingProfiler liest ausführbaren Binärcode und simuliert die Ausführung jeder einzelnen Task auf einer generischen Prozessorarchitektur mit einem vorgegebenen Instruktionssatz, z. B. PowerPC. Alle möglichen Ausführungspfade werden erforscht und der Worst-Case-Pfad für die Ausführungszeit identifiziert. Benutzerinteraktion ist nicht erforderlich. Das Analyseergebnis ist ein realistisches Worst-Case-Szenario, wenngleich keine Garantie, wie sie aiT bietet.

Engpässe und Schwachstellen können sehr früh in der Entwicklung erkannt und somit typische Integrationsprobleme in späteren Phasen vermieden werden.