Verifikation von Embedded Software durch Integration von Test und Beweis

Mit formalen Methoden lässt sich mathematisch die Sicherheit eines Systems nachweisen. Klassisches Testing überprüft, ob geschriebener Code den Anforderungen genügt. Warum nicht beides anwenden?

Anbieter zum Thema

Parasoft® Deutschland GmbH

RTI Real-Time Innovations

AdaCore

Die wohl kniffligste Aufgabe für einen Embedded-Softwareentwickler ist, nachzuweisen, dass ein System die Anforderungen erfüllt - auch „negative“ Anforderungen, wie die Abwesenheit von Laufzeitfehlern, Sicherheitsrisiken oder Security-Schwachstellen - wobei Vertrauen in direktem Bezug zur Kritikalität der Software steht. Im Laufe der Jahre wurden zahlreiche Verifikationsmethoden entwickelt, darunter auch Kombinationen aus manuellen Reviews, automatischer (statischer) Analyse und Tests.

Typische Kombination aus Review, Analyse und Testing

Diese Methoden basieren auf folgendem Grundprinzip: Jedem Softwaremodul wird ein Vertrag (Contract) zugeordnet, der dessen Anforderungen definiert. Der Code muss diesen Vertrag erfüllen. Der Vertrag kann z.B. Architekturaspekte beinhalten, die die Datenabhängigkeiten und -beziehungen des Moduls definieren, oder auch Funktionalitätsaspekte, die das Modulverhalten bestimmen. Für ein Subprogramm (Codemodul) enthalten sie eine Vor- und Nachbedingung. Die Vorbedingung ist der Programmzustand des Subprogramms bei dessen Aufruf; die Nachbedingung ist der Programmzustand, den es garantiert, bevor es zurückkehrt. Bei der Verifikation des Funktionsvertrags eines Subprogramms ist nachzuweisen, dass bei jedem Aufruf des Subprogramms dessen Vorbedingung erfüllt wird.

Darüber hinaus ist der Nachweis erforderlich, dass das Subprogramm keine Laufzeitfehler enthält (impliziter Vertrag) und dass bei seiner Rückgabe die Nachbedingung erfüllt wird.

Solche Anforderungen/Verträge werden bisher entweder informell (in natürlicher Sprache) oder in einer entsprechenden Notation unabhängig von der jeweils verwendeten Programmiersprache spezifiziert. Die Verifikation der Verträge erfolgt durch statische Analyse oder (besonders bei Funktionsverträgen) mithilfe von Tests, wobei die beiden Methoden keinen klaren Bezug zueinander haben oder kein Übergang vorgesehen ist (z.B. um bei bestimmten Prüfungen Tests durch statische Analyse zu ersetzen bzw. zu ergänzen). Der Verifikationsprozess beinhaltet also verschiedene Methoden, die lose integriert sind und unterschiedliche Vertrauensgrade liefern, je nachdem, wie umfassend die Tests sind, welche Möglichkeiten (bzw. Einschränkungen) das statische Analyseverfahren hat, und ob die statische Analyse korrekt ist (d.h. ob sie zuverlässig erkennt, wenn Eigenschaften nicht erfüllt werden, die sicherzustellen bzw. zu überprüfen sind).

Umsetzung in der Programmiersprache Ada

Diese Themen lassen sich mit der Sprache SPARK/Ada bzw. dem entsprechenden Toolset adressieren. Ada ist eine stark typisierte Universal-Programmiersprache, die sich in vielen Bereichen des Software Engineering und bei der Entwicklung hochzuverlässiger Embedded-Software seit langem bewährt hat. Mit der neuesten Version Ada 2012 wurde ein Standardprozedere für Verträge eingeführt (Vor- und Nachbedingungen) - mit Laufzeitsemantik: Wenn ein Vertrag nicht eingehalten wird, löst dies einen Laufzeitfehler (Exception) aus.

