Formal korrekten C-Code durch Benutzung von SPARK programmieren

Ein einfacher Weg zu sicherer Software: Durch den Einsatz der Ada-Variante SPARK ist es möglich, schnell und unkompliziert in C geschriebene Programme automatisch auf Korrektheit zu überprüfen.

Anbieter zum Thema

MicroConsult Microelectronics Consulting & Training GmbH

Parasoft® Deutschland GmbH

AdaCore

Das Schreiben von Software für Applikationen wird noch größtenteils von Menschen gemacht. Menschen machen aber Fehler, in den meisten Fällen eher ungewollte und nicht bewusste. Die Statistik zeigt, das bei 1.000 LOC (Lines of Code) ungefähr 10-15 Fehler auftreten. Wenn wir jetzt uns eine sicherheitsrelevante Anwendung mit ~800.000 Zeilen Code vorstellen, dann können wir annehmen das 8.000 bis 15.000 Fehler darin enthalten sind. Daher braucht die Entwicklung von sicherheitsrelevanten Anwendungen Wege um die Anzahl der Fehler drastisch zu reduzieren.

Formelle Methoden als generelle Stütze beim Programmieren

Formelle Methoden können hier helfen. Aber das gilt nicht nur für sicherheitsrelevante Anwendungen, es gilt auch für Software in unserem alltäglichen Leben. Wie oft werden Benutzer mit schlecht geschriebener Software konfrontiert? Abstürze oder nicht korrekt implementierte Funktionalität sind an der Tagesordnung. Der Benutzer wird zum Beta-Tester. Der Einsatz von formellen Methoden sollte daher auch auf die „alltäglichen“ Anwendungen übertragen werden um die Qualität der Software zu erhöhen.

Bildergalerie

Bildergalerie mit 9 Bildern

Aber schauen wir erst einmal welche Möglichkeiten im Moment zur Verfügung stehen um die Anzahl der Fehler in der Software zu reduzieren.

Möglichkeiten bei der Fehlersuche und ihre Einschränkungen

Ein weit verbreiteter Ansatz ist die Verwendung von Coding Standards, die jeder Entwickler berücksichtigen muss. MISRA-C ist ein populäres Beispiel. Die Sprachen C und C++ haben viele Möglichkeiten uneindeutig zu sein und Richtlinien helfen hier die mögliche Anzahl von Fehler zu reduzieren. Es macht den Code außerdem besser lesbar für Andere. Im Markt sind Werkzeuge verfügbar die Programmierern helfen diese Standards anzuwenden.

Aber MISRA-C und auch andere Standards helfen nicht Fehler in der Software zu finden. Sie beschränken die Sprachen nur und helfen syntaktische Fehler und uneindeutige Anwendung von Konstrukten zu vermeiden. Selbst wenn die Regeln für einen Standard angewendet werden und syntaktisch korrekter Code vorhanden sind, heißt es noch nicht, dass dieser funktional korrekt arbeitet [7].

Ein weiterer Weg ist die Erhöhung der Anzahl von Tests. Mehr ausgeführte Tests sollten mehr Fehler zum Vorschein bringen, theoretisch. Das Problem bei diesem Ansatz ist, das die Tests meist ausgelegt sind um das richtige Verhalten zu testen. Moderne Entwicklungsprozesse legen sogar fest, das Test noch vor der Entwicklung der Anwendung geschrieben werden müssen. Das zeigt das Problem auf, denn die Tests werden so geschrieben, dass sie das richtige Verhalten der Anwendung wieder spiegeln und sind nicht dafür ausgelegt versteckte Fehler im Programm zu finden.

Daher heißt mehr Testen nicht unbedingt das alle Fehler gefunden werden. Tests helfen mehr Fehler zu finden, wen diese während der Testphase auftreten. Verschiedene Werkzeuge sind verfügbar, die durch Analyse des Softwarecodes helfen, die notwendigen Test zu finden. Aber die Benutzung der Werkzeuge und die Ausführung der Test verbraucht mehr Zeit im Entwicklungsprozess [6].

