SPARK und MISRA-C – Die Vorteile von Sprach-Subsets

Anbieter zum Thema

Axivion GmbH

Parasoft® Deutschland GmbH

RTI Real-Time Innovations

AdaCore

Coding-Standards wie MISRA C sollen auf einfachem Weg für sauberen und sicheren Software-Code sorgen. Doch die Einhaltung einiger der Codierungsregeln ist nicht leicht zu garantieren. Ein Sprach-Subset wie SPARK kann hier Abhilfe schaffen.

MISRA C wurde 1998 als Coding-Standard für C entwickelt und seitdem zweimal überarbeitet; die aktuelle Version ist „MISRA C:2012”. Der Schwerpunkt ist, fehleranfällige Konstrukte der Programmiersprache C zu vermeiden, ohne dabei einen bestimmten Programmierstil zu erzwingen. Eine Studie von Coding Standards für C von Les Hatton, die insgesamt 11 Coding Standards umfasste, fand, dass MISRA-C der einzige Standard ist, der sich ausschließlich auf Fehlervermeidung konzentriert, statt einen bestimmten Stil zu diktieren.

Die Beliebtheit der Programmiersprache C, sowie ihre vielen Fallen und Fehlerquellen, führten zu dem großen Erfolg von MISRA C in Bereichen, wo C für hochkritische Software angewandt wird. Dieser Erfolg führte zu vielen verschiedenen Implementationen von MISRA-C-Checkern. Kriterien der Auswahl sind die Abdeckung der MISRA-C-Regeln, da es unmöglich ist, alle 16 Direktiven und 143 Regeln zu überprüfen.

Insbesondere sind 27 der 143 Regeln gar nicht entscheidbar: Kein automatisches Werkzeug kann alle Verstöße dieser Regeln entdecken, ohne dabei auch Verstöße zu melden, die gar keine Verstöße sind. Ein Beispiel hierfür ist Regel 1.3: „Es soll kein undefiniertes oder kritisches nicht spezifiziertes Verhalten auftreten”. Anhang H von „MISRA C:2012” listet dann hunderte von Fällen von undefiniertem und kritischem nicht spezifizierten Verhalten im Standard der C Programmiersprache, wovon die meisten jeweils unentscheidbar sind. Die meisten MISRA-C-Checker ignorieren unentscheidbare Regeln wie Regel 1.3, und das obwohl Verstöße gegen solche Regeln einen großen Einfluß auf die Software-Qualität haben können.

Für andere Programmiersprachen gibt es aber Technologien, basierend auf statischer Analyse, die diese Aufgabe lösen können, ohne den Benutzer mit Falschmeldungen zu überschwemmen.

Ein Beispiel ist SPARK, entwickelt von AdaCore, Altran und Inria, das auf diesen vier Prinzipien basiert:

• Die zugrunde liegende Programmiersprache Ada bietet ein solides Fundament für statische Analysen durch einen klar definierten Sprachstandard, starke Typisierung und Features zur Software-Spezifikation;

• Das Subset von Ada mit dem Namen SPARK schränkt Ada so ein, dass statische Analysen noch effizienter sind. Dies wird erreicht, indem mehrdeutige Sprachfeatures, wie Seiteneffekte von Funktionen sowie Aliasing, eingeschränkt werden;

• Die statische Analyse von SPARK analysiert jede Funktion unabhängig vom Rest des Codes. So kann eine präzisere Analyse durchgeführt werden, Falschmeldungen werden reduziert; und

• Die statische Analyse von SPARK ist interaktiv. Sie ermöglicht dem Nutzer, die Analyse falls nötig in die richtige Richtung zu lenken, und erzeugt automatisch Gegenbeispiele, wenn Annotationen nicht bewiesen werden können.

SPARK kann inkrementell in einem C-Projekt angewendet werden, wo Schritt für Schritt durch die fünf Level der SPARK Einführung mehr Garantien erhalten werden können, sowie durch hybride Verifikation, die formale Analysen (SPARK) mit traditionellen Testing-Methoden kombiniert.

SPARK Stone Level – Grundlegende Garantien

Das erste Niveau der Einführung von SPARK nennt sich der Stone Level. Dieser Level bedeutet, dass der Code den SPARK-Subset-Regeln entspricht. Schon in diesem Level erhält man einige Vorteile im Code, die in C schwer zu garantieren sind:

• Die Nutzung eines Modulsystems im Gegensatz zu C’s textueller Inklusion von Header-Dateien, die keinerlei Garantien gibt;

• Strenge, gut lesbare Syntax, die Wert auf Klarheit legt und Fallstricke minimiert, im Gegensatz zu C’s sehr freigiebiger Syntax, die es leicht macht, unerwünschte Nebeneffekte in Programmcode zu schreiben;

