Zusammenfassung

  • Dorothy E. Denning ordnete 1976 Sicherheitsklassen partiell und nutzte die kleinste obere Schranke, den Join, um die Mindestklasse eines Ergebnisses aus mehreren Eingaben zu bestimmen.
  • Das Modell erfasst ausdrückliche Übertragungen und implizite Abhängigkeiten über Kontrollbedingungen, aber nur innerhalb deklarierter Klassen und dargestellter Programmsemantik.
  • Verdeckte Kanäle, falsche Kennzeichnungen, Implementierungsfehler und unbegründete Deklassifizierung bleiben getrennte Risiken. Ein bestandener Gittertest ist kein Sicherheitsurteil über das Gesamtsystem.

Welche Klasse braucht ein Ergebnis, das von zwei verschieden eingestuften Eingaben abhängt? In „A Lattice Model of Secure Information Flow“ antwortet Dorothy E. Denning: die kleinste Klasse, die beide Eingaben erreichen dürfen. Diese kleinste obere Schranke ist ihr Join.

A → B bedeutet, dass Information der Klasse A nach B fließen darf. Die Relation ist reflexiv, transitiv und antisymmetrisch, also eine partielle Ordnung. Zwei Abteilungen können unvergleichbar bleiben und dennoch eine gemeinsame obere Klasse besitzen. Hängt c von a und b ab, gilt class(a) join class(b) → class(c).

Damit wird eine politische Vorgabe mechanisch prüfbar. Der Ausdruck sagt jedoch nicht, dass c in der Wirklichkeit ungefährlich ist. Er sagt, dass der dargestellte Einfluss unter den gewählten Klassen und Regeln erlaubt ist.

Ein Zweig kann Information tragen

Denning versteht Fluss als Einfluss. b := a ist ein ausdrücklicher Fluss. Bei if a = 0 then b := c kann der Endzustand von b verraten, ob die Bedingung über a wahr war. So entsteht ein impliziter Fluss von a nach b, obwohl der Wert von a nicht kopiert wird.

Auch heutige Software verrät Information über Verzweigungen, Fehler, Zähler und Laufzeiten. Eine Prüfung, die nur kopierte Felder verfolgt, übersieht diese Abhängigkeiten. Das Gitter zwingt dazu, alle modellierten Einflüsse in die Zielklasse einzurechnen.

Klassen von Variablen, Ausdrücken und Bedingungen lassen sich vor der Ausführung fortschreiben. Nicht erlaubte Ziele können abgewiesen werden. „Certification of Programs for Secure Information Flow“ führte dieses Verfahren weiter aus.

Dabei ist die Urheberschaft eindeutig zu halten. Der Gitteraufsatz von 1976 stammt allein von Dorothy E. Denning. Der Zertifizierungsaufsatz ist eine gemeinsame Arbeit von Dorothy E. Denning und Peter J. Denning, 1977 veröffentlicht nach dem Purdue Technical Report 76-181. Die Trennung zeigt auch den Weg vom Modell zur gemeinsam entwickelten Prüfmethode.

Das Modell endet an seiner Darstellung

Der Aufsatz von 1976 beschränkt sich auf legitime und Speicherkanäle. Verdeckte Kanäle, etwa Signale über die Systemlast, sind ausdrücklich nicht Gegenstand. Eine Zertifizierung kann außerdem keinen Fluss prüfen, der in der Programmdarstellung fehlt. Fehlende Grenzprüfungen, hängende Referenzen, Compilerfehler, ein abweichendes Binärprogramm oder Hardwaredefekte können zertifizierte Semantik und echte Ausführung trennen.

Auch die Kennzeichnung kann falsch sein. Wird ein Geheimnis als öffentlich markiert, kann das Modell eine unerwünschte Übertragung korrekt erlauben. Umgekehrt führt ausschließlich aufwärts gerichteter Fluss leicht zu Überklassifizierung. Die gemeinsame Studie „Data Security“ behandelt autorisierte Herabstufung und informationsverlierende Programme. Beides braucht eine eigene Begründung: Wer darf freigeben, welche Information ging verloren, und wie wurde dies geprüft?

Zeit- und Ressourcenkanäle können ohne normale Zuweisung kommunizieren. Ein formal erlaubtes Ergebnis kann zudem an ein unsicheres Endgerät oder an einen Dienst gelangen, der seine Kennzeichnung entfernt. Das sind keine Widerlegungen des Gitters, sondern Anwendungen außerhalb seines Anspruchs.

In „The Limits of Formal Security Models“ erinnerte Denning 1999 daran, dass formale Methoden Eigenschaften innerhalb vereinfachter Modelle und Annahmen feststellen, reale Angriffe aber oft außerhalb dieses Rahmens liegen. Die Lehre lautet nicht weniger Formalität, sondern eine genaue Bezeichnung des Ergebnisses.

Ein Nachweis in einer längeren Kette

Ein belastbares Verfahren verbindet den Test mit der versionierten Flusspolitik, der Herkunft aller Kennzeichnungen und der semantischen Abdeckung des Analysators. Es hält die Identität von Quelltext, Werkzeug, Compiler, Abhängigkeiten, Binärdatei und Deployment zusammen. Deklassifizierung besitzt eigene Berechtigung und Protokolle; Laufzeit und Endpunkte bewahren Kennzeichnungen; Seitenkanäle werden gesondert geprüft.

Bell–LaPadula gehört zur benachbarten Geschichte mehrstufiger Sicherheit und steht in Dennings Literaturverzeichnis. Es ersetzt nicht ihre eigene Verbindung von Informationsabhängigkeit, Klassenkombination und Programmzertifizierung. Zugriffskontrolle fragt, was ein Subjekt tun darf. Dennings Gitter fragt, welche Klasse aus allen Einflüssen auf ein Ergebnis folgt.

Gerade diese begrenzte Aussage macht das Modell dauerhaft nützlich: Es beantwortet eine wichtige Frage exakt, ohne die übrigen Fragen zu verdecken.

Quellen