Ein weiterer Ansatz könnte die Erhöhung der Anzahl von Reviews sein. Dies erhöht die Möglichkeit das Fehler gefunden werden, ist aber immer noch keine Garantie. Da die Arbeit des Reviews von Menschen ausgeführt wird, sind wir wieder beim ersten Problem, Menschen machen Fehler. Reviews sind also nicht die perfekte Lösung. Es erhöht außerdem den Aufwand und verbraucht mehr Arbeitszeit von Mitarbeitern im Entwicklungsprozess. Reviews machen außerdem nur Sinn wenn die Menge des Codes der angeschaut wird klein ist. Wenn sich die Menge des Codes erhöht oder der Code komplex ist, erhöht sich die Wahrscheinlichkeit das Probleme übersehen werden.

Der nächste mögliche Ansatz ist die Verwendung von statischen Analysewerkzeugen. Das ist ein Schritt in die richtige Richtung und wird als unerlässlich von Herrn Holzmann in seinen zehn Regeln [1] für die Entwicklung von sicherheitsrelevanten System vorgeschrieben. Aber statische Analysewerkzeuge werden keinen funktionalen Fehler im Code finden.

Als Beispiel hierfür können wir eine Funktion betrachten, die Daten in aufsteigender Ordnung sortieren soll, dies aber in absteigender Ordnung macht [8]. Diese Art von Fehler werden statische Analysewerkzeuge nicht finden. In den letzten Jahren ist viel Aufwand betrieben worden um die Qualität der Algorithmen in den Analysewerkzeugen zu verbessern und die Anzahl der „False-Positive“ Meldungen zu reduzieren. „False-Positive“ sind Fehler die die Werkzeuge anzeigen, aber in wirklich sind es gar keine Fehler [8]. Dies hat dazu geführt das statische Code-Analysewerkzeuge sehr nützlich und hilfreich sind. Es hinterlässt aber immer noch die Lücke funktionelle Fehler zu finden.

Eine Kombination aller vorher genannten Methoden ist die Zertifizierung. Für unterschiedliche Industriebereiche gibt es verschieden Prozeduren die befolgt werden müssen und dann von einer Zertifizierungsbehörde abgenommen werden. DO178 oder EN 50128 sind Beispiele hier. Für ISO 26262 gibt es keine offizielle Zertifizierungsbehörde, trotzdem ist sie ein Schritt in die richtige Richtung. Zertifizierung garantiert einen hohen Standard, dass alle Schritte richtig ausgeführt wurden und die Anzahl der Fehler auf ein Minimum beschränkt wurde. Es ist aber immer noch keine Garantie für die totale Abwesenheit von Fehlern.

Ein anderer Weg zum Auffinden von Fehler kann die Verwendung von formellen Methoden sein. Diese sind eine Erweiterung der statischen Analysemethoden, aber mit einer anderen Absicht. Statische Analysemethoden werden verwendet um Fehler in der Software zu finden, formelle Methoden werden verwendet, um vom Anfang an fehlerfreie Software zu entwickeln.

Der Unterschied für den investierten Aufwand zwischen einem Test basierten Ansatz und einem Ansatz der formelle Methoden verwendet kann in Bild 1 gesehen werden. Die rot gestrichelte Linie zeigt die Kosten für das Finden von Fehler in der Software über den Zeitraum eines Entwicklungsprojektes, die durchgezogenen Linien zeigen auf wann wie viele Fehler gefunden werden. In späten Phasen des Entwicklungsprozesses steigen die Kosten für das Beseitigen von Fehler erheblich an, im Vergleich zum Finden der Fehler in früheren Phasen. In traditionellen Entwicklungsprozessen mit einem testbasierten Ansatz ist genau dass der Fall. Die Probleme werden in der Test und der Integrationsphase gefunden und erzeugen so mehr Kosten je später sie entdeckt werden. Dies hat zu Kostenexplosionen in Projekten, Reduktion von geplanten Funktionalitäten oder sogar zum totalen Scheitern von Projekten geführt. Mit der Verwendung von formellen Methoden kann das Auffinden von Fehler in frühere Entwicklungsphasen verlegt werden und somit die Kosten signifikant senken. Es findet ein sogenanntes Frontloading statt. Dies wird auf der rechten Seite von Bild 1 mit der grünen, nicht gestrichelten Linie dargestellt.