• Einhaltung der strengen Typisierung von Ada und SPARK, im Gegensatz zu C’s „schlechter Typsicherheit, [die] eine Vielfalt von impliziten Typkonversionen erlaubt, [die] die Sicherheit der Anwendung beeinträchtigen können.” (MISRA C:2012, Annex C).

MISRA C versucht zwar, die entsprechenden Schwächen von C durch eine Reihe von Empfehlungen zu vermeiden. Insbesondere definiert MISRA C stärkere Typregeln („das essentielle Typenmodell”) und schränkt die Verwendung von Funktionsparametern und -resultaten sowie Kontrollstrukturen ein. Diese Regeln vermeiden zwar viele häufige Programmierfehler, sie sind aber absichtlich nicht vollständig, da sonst die meisten C-Programme illegal wären.

Diese grundlegenden Garantien sind in SPARK dank der stärkeren Regeln, die das SPARK-Subset definieren, leicht zu erreichen, durch eine einfache Analyse, wie sie zum Beispiel vom Compiler ausgeführt werden kann. Diese Analyse wird von dem GNATprove genannten Werkzeug ausgeführt, das Teil von SPARK ist.

SPARK Silver Level – Starke Sicherheitsgarantien

Die MISRA-C-Richtlinien versuchen auch subtilere Fehler zu vermeiden: Lesen von nicht initialisierten Daten, Seiteneffekte in Ausdrücken, sowie nicht definiertes Verhalten wie Division durch null und Pufferüberläufe. Alle Diese potentiellen Probleme sind unentscheidbare Probleme, also sind nur wenige MISRA-Checker in der Lage, alle Probleme zu finden.

Beim SPARK Silver Level sind diese Probleme aber völlig ausgeschlossen. Dazu muss der Benutzer sowohl die sogenannte Flow Analysis anwenden (auch Bronze Level genannt), und dann das Fehlen von Laufzeitfehlern beweisen (dann ist der Silver Level erreicht). Um dies zu erreichen, muss der Entwickler in der Regel präzisere Typen definieren, und Verträge zu Funktionen hinzufügen (sogenannte Vorbedingungen, die der aufrufende Code erfüllen muss, und Nachbedingungen, die die Funktion selbst erfüllen muss).

Um den Silver Level zu erreichen, interagiert der Entwickler mit der Entwicklungsumgebung: Der Entwickler startet die Analyse für das ganze Programm oder nur einen Teil, untersucht die GNATprove-Diagnose, modifiziert das Programm (etwa durch das Hinzufügen von neuen Verträgen oder die Modifikation existierender) und wiederholt das Ganze. Diese Interaktion wird durch die detaillierte Information, die GNATprove bei jedem Schritt ausgibt, erleichtert.

Bild 2 zeigt eine Beispielnachricht von GNATprove. Nach der Indikation der genauen Operation, die einen arithmetischen Überlauf provozieren könnte, gibt GNATprove ein Beispiel für Eingabewerte, die zu dem Überlauf führen (hier: der größtmögliche Integerwert, in Ada/SPARK als Integer’Last geschrieben). Der „reason for check” (Grund für die Fehlermeldung) erklärt, dass das Ergebnis der Addition in einen Maschineninteger mit 32-Bit passen muss, was nicht der Fall ist, wenn X schon vor der Addition der größte Integer ist.

Dann schlägt GNATprove vor, eine Vorbedingung zu der Incr-Funktion hinzuzufügen, um zu bestimmen, dass Incr nicht mit X als dem größten Integerwert aufgerufen werden soll (siehe Bild 3). Das ist eine praktische Hilfestellung, da diese Konstrukte meistens übersehen werden und zu sporadischen Fehlern führen können.

SPARK über den Silver Level hinaus

SPARK kann Vorteile bringen, die weit darüber hinausgehen, was ein MISRA-C-Checker kann. Auf den Gold- sowie Platinum-Levels können Entwickler Eigenschaften des Programms durch SPARK Verträge spezifizieren, und dann GNATprove benutzen, um diese Eigenschaften auch zu garantieren. Des weiteren kann vom Programmfluss nicht erreichbarer Code entdeckt werden (ein Ziel, das MISRA C auch zu erreichen versucht).

Im Grunde sind alle Ziele von MISRA C in SPARK einfacher zu erreichen, durch die Kombination von einer besseren Basissprache (Ada) und einem mächtigen Analysetool (GNATprove). Entwickler, die MISRA C einsetzen möchten, können noch höhere Garantien erreichen, indem sie Teile der Anwendung in SPARK entwickeln.

Eine Hilfe für die Einführung von SPARK der Implementation Guidance for the Adoption of SPARK, der direkt bei Adacore bezogen werden kann. Ein detaillierterer Vergleich zwischen SPARK und MISRA C findet sich auf learn.adacore.com.

Formal korrekten C-Code durch Benutzung von SPARK programmieren

Fünf praktische Tipps zum Erlangen der MISRA-Konformität

* Yannick Moy ist R&D Engineer bei AdaCore in Paris.

(ID:46950925)