In den meisten Anwendungsbereichen ist es möglich, mit Software, die noch ein paar Restfehler enthält, zu leben, so lange die Fehler in der normalen Benutzung nicht zu einer Störung führen. Für hochzuverlässige und sicherheitsrelevante Software kann es eine solche Toleranz nicht geben.
Bei der Herstellung von Software mit herkömmlichen Methoden ist es praktisch unvermeidlich, daß Fehler beim Entwurf oder der Kodierung auftreten. Normalerweise versucht man, durch Testen der fertiggestellten Software oder von Softwareteilen Fehler zu lokalisieren und anschließend zu korrigieren.
Tests können nur Fehler nachweisen
Mit dem iterativen Verfahren des Testens ist, auch unter Zugrundelegung eines methodischen Ansatzes, in der Praxis nur ein begrenzter Grad an Fehlerfreiheit nachweisbar, da sich ein vollständiger Test beziehungsweise eine vollständige Funktionsüberprüfung komplexer Programme nicht durchführen läßt.
Eine bekannte Tatsache ist, daß durch die Anwendung von Test-Methoden zwar das Vorhandensein von Fehlern in den geprüften Programmpfaden, nicht aber die Fehlerfreiheit nachgewiesen werden kann. Die Sicherheit und Zuverlässigkeit der Software muß nicht nur bei den üblichen Betriebsbedingungen, sondern auch in Ausnahmesituationen gewährleistet sein. Deshalb müssen, um ein komplexes Softwaresystem daraufhin zu überprüfen, ob zum Beispiel alle möglichen Eingaben zu dem vorgeschriebenen Ergebnis führen, andere Methoden eingesetzt werden.
Als Alternative zum Testen gibt es formale Methoden, die ihre Grundlage in der mathematischen Logik haben. Der Bedarf für solche formalen Methoden wurde erst in den späten sechziger Jahren geweckt, als große Computerhersteller erkannten, daß Software-Entwicklungskosten jene für die Hardware weit übertrafen. Sie sprachen - und sprechen immer noch - von einer "Software-Krise". Trotz erheblicher Fortschritte bei den Software-Entwicklungsmethoden wurde die Kluft zwischen Kosten für sichere Hardware und Kosten für sichere Software größer.
Als Ausweg wurde schon vor Jahren auf die Bedeutung der formalen Methoden für den Nachweis, daß ein Softwaresystem gewisse Sicherheitsanforderungen erfüllt, hingewiesen. Entsprechend wurden in den Kriterien für die Bewertung der Sicherheit von Systemen der Informationstechnik sowohl in den USA (Orange Book) wie auch später in der Bundesrepublik (IT-Sicherheitskriterien) vorgeschrieben, daß bei der Entwicklung von Systemen, die höchste Sicherheits- und Zuverlässigkeitsstufen erreichen sollen, die Anwendung formaler Methoden zwingend erforderlich ist.
Wenn man von formalen Methoden im Zusammenhang mit Softwaresicherheit spricht, so meint man im allgemeinen die formale Spezifikation und Verifikation. Der Begriff formale Spezifikation bezeichnet eine Beschreibung der geforderten Software-Eigenschaften, die eine formale, das heißt eine mathematische Behandlung zuläßt. Neben der ausführbaren Programmiersprache ist daher eine formale Spezifikationssprache notwendig. Normalerweise besteht dabei die Spezifikation eines Programms aus den Anfangsbedingungen (Beschreibung der Eigenschaften der vorhandenen Daten) und aus den Endbedingungen (Beschreibung der geforderten Ergebnisse).
Ein Programm ist, vereinfacht gesagt, dann die korrekte Lösung der Aufgabenstellung, falls jedes Eingabedatum, das die Anfangsbedingung erfüllt, auf ein Ausgabedatum abgebildet wird, das die Endbedingung erfüllt. Eine formale Spezifikationssprache unterscheidet sich von herkömmlichen Programmiersprachen zum einen dadurch, daß sie direkt auf einer Logik aufbaut, zum anderen, daß in ihr ausgedruckt wird, was ein Programm tun soll - nicht das "Wie". Durch das Aufstellen einer formalen Spezifikation wird der Entwickler gezwungen, eine allgemeine informelle Problembeschreibung präzise in eine mathematisch exakte Form zu überführen. Die notwendige Formalisierung hilft schon wesentlich, Unklarheiten und Mißverständnisse zu vermeiden. Zudem kann sie rechnergestützt durch statische Analysen hinsichtlich Widerspruchsfreiheit und formaler Vollständigkeit überprüft werden.
Der bei den formalen Methoden verwendete Begriff der Verifikation bezeichnet dann den eigentlichen mathematischen Nachweis, daß ein Programm einer formalen Spezifikation genügt. Im Unterschied zur Software-Validierung, bei der informelle Methoden wie Code-Inspektion, Walk-through, Simulation und der systematische Test angewendet werden, basiert die Verifikation auf einem formalen System, bestehend aus formaler Sprache und einer Logik, in dem mathematisch Beweise durchgeführt werden können.
Der Einsatz von formalen Spezifikations- und Verifikationsmethoden für komplexe Computer-Programme erfordert maschinelle Unterstützung durch Entwicklungsumgebungen und Verifikationssysteme. Seit einiger Zeit gibt es Werkzeuge, die auf der Grundlage der formalen Spezifikationstechnik, der statischen Programmanalyse und der automatisierten Verifikationstechnik Unterstützung bei der Validierung und Verifikation von sicherheitsrelevanten Computer-Programmen leisten. Dies sind zum Beispiel Gypsy, Boyer-Moore-Beweiser, Cartesiana, PasquaIe, Eves oder Malpas. Viele ausländische Werkzeuge unterliegen aufgrund ihrer staatlichen Förderung Export-Restriktionen und sind erfahrungsgemäß in der Bundesrepublik höchstens für Demonstrationszwecke erhältlich (siehe Kasten). Die in der Bundesrepublik entwickelten Werkzeuge konnten bisher nur als Forschungssysteme oder Prototypen vorgestellt werden. Eines der wenigen verfügbaren Systeme, das schon in kommerziellen Projekten der Software-Sicherheit eingesetzt wurde, ist das in England entwickelte erwähnte Werkzeug Malpas. So wurden in Kanada die sicherheitsrelevanten Software. Anteile für Darlington-Kernreaktoren damit analysiert. Im britischen Verteidigungsministerium wird zur Abnahme aller sensitiven Software-Komponenten der Luft- und Raumfahrt die Durchführung einer statischen Analyse und die Verifikation gegen eine formale Spezifikation mit diesem Produkt gefordert.
Einordnung in den Software-Life-Cycle
Prinzipiell sind bei der Entwicklung fehlerfreier Software-Systeme zwei sich ergänzende und miteinander zu kombinierende Zielrichtungen einzuschlagen.
- Man ergreift bereits bei der Entwicklung konstruktive Maßnahmen, wie zum Beispiel das Aufstellen einer formalen Spezifikation, die dazu beitragen, Fehler möglichst von vornherein zu vermeiden.
- Es wird durch entwicklungsnachgeschaltete analytische Maßnahmen versucht, Fehler im Quellcode aufzudecken, beispielsweise durch statische Analyseverfahren.
Die formale Methode der Spezifikation und Verifikation sollten deshalb im Sinne einer frühen Fehlererkennung bei entsprechenden Sicherheitsanforderungen unbedingt in den konventionellen Prozeß der Software-Entwicklung integriert werden, um sie mit den informellen Methoden wie Simulation, Konfigurationsmanagement etc. zu verbinden, so daß sich die Methoden gegenseitig ergänzen und unterstützen können. Bei der Beschaffung eines Validierungs- und Verifikationswerkzeuges ist daher auf die Integrierbarkeit mit bestehenden Entwicklungsumgebungen (CASE-Tools) zu achten.
Formale Spezifikation und Verifikation kann sehr aufwendig sein. Dieser Aufwand läßt sich daher nur im Zusammenhang mit dem Nachweis von Sicherheitseigenschaften für Systemteile vertreten, an die besonders hohe Anforderungen bezüglich Sicherheit und Zuverlässigkeit gestellt werden. Dieser Aufwand kann durch den Einsatz der erwähnten Werkzeuge reduziert werden. Damit wird praktisch die Möglichkeit eröffnet, sowohl bei der Verifikation bestehender als auch beim Schreiben neuer Software Fehlerfreiheit mit einem vertretbaren Aufwand nachzuweisen.
Blockierte Sicherheitssoftware
Softwarekomponenten sind immer häufiger Bestandteil von Produkten und Systemen, bei denen ein Fehlverhalten zur Gefährdung von Personen und Sachwerten oder zum Verlust der Informationssicherheit führen kann. Aus der zunehmenden Notwendigkeit heraus, die Sicherheit und Zuverlässigkeit von Software nachzuweisen, wurden zahlreiche Methoden und Werkzeuge in den Bereichen Programmtest, Programmanalyse und Programmverifikation entwickelt. Leider stehen sie dem Markt nicht im vollem Umfang zur Verfügung, weil sie häufig mit öffentlichen Mitteln an Hochschulen entwickelt wurden. Gehen die Hochschulen mit den Produkten auf den Markt, so müssen die Mittel häufig an die fördernde Institution zurückgezahlt werden. Diese Bedingung verhindert häufig eine normale Vermarktung.