FRAMA-C als eine mögliche formelle Methode

Es gibt zwei Wege, formelle Methoden anzuwenden. Auf der einen Seite gibt es den Ansatz von FRAMA-C [2]. Wie der Name schon sagt, dieser Ansatz arbeitet mit der Programmiersprache C. FRAMA-C stellt eine Plattform da, die mit mehreren verschiedenen Werkzeugen den Code formell überprüfen kann. Diese Werkzeuge werden Prover genannt.

Um dieses aber den Werkzeugen zu ermöglichen muss der C-Code mit zusätzlichen Kommentaren versehen werden, die den Provern erklären wie der Code funktionieren soll. Dies stellt zusätzlichen Aufwand für die Entwickler dar. Es bedeutet auch, dass eine zusätzliche Sprache gelernt werden muss, den die Kommentare müssen in ACSL (ANSI/ISO C Specification Language) [9] geschrieben werden. Dieser Ansatz hat Erfolge aufgezeigt. Er verlängert aber auch die Entwicklungszeit, weil zusätzlicher Aufwand betrieben werden muss und mehr Zeit für das Schreiben des Programms aufgewendet wird, durch das Einfügen der notwendigen Kommentare.

Alternative Methode mit SPARK

Anstatt zwei Sprachen zu kombinieren gibt es einen effizienteren Ansatz, der alle notwendigen Konstrukte in einer Sprache enthält. Dieser Ansatz wird mit SPARK [11] verfolgt. Die Unterschiede zwischen FRAMA-C und SPARK können in Bild 2 gesehen werden. SPARK ist kein Weg um Fehler zu finden, sondern ein Weg die volle Fehlerfreiheit in der Software zu garantieren. Die Mathematik dahinter ist mit der von FRAMA-C vergleichbar und es können die gleichen Prover eingesetzt werden. Nur der Ansatz unterscheidet sich. FRAMA-C arbeitet mit Annotationen in der Form von Kommentaren, SPARK ist eine Untergruppe der Programmiersprache Ada und enthält alle notwendigen Annotationen in der Sprache selber. Wie von dem Experiment von Christophe Garion und Jérôme Hugues gesehen werden kann, erfordert die schwächere Semantik von C doppelt so viele Annotationen und bedeutet daher doppelt so viel Arbeit [2]. Die beiden haben die komplette Fehlerfreiheit in C und SPARK Laufzeitbibliotheken für AADL überprüft, unter der Verwendung von FRAMA-C für die C Version der Bibliothek und SPARK für die ADA Variante, unter Verwendung des Werkzeuges GNATprove. SPARK ist also ein mit weniger Aufwand versehender Ansatz als FRAMA-C, weil der Programmierer in der gleichen Sprache arbeiteten kann, in der er den Code und die Bedingungen zur Überprüfung der korrekten Funktionsweise schreibt.

Ein Hindernis bei der Benutzung von SPARK ist allerdings die Voraussetzung eines Ada 2012 Compilers für die verwendete Hardware. Auch wenn es sehr gute Unterstützung für viele Plattformen gibt, so ist es doch weniger wahrscheinlich einen Ada 2012 Compiler für exotische Plattformen zu finden. Es ist hier wahrscheinlicher einen ISO kompatiblen C-Compiler zur Verfügung zu haben. Aber in dem Fall, dass es keinen Ada Compiler für eine Plattform gibt, ist es trotzdem möglich die Vorteile von SPARK zu benutzen.

(ID:45474853)