Dieses Bild hat keinen alternativen Text.
olaser/ iStockphoto

Formale Verifikation für die funktionale Sicherheit

Ob in der Bahn- oder der Automobilindustrie, der Medizin oder in der Luft- oder Raumfahrt: in vielen Anwendungsbereichen gibt es Softwarefunktionen, deren sicherer Betrieb nachgewiesen werden muss, da sonst Menschenleben auf dem Spiel stehen. Wie auch in anderen Bereichen gilt auch in diesen Domänen das konventionelle Testen als vorherrschende Methode für die Qualitätssicherung - für höchste Sicherheitsanforderungen wird aus gutem Grund aber auch der Einsatz formaler Methoden zur Verifikation empfohlen. Die in den genannten Domänen zunehmend komplexer werdenden Systeme stellen allerdings ganz besondere Herausforderungen an beide Verfahren. Das Ziel der formalen Verifikation ist es, mittels mathematisch fundierter Methoden, strenge Aussagen über das korrekte Funktionieren eines Systems zu erhalten. Auch dieser Bereich der Softwarequalitätssicherung ist Teil der Expertise von Fraunhofer FOKUS.

Vorgehen und Ziele der Verifikation

Die Formale Verifikation von Software basiert auf sogenannten Formalen Methoden, einer Kombination aus mathematischer Logik, diskreter Mathematik und formal definierten Sprachen. Der Einsatz formaler Methoden ist durch die Erwartung motiviert, dass die Durchführung geeigneter mathematischer Analysen wie in anderen Ingenieursdisziplinen dazu beiträgt die Korrektheit eines Systems festzustellen. Dies ist auch der große Vorteil im Vergleich zum Testen: Ist die Durchführung der formalen Methode erfolgreich, können definitive Aussage getroffen werden, deren Signifikanz weit über die erfolgreiche Ausführung von Tests hinausgeht. In vielen Fällen kann der Einsatz formaler Methoden die Zertifizierung durch autorisierte Stellen erleichtern.

Normen

In den unterschiedlichen Anwendungsgebieten sind die Anforderungsprofile für Formale Verifikation in Normen festgeschrieben: Für die Software in der Luftfahrt ist die im Januar 2012 erschienene DO-178C maßgeblich. Eine wichtige Erweiterung dieser Norm waren die im Anhang DO-333 veröffentlichten Richtlinien und Hinweise für den Einsatz formaler Methoden. Im Bereich des Zugverkehrs ist die EN 50 128, ebenfalls im Jahr 2012 erschienen, die zentrale Europäische Norm für sicherheitsrelevante Software. Auch in dieser Norm wird festgelegt, welche Verfahren, Prinzipien und Maßnahmen durchgeführt werden müssen, um die zu überprüfende Software als sicher bezeichnen zu können. Die ISO 26262 ist hingegen die Norm für elektrische und elektronische Systeme in Kraftfahrzeugen, in der ebenfalls ein Vorgehensmodell, sowie Methoden für die Entwicklung und Produktion festgelegt werden. 

Herausforderungen

Bei der formalen Verifikation ergeben sich verschiedenartige Herausforderungen, die es zu lösen gilt. Wie bereits erwähnt, gestaltet sich die Übersetzung realer Sachverhalte in formale, mathematische Beschreibungen häufig als schwierig. Des Weiteren stehen bei der Verifikation immer häufiger das Zusammenspiel von Safety (Vermeidung von Schaden) und Security (Vermeidung von Vergehen) im Fokus. Folgendes Szenario soll der Veranschaulichung dienen: Eine Notausgangstür in einem Kinosaal muss stets gewährleisten, dass die Besucher das Kino schnellstmöglich verlassen können. Gleichzeitig muss sie aber verhindern, dass Unbefugte ohne zu bezahlen, von außen in den Saal eindringen können. Die Tür muss dementsprechend von innen zu öffnen sein, von außen jedoch verschlossen bleiben. Auf ähnliche Probleme stößt man vielerorts bei der Softwareentwicklung.

Eine weitere Herausforderung stellt die korrekte Entwicklung der Verifikationssoftware selbst dar. So muss stets verhindert werden, dass eine geprüfte Software trotz Mängel als fehlerfrei gekennzeichnet wird (false-positive). In diesem Fall ist die Verifikation nicht nur falsch, sondern potenziell gefährlich. In korrekt entwickelter Verifikationssoftware treten derartige Fehleinschätzungen deshalb auch nicht auf. Der gegenteilige Fall, in welchem ein Fehler gemeldet wird, obwohl keiner existiert (false-negative) ist zwar weniger kritisch, untergräbt jedoch ebenfalls die Tauglichkeit der Verifikationssoftware.

Formale Methoden 

Heutzutage untergliedert man formale Methoden grob in die folgenden drei Guppen:

1) Deduktive Verifikation:

