Formale Testmethoden: Reif für den Mainstream

31.01.2019Autor / Redakteur: Benjamin M. Brosgol und Yannick Moy * / Sebastian Gerstl |

Gerade in kritischen Systemen ist es essentiell, dass deren Software alle Funktionalitäten korrekt implementiert und keine Fehler enthält. Formelle Methoden lösen dabei traditionelle Tests mehr und mehr ab.

Anbieter zum Thema

MicroConsult Microelectronics Consulting & Training GmbH

Parasoft® Deutschland GmbH

RTI Real-Time Innovations

AdaCore

Nach wie vor ist Test das Mittel der Wahl für die Verifikation von Software, aber es ist bekannt, dass der Test außer in den einfachsten Fällen nicht alle Situationen testen kann. Automatische statische Analysen können die relevanten Programmeigenschaften mathematisch beweisen.
(Bild: gemeinfrei / CC0 )

In der Geschichte der Informatik war die Disziplin der formalen Methoden lange Zeit auf die Forschung beschränkt. Aber in den letzten zehn Jahren hat sich die Situation verändert. Dank technologischer Fortschritte sind die formalen Methoden in den Mainstream gerückt, insbesondere für hochsichere und hochkritische Systeme. Projekte können formale Methoden auf diversen Niveaus einführen, mit variierenden Kosten und Nutzen, zusätzlich oder manchmal an Stelle des Tests. In letzter Zeit wurden formale Methoden eingesetzt, um in Projekten wie sicheren USB-Sticks oder im Militärbereich extreme Anforderungen an die Sicherheit und Zuverlässigkeit zu erfüllen.

Eine formale Methode ist eine Technik, um den Quellcode eines Programms statisch zu analysieren und dabei bestimmte Eigenschaften des Programms zu beweisen. Seit dem Anfang der Programmierung waren solche Methoden Gegenstand der Forschung, denn der Vorteil gegenüber dem Test liegt auf der Hand: Verifikation des Programms für alle möglichen Eingaben und Situationen, statt nur einer begrenzten Menge, und dadurch mögliche Kostenreduktionen in der Wartung der Software.

In der Vergangenheit hatten solche Methoden jedoch gewisse Nachteile, die die Industrie davon abhielten, sie einzusetzen: die Analyse dauerte zu lange und skalierte nicht für größere Programme, die erlaubten Sprachelemente waren zu restriktiv, der Einsatz der Werkzeuge benötigte spezielle Kenntnisse, die Balance zwischen der Korrektheit des Werkzeugs (alle Fehler eines bestimmten Typs im Programm finden) und der Präzision (möglichst wenige falsche Meldungen) war nicht gut, sowie allgemein die Schwierigkeit, neue Methoden in den Entwicklungsprozess einzuführen.

Fortschritte in diversen Bereichen haben diese Nachteile mittlerweile wesentlich verringert. Bessere Technologien, bessere Hardware (insbesondere Prozessoren mit mehreren Kernen) und bessere und ausdrucksstärkere Sprachen und Tools machen formale Methoden nun auch in der Praxis anwendbar. Diese neueren Tools sind auch leicht zu lernen – die Entwickler brauchen keine Spezialkenntnisse über die Beweissysteme – und formale Methoden können auch Schritt für Schritt in ein Projekt eingeführt werden, je nach den Eigenschaften, die bewiesen werden sollen.

Formale Methoden einsetzen, am Beispiel von SPARK

Eine formale Methode die den erwähnten Fortschritt verdeutlicht ist die Programmiersprache SPARK und die dazugehörigen Werkzeuge. SPARK ist eine Teilmenge der Programmiersprache Ada und stützt sich dabei auf die Features der vertragsbasierten Programmierung (eingeführt in Ada 2012), insbesondere die Vor- und Nachbedingungen. Ein Beispiel von SPARK Quellcode ist in Bild 1 näher erläutert.

SPARK kann auf unterschiedliche Weise eingesetzt werden, je nachdem wie kritisch die Software ist und welche Eigenschaften bewiesen werden sollen. In der Reihenfolge der Vorteile eines SPARK-Beweises (aber auch des Aufwands) gibt es die folgenden Stufen:

„Stone“: das Programm gehört zur SPARK-Teilmenge

„Bronze“: Alle Daten sind korrekt initialisiert; auch der Datenfluss wird überprüft

„Silver“: Laufzeitfehler können ausgeschlossen werden

„Gold“: Schlüsseleigenschaften des Programms können bewiesen werden

„Platinum“: volle funktionale Korrektheit des Programms kann bewiesen werden.

Das „Stone“ Niveau ist ein Zwischenschritt zur Einführung der formalen Methode und stellt sicher, dass die nächsten Schritte angewendet werden können. Bronze sollte für den Großteil des Codes verwendet werden, da die dadurch garantierten Eigenschaften durch den Test schwer überprüft werden können.

Für kritische Module wird das Silver-Niveau empfohlen. Es stellt sicher, dass der Code keine gefährlichen Fehler wie „Pufferüberlauf“ oder arithmetischen Überlauf enthält. Auf dem höchsten Sicherheitslevel kann schließlich auch Gold oder Platinum eingesetzt werden.

Beispiel eines SPARK Programms: Der „Global“ Vertrag spezifiziert, dass die Implementation von „Insert“ die Variable „T“ sowohl lesen als auch schreiben wird. Die „Pre“ Vorbedingung muss bei jedem Aufruf von „Insert“ erfüllt werden: „T“ soll nicht voll sein und soll nicht bereits den einzufügenden Wert enthalten. Die „Post“ Nachbedingung ist die Eigenschaft die „Insert“ selbst garantiert: der as „Item“ überreichte Parameter ist dann in „T“ enthalten. Die SPARK Werkzeuge können dazu verwendet werden, diese Verträge zu überprüfen: dass T wie spezifiziert in „Insert“ benutzt wird (und keine anderen globalen Variablen), dass alle Aufrufe von „Insert“ die Vorbedingung erfüllen, und dass „Insert“ seine Nachbedingung erfüllt.
(Bild: Adacore)

Beim Einsatz von formalen Methoden gibt es eine Situation, die im Test nicht auftritt: was soll geschehen, wenn das Werkzeug eine Eigenschaft nicht beweisen kann, also eine Fehlermeldung ausgibt? Das Problem kann ein echter Bug sein, entweder direkt im Quellcode, oder in den spezifizierten Verträgen. In diesem Fall hat das Werkzeug ein Problem gefunden, das nun zeitig korrigiert werden kann, bevor große Kosten durch den Fehler entstehen. Es kann aber auch sein, dass diese Meldung eine „falsche Meldung“ ist, dass also der Code und die Verträge richtig sind, das Werkzeug dies aber nicht beweisen kann. Hier kann Erfahrung mit dem Werkzeug helfen, und bestimmte Heuristiken (zum Beispiel Schleifeninvarianten) eingesetzt werden.

Bei der formalen Methode SPARK gilt kein „Alles oder nichts“. Sie kann mit normalem Test kombiniert werden, wo zum Beispiel der formale Beweis nur auf einen Teil des Codes angewendet wird, in der Regel auf den kritischsten Teil. Dabei kann der restliche Code in Ada, C oder auch anderen Sprachen sein, die Fähigkeiten von Ada und SPARK zur Erstellung von Schnittstellen erlauben Anwendungen mit mehreren Programmier- sprachen.

Erfahrungen mit SPARK in der Verifikation

Mehrere aktuelle Projekte zeigen wie formale Methoden im allgemeinen, und SPARK im Besonderen, im Mainstream der Verifikation ankommen.

Sicherer USB-Stick: Die französische Behörde zur Informationssicherheit ANSSI hat SPARK für das größte Modul im Mikrokernel des quelloffenen, STM32-basierten USB-Sticks WooKey verwendet. WooKey erlaubt Verschlüsselung und Schutz der Daten, sowie andere Sicherheitsmechanismen, und wurde als Antwort auf die „BadUSB“ Sicherheitslücke entwickelt, die USB-Geräte in Angriffsvektoren verwandeln kann. Das Projekt hat formale Methoden mit dem Ersatz von Modulen in C durch Ada und SPARK eingefügt und konnte das „Silver“-Niveau erreichen (Ausschluss von Laufzeitfehlern).

Aerospace Software: Thales, weltweiter Anbieter von Produkten in der Luftfahrt, Eisenbahn, Verteidigung sowie im Sicherheitsbereich, hat mit AdaCore an mehreren Pilotprojekten zusammengearbeitet um die Kosten und Vorteile von formalen Methoden je nach Level einschätzen zu können. Die dabei gelernten Erfahrungen wurden in einer Broschüre Implementation Guidance for the Adoption of SPARK dokumentiert (Broschüre nur auf Englisch verfügbar). In einem der Pilotprojekte im Verteidigungsbereich wurde eine gewünschte Eigenschaft des Codes (Gold-Niveau) als Automat in 7000 Codezeilen ausgedrückt. Dabei konnte von zwei Entwicklern mit Hilfe eines SPARK-Experten der Silver-Level in einem Tag, der Gold-Level in weiteren vier Tagen erreicht werden.

Traditionelle Methoden allein reichen heute nicht mehr aus

Da auch in kritischen Systemen immer mehr Software eingesetzt wird, wird es immer wichtiger, zu überprüfen, dass die Software die beabsichtigte Funktionalität korrekt implementiert und keine Fehler oder Sicherheitslücken enthält, die die Sicherheit gefährden können. Traditionelle Verifikationstechniken, die in der Vergangenheit ausreichend waren, sind es heutzutage nicht mehr, und müssen durch gründlichere Methoden ergänzt werden.

Formale Methoden können diese Rolle übernehmen. Sie sind nicht länger auf den Einsatz in Forschungsbereichen beschränkt, sondern sind praktikabel, erlernbar und effektiv, und finden heutzutage bereits in der Industrie Anwendung.