Im Hinblick auf die Erstellung und Prüfung formaler Spezifikationen gemäß den gültigen Kriterien (ITSEC, CC) bleiben erfahrungsgemäß nach dem Lesen der entsprechenden Passagen viele Fragen offen. Dieser Leitfaden soll – insbesondere für die Erstellung und Prüfung formaler Sicherheitsmodelle (Formal Model of Security Policy, FMSP) – dazu beitragen, Entwicklern und Evaluatoren ein besseres Verständnis dieser Thematik im Kontext der Kriterien zu ermöglichen. Ferner soll er helfen, den Mehrwert formaler Sicherheitsmodelle über die reine Erfüllung der Kriterienanforderungen hinaus zu erkennen.

Hierzu werden zunächst die verschiedenen und an verteilten Stellen der Kriterien definierten Anforderungen differenziert nach ITSEC und CC zitiert. Diese werden mit den Charakteristika formaler Methoden, bekannten und veröffentlichten formalen Sicherheitsmodellen und den Erfahrungen aus der Entwicklung und Prüfung formaler Modelle in Bezug gesetzt. Insbesondere wird deutlich, daß die in den Kriterienwerken zitierten Modelle nach Bell-LaPadula und Biba nur jeweils generische Rahmen definieren, in denen verschiedene Sicherheitspolitiken zur Zugriffskontrolle definiert werden können.

Deutlich herausgestellt wird, dass die formalen Sicherheitsmodelle keine isolierten Spezifikationen sind, sondern mit anderen Evaluationsdokumenten im direkten und engen Bezug stehen müssen, wie z. B. mit der funktionalen Spezifikation (siehe CC, Beschreibung ADV_FSP).

So weit es der Verständlichkeit dient, werden die Anforderungen an die Bestandteile formaler Sicherheitsmodelle nicht nur präzisiert, sondern mit kleinen Auszügen aus einem existierenden formalen Modell zu Integrated Circuit Cards mit Signaturfunktion nach DIN V 66291-1 unterlegt und erläutert.

Alle bisherigen Erfahrungen zeigen, dass durch eine formale Modellierung der Sicherheitspolitik – als formales Sicherheitsmodell – ein Zugewinn an Vertrauen in die Sicherheit des nach dieser Sicherheitspolitik arbeitenden Produktes erreicht werden kann. Dies gilt unter anderem deshalb, weil immer bereits Schwachstellen und Fehler auf Basis der informellen Sicherheitspolitiken aufgedeckt werden konnten.

Bisher werden diese Ergebnisse insofern immer teuer erkauft, weil die Erstellung formaler Sicherheitsmodelle als isolierte Evaluationsaufgabe nach Ende der Produktentwicklung verstanden wird und nicht bereits Teil der Systementwicklung ist. Wäre dies der Fall, würden viele Fehler und Sicherheitsschwachstellen in Produkten frühzeitig vermieden und bräuchten nicht im Nachhinein mit großem Aufwand beseitigt werden.

Der bisherige Leitfaden ist in das AIS Dokument AIS 39 überführt worden.