Diese Methoden involvieren mathematische Argumente und Beweise, um bestimmte Eigenschaften eines formalen Modells zu etablieren. Eine konkrete Anwendung könnte darin bestehen, dass formale Funktionskontrakte zur Beschreibung des erwarteten Verhaltens erstellt werden. Durch eine auf dem Hoare-Kalkül beruhende Analyse der Funktionskontrakte und -implementierungen werden dann mathematische Theoreme generiert. Dabei wird mathematisch-formal beschrieben, wie die Ausführung eines Programmteiles den Zustand der gesamten Berechnung verändert. Idealerweise werden die Beweise dieser Theoreme maschinell mithilfe automatischer Theorem Beweiser durchgeführt. In schwierigen Fällen kommen auch interaktive Beweisassistenten zum Einsatz.

2) Modelüberprüfung

Bei der Modelüberprüfung (engl. model checking) werden alle möglichen Verhaltensweisen eines formalen Modells analysiert, um zu untersuchen, ob eine bestimmte gewünschte Eigenschaft erfüllt wird. Typischerweise kommen hier Spezifikationen mittels temporal-logischer Formeln zum Tragen. Ist dies nicht der Fall, wird eine Begründung dafür ausgegeben, warum das gewünschte Ergebnis nicht erzielt werden konnte.

3) Abstrakte Interpretation

Während beim Testen ein Programm mit konkreten Eingabedaten ausgeführt wird, wird bei der abstrakten Interpretation die Programmausführung statisch analysiert. Zudem beschränkt man sich nicht auf einzelne Eingabedaten, sondern analysiert den Programmzustand für sehr große Datenbereiche durch. Bei dieser abstrakten Ausführung (Interpretation) des Programms wird der Einfachheit halber der Programmzustand in vergröberter Form betrachtet. Diese vergröberte Analyse kann zwar zu ungenauen Ergebnissen führen, die Analyse stellt aber sicher, dass nie kein Fehler berichtet wird, wo in Wirklichkeit einer vorliegt. 

Verfikation bei FOKUS 

Die Wissenschaftler von Fraunhofer FOKUS arbeiten seit Jahren an der Weiterentwicklung und der Praxiseinführung von formalen Verifikationsmethoden.


Device-Soft Deduktive Verifikation für sicherheitskritische Software eingebetteter Systeme

So wurden im DEVICE-SOFT-Projekt deduktive Verifikationsmethoden für die Qualitätssicherung von sicherheitskritischen, eingebetteten Systemen eingesetzt. Dafür wurde die statische Analyseplattform Frama-C von CEA List genutzt. Mathematische Methoden, wie das Hoare-Kalkül werden verwendet, um eine Menge von logischen Regeln zu liefern, die es erlauben, mittels mathematischer Logik Aussagen über die Korrektheit von Computerprogrammen zu liefern. Dabei hat die Erfahrung gezeigt, dass Unit-Beweise bei geringeren Kosten eine höhere Qualität erbringen als Softwaretests. Der Einsatz deduktiver Verfahren erleichtert somit die Zertifizierung sicherheitskritischer Software, da im Gegensatz zum Testen beweisen lässt, dass eine Software für alle möglichen Eingaben spezifikationsgemäß funktioniert.


Vessedia

In sicherheitskritischen Branchen werden hohe Investitionssummen in langwierige Verifikationsprozesse gesteckt. Mit dem Internet der Dinge (IoT) hat sich der Branchenfokus hin zu kurzen Entwicklungszyklen und möglichst niedrigen Kosten verlagert. Dies führt zu einem Konflikt zwischen den früheren Verifikationsmethoden und den Anforderungen der neuen Branchen, wodurch eine umfassende Prüfung der Safety und Security im Bereich des IoT erschwert wird.

Im Vessedia-Projekt, das seit September 2017 läuft, werden die Einsatzmöglichkeiten von Softwareanalyse-Werkzeugen erweitert, um diese in hochdynamischen Systemen mit weniger kritischen Anwendungen flexibler und kurzfristiger einsetzbar gemacht zu werden. Zusätzlich werden die entwickelten Analyseverfahren geringere Kosten verursachen. Die Arbeit im Projekt findet sowohl auf der Grundlagenebene als auch in der praktischen Anwendung der Ergebnisse statt. Die Hauptziele sind demnach:

  • die Entwicklung einer Methodik, um Werkzeuge zur Softwareanalyse wirksam einzusetzen,
  • die Standardisierung von Werkzeugen zur statischen Analyse, um deren Einsatzmöglichkeiten zu erweitern,
  • der Nachweis der verbesserten Analysemethoden auf dem für die Entwicklung von IoT-Anwendungen weit verbreiteten Betriebssystem Contiki OS,
  • die Entwicklung eines »Security Certification Levels« (SCL) für IoT-Anwendungen, für die eine Common Criteria-Zertifizierung zu kostenintensiv ist.

Fraunhofer FOKUS ist im Vessedia-Projekt federführend für den Bereich Methoden verantwortlich. Die Wissenschaftler beschäftigen sich auch mit der Qualitätssicherung der eingesetzten Analyse-Werkzeuge. Zusätzlich wird an Ansätzen geforscht, um statische Analysen mithilfe des Frama-C Werkzeugs schneller Cloud-basiert durchführen zu können. Außerdem werden Leitlinien für eine kosteneffiziente Kombination von statischer Analyse und Testen für IoT-Anwendungen erarbeitet.