SPARK ist eine formal analysierbare Teilmenge von Ada mit Einschränkungen, die den Beweis von Programmeigenschaften basierend auf Verträgen im Quellcode ermöglichen. SPARK wird durch eine Toolsuite zur statischen Analyse beim Nachweis von Eigenschaften unterstützt - von korrektem Daten-/Informationsfluss und der Abwesenheit von Laufzeitfehlern bis hin zur Einhaltung formal spezifizierter Anforderungen. Verträge, die in Ada zur Laufzeit verifiziert werden (mithilfe von Tests), lassen sich in SPARK anhand von Beweismethoden statisch verifizieren.

Bild 1 zeigt eine Inkrementprozedur in SPARK. Das SPARK Proof-Tool kann alle Verträge dieses Beispiels verifizieren und die Abwesenheit von Laufzeitfehlern während der Ausführung des Increment-Body sicherstellen.

Vorteile der Implementierung in SPARK/Ada

Die SPARK/Ada-Sprachtechnologie basiert auf einer vertragsbasierten Programmierung, die sowohl die statische als auch dynamische Verifikation unterstützt und zahlreiche Vorteile bietet:

• In frühen Entwicklungsphasen lassen sich Verträge mithilfe von Tests verifizieren; im Laufe der weiteren Systementwicklung können kritische Module statisch verifiziert werden.

• Die Einführung formaler Methoden ist nicht “in Stein gemeißelt“: Ein Ada-System lässt sich je nach Sicherheitsanforderungen auf verschiedenen Stufen für SPARK anpassen. Bei hochsicheren Komponenten ist es unerlässlich, die Abwesenheit von Laufzeitfehlern nachzuweisen und sicherzustellen, dass das System nicht durch Fehler wie beispielsweise Pufferüberlauf beeinträchtigt wird.

• Innerhalb einer Applikation lassen sich Komponenten mit unterschiedlichen Sicherheitsanforderungen mit verschiedenen Methoden verifizieren; die relevanten Prüfungen finden dabei an den Schnittstellen statt.Dies bietet zwei Vorteile: Eine formal verifizierte Komponente kann ein getestetes Subprogramm aufrufen (z.B. ein Low-Level-Programm, das vielleicht in Ada, einer Assemblersprache oder C programmiert ist), mit formaler Verifikation, dass die Vorbedingung des Programms erfüllt ist. Eine getestete Komponente wiederum kann ein formal verifiziertes Subprogramm aufrufen. Beim Aufrufenden wäre anhand von Tests das erforderliche Vertrauen zu schaffen, dass die Vorbedingung erfüllt ist.

• Die Ergänzung DO-333 Formale Methoden zur Norm DO-178C für in der Luftfahrt verwendete Software beschreibt, dass sich mithilfe beweisbasierter Verifikation das Testerfordernis für Systeme, die einer Zertifizierung unterliegen, reduzieren lässt.

• Ada unterstützt die Embedded-Systemprogrammierung und bietet z.B. die Möglichkeit, Interrupt-Handler in Ada zu programmieren und eine eingeschränkte und deterministische Teilmenge der Task-Funktionen zu verwenden (sog. Ravenscar Profil). Auch SPARK bietet diese Unterstützung und ermöglicht so die formale Verifikation von Low-Level-Modulen oder -Code mit nebenläufiger Programmierung.

Ob für die Verifikation Tests oder formale Methoden verwendet werden, ist keine Entweder-oder-Entscheidung. Die Technologien ergänzen einander, und Erfahrungen in realen Luftfahrtanwendungen haben gezeigt, dass die Integration beweisbasierter Methoden mit herkömmlichen Testverfahren sinnvoll und kosteneffizient ist. Mit Ada und SPARK lassen sich beide Methoden in der Entwicklung hochsicherer Embedded-Software zielführend einsetzen. Der Verifikationsaufwand sinkt und das Vertrauen, dass die Eigenschaften sicherheitskritischer Programme eingehalten werden, steigt.

Übersetzung: Sabine Pagler

* Benjamin M. Brosgol ist Senior Software Engineer bei AdaCore in Boston.

(ID:45583525)