• Formale Sicherheitsmodelle

  • Leitfaden für die Erstellung und Prüfung formaler Sicherheitsmodelle im Rahmen von ITSEC/CC

Zuverlässigkeit, Vertrauenswürdigkeit und Korrektheit von Software-Systemen gewinnen als Qualitätsfaktoren unter wirtschaftlichen und gesellschaftlichen Aspekten zunehmend an Bedeutung. Das zuverlässige Funktionieren komplexer Software-Systeme ist inbesondere für die Sicherheit von technischen Systemen von großer Relevanz. Bei modernen Industrieanlagen und im Verkehrsbereich drohen als Folge des Versagens Gefahren für Menschen und Umwelt. Bei der Kommunikation und Verwaltung von Daten sowie beim Zahlungsverkehr drohen, aufgrund fehlerhaften Verhaltens entsprechender informationstechnischer Systeme (IT-Systeme), Bruch der Vertraulichkeit, Verlust oder Verfälschung von Daten und, in fast allen Fällen, erhebliche wirtschaftliche Nachteile. Letztere entstehen nicht nur aus den Schäden, die durch schlecht konzipierte und/oder fehlerhaft realisierte Systeme verursacht werden, sondern auch durch den zusätzlichen Aufwand für die Behebung von Mängeln.

Regierungen zahlreicher Staaten, aber auch übernationale Organisationen, haben verbindliche Kriterien und Standards für die Beurteilung der Betriebssicherheit (Safety) und der Informationssicherheit (Security von informationsverarbeitenden Systemen definiert. Bei der Beurteilung der Korrektheit eines Systems nach diesen Kriterien kommt dem Entwicklungsprozeß eine zentrale Rolle zu. In unterschiedlicher Ausprägung erfordern die hohen Evaluationsstufen dieser Kriterien den Einsatz formaler Methoden zur Erstellung mathematisch nachweisbar korrekter IT-Systeme.

Formale Methoden können in Abhängigkeit der Einsatztiefe charakterisiert werden. Mit der Einsatztiefe formaler Methoden erwächst das Vertrauen in die Korrektheit der so entwickelten SW-Komponenten. Im Basisfall werden formale Methoden ausschließlich zur Spezifikation des zu entwickelnden Systems eingesetzt. Das bedeutet sowohl zur formalen Modellierung der funktionellen Leistungsmerkmale in der top-level Leistungsspezifikation als auch die Auszeichnung spezieller Sicherheitseigenschaften im sog. Sicherheitsmodell. Die nächste Einsatzebene für formale Methoden ist die Unterstützung des stufenweisen Verfeinerungsprozesses von einer top-level-Spezifikation hin zu ablauffähigen Softwaresystemen. In der tiefsten Einsatzebene formaler Methoden werden diese zusätzlich zur automatischen Generierung der Beweispflichten und zur vollständigen Unterstützung der Beweistätigkeiten eingesetzt; dies umfaßt sowohl den Nachweis von Sicherheitseigenschaften innerhalb der top-level-Leistungsspezifikation als auch den Nachweis der Korrektheit bei der stufenweisen Spezifikationsverfeinerung.

Das BSI hat in den vergangenen Jahren die Entwicklung und Verbreitung von formalen Softwareentwicklungstechniken gefördert und befasst sich auch weiterhin mit exemplarischen Anwendungen und generischen Sicherheitsmodellen für sicherheitsrelevante Gebiete.