💻 computer science

Security Engineering in IIIf, Part II -- Shadowing the IIIf

Diese Arbeit erweitert das Security Engineering des Isabelle Insider und Infrastructure Framework (IIIf), indem sie Morgans „Shadow“-Konzept einführt, um die Informationsfluss-Sicherheit zu formalisieren, wodurch das Verfeinerungsparadoxon gelöst und Bedingungen für sichere Verfeinerungen etabliert werden, die anhand eines Flugradar-Systems illustriert werden.

Ursprüngliche Autoren: Florian Kammüller

Veröffentlicht 2026-06-30

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Florian Kammüller

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Das große Ganze: Das „Flugradar“-Problem

Stellen Sie sich vor, Sie schauen auf einer Flugradar-App auf Ihrem Handy nach Flugzeugen. Sie sehen Flugzeuge, die sich über die Karte bewegen. Normalerweise ist das harmlos. Aber was wäre, wenn ein Flugzeug plötzlich einen seltsamen Zickzack-Umweg um ein bestimmtes Gebiet fliegt?

In der realen Welt fliegen Flugzeuge nicht aus Spaß in Zickzack-Linien. Wenn ein Flugzeug plötzlich um eine geheime Militärbasis oder den Standort einer VIP-Person herumschwenkt, ist dieses „Ausweichen“ ein Hinweis. Auch wenn die App die geheime Basis nicht anzeigt, verrät das Muster der Flugbewegung genau, wo die Gefahrenzone liegt.

Dies ist das Problem, das die Arbeit behandelt: Wie verhindern wir, dass geheime Informationen durch die Nebenwirkungen des Systemverhaltens „durchsickern“?

Die Akteure und das Setting

Das System (IIIf): Stellen Sie sich dies als ein riesiges, superstrenges Regelwerk für eine digitale Stadt vor. Es verfolgt, wer wo ist, welche Regeln sie befolgen und wie sich Dinge bewegen. Die Autoren verwenden ein leistungsstarkes Computerwerkzeug namens „Isabelle“, um dieses Regelwerk so streng zu schreiben, dass der Computer seine Korrektheit beweisen kann.
Der Angreifer (Eve): Eve ist eine neugierige Beobachterin, die alles sehen kann, was das System der Öffentlichkeit zeigt (wie die Position des Flugzeugs auf der Karte), aber nicht die Geheimnisse kennen darf (wie den Standort einer geheimen Basis).
Das Geheimnis (Kritischer Standort): Dies ist die „verbotene Zone“, die das System zu schützen versucht.

Das Problem: Das „Refinement-Paradoxon“

Die Autoren erklären eine knifflige Situation, die als Refinement-Paradoxon bezeichnet wird.

Stellen Sie sich vor, Sie entwerfen ein sicheres System (die „abstrakte“ Version). Sie beweisen dem Computer, dass Eve das Geheimnis nicht erraten kann. Großartig!
Dann entscheiden Sie sich, das System besser oder detaillierter zu machen (die „verfeinerte“ Version). Vielleicht fügen Sie eine neue Funktion hinzu, wie zum Beispiel die Anzeige der Geschwindigkeit des Flugzeugs.

Das Paradoxon: Selbst wenn Ihre neue Funktion harmlos erscheint, könnte sie versehentlich ein neues „Leck“ erzeugen.

Analogie: Stellen Sie sich vor, Sie verstecken einen geheimen Zettel in einem Safe. Sie beweisen, dass der Safe sicher ist. Dann beschließen Sie, einen winzigen, dekorativen Griff an den Safe zu montieren. Sie haben das Schloss nicht verändert, aber jetzt, wenn man den Safe schüttelt, klappert der Griff je nach Position des Zettels im Inneren unterschiedlich. Plötzlich verrät der Griff das Geheimnis.

In dem Beispiel der Arbeit: Wenn das System die Geschwindigkeit des Flugzeugs basierend auf seinem echten (verborgenen) Pfad berechnet anstatt auf seinem öffentlichen Pfad, wird die Geschwindigkeitszahl immer merkwürdig sein, wenn das Flugzeug eine geheime Zone umfliegt. Eve sieht die merkwürdige Geschwindigkeit und weiß sofort, wo die geheime Zone liegt. Das System wurde „detaillierter“, aber es wurde weniger sicher.

Die Lösung: Der „Schatten“

Um dies zu beheben, führen die Autoren ein Konzept namens Schatten ein, das von einem Mathematiker namens Morgan inspiriert wurde.

Was ist ein Schatten?
Betrachten Sie den Schatten als einen „Beutel voller Möglichkeiten“ für die geheime Information.

Zu Beginn ist der Schatten ein riesiger Beutel, der jede einzelne Möglichkeit enthält, wo sich das Geheimnis befinden könnte. Der Angreifer ist völlig verwirrt; er hat keine Ahnung, wo das Geheimnis ist.
Während das System läuft, sollte der Schatten groß bleiben. Wenn der Schatten kleiner wird, bedeutet das, dass der Angreifer etwas Neues gelernt hat.

Das Ziel: Ein sicheres System ist eines, bei dem der Schatten niemals schrumpft. Wenn der Schatten gleich groß bleibt, bleibt die Unwissenheit des Angreifers erhalten. Er weiß immer noch nicht mehr als zu Beginn.

Wie sie das Flugradar behoben haben

Die Autoren wendeten diese „Schatten“-Idee auf ihr Flugradar-System an:

Das Leck: In der ursprünglichen unsicheren Version verriet die Bewegung des Flugzeugs den geheimen Standort. Der Schatten wurde kleiner, weil der Angreifer bestimmte Standorte basierend auf dem Pfad des Flugzeugs ausschließen konnte.
Die Lösung: Sie fügten einen „Versteck“-Mechanismus hinzu. Wenn ein Flugzeug eine geheime Zone umfliegen muss, zeichnet das System den echten Pfad in einer geheimen Box (der critpos-Komponente) auf, zeigt das Flugzeug auf der öffentlichen Karte jedoch so an, als wäre es geradewegs durch die geheime Zone geflogen.
Das Ergebnis: Da die öffentliche Karte normal aussieht, wird der „Beutel voller Möglichkeiten“ (der Schatten) des Angreifers niemals kleiner. Der Angreifer glaubt immer noch, dass die geheime Zone überall sein könnte.

Der „magische“ Beweis

Die Arbeit unternimmt zwei wesentliche Schritte:

Äquivalenz: Sie haben bewiesen, dass „Der Schatten schrumpft niemals“ exakt dasselbe ist wie „Non-Interferenz“ (ein technischer Fachbegriff dafür, dass „Geheimnisse keine Auswirkungen auf das haben, was die Öffentlichkeit sieht“). Es ist so, als würde man beweisen, dass „Der Beutel voll bleibt“ dasselbe ist wie „Niemand hat Äpfel gestohlen“.
Die Sicherheitsregel für Upgrades: Sie haben eine Regel (Theorem 2) erstellt, um zu prüfen, ob ein zukünftiges Upgrade (Refinement) sicher bleibt.
- Die Regel: Wenn Sie eine neue Funktion hinzufügen, müssen Sie prüfen, ob diese vom Geheimnis abhängt. Wenn die neue Funktion vom Geheimnis abhängt, wird der Schatten schrumpfen und das Upgrade ist unsicher.
- Die Bedingung: Wenn die neue Funktion völlig unabhängig vom Geheimnis ist, bleibt der Schatten groß und das Upgrade ist sicher.

Zusammenfassung

Die Arbeit löst ein Problem, bei dem das detailliertere Gestalten eines Systems versehentlich Geheimnisse preisgibt. Sie nutzen einen „Schatten“ (einen Beutel voller Möglichkeiten), um zu verfolgen, was ein Angreifer weiß. Wenn der Schatten voll bleibt, ist das System sicher. Sie haben bewiesen, dass man, wenn man ihre spezifischen Regeln bei der Hinzufügung neuer Funktionen befolgt, das System upgraden kann, ohne versehentlich Geheimnisse preiszugeben.

Kurz gesagt: Sie haben einen mathematischen „Sicherheitsdienst“ gebaut, der jedes Mal prüft, wenn Sie eine neue Funktion zu einem System hinzufügen, um sicherzustellen, dass die neue Funktion den Geheimnissen nicht versehentlich etwas zu zuflüstert.

Technische Zusammenfassung: Shadowing der Isabelle Insider und Infrastructure Framework

Problemstellung
Das Isabelle Insider and Infrastructure Framework (IIIf) bietet eine formale Basis für das Security Engineering von Systemen, die menschliche Akteure, Richtlinien sowie physische und logische Komponenten involvieren, unter Verwendung eines Refinement-Risk (RR)-Zyklus. Während das IIIf trace-basierte Verfeinerung (Refinement) und Eigenschaftserhaltung für Standard-Sicherheitseigenschaften (z. B. Erreichbarkeit) unterstützt, steht es vor einer kritischen Einschränkung hinsichtlich der Informationsflusskontrolle (Information Flow Control, IFC). Speziell die Eigenschaft der Nichtinterferenz (Noninterference, NI) – welche sicherstellt, dass hochgesicherte (geheime) Zustände keine Einflussnahme auf niedrig gesicherte (öffentliche) Beobachtungen ausüben – wird unter Spezifikationsverfeinerung nicht generell bewahrt. Dieses Phänomen, bekannt als „Refinement-Paradoxon“, bedeutet, dass eine Spezifikation, die NI erfüllt, eine verfeinerte Implementierung hervorbringen kann, die Informationen durch implizite Flüsse preisgibt. Bestehende Model-Checking-Ansätze innerhalb des IIIf sind unzureichend, um solche Trace-Set-Eigenschaften zu verifizieren, was eine neue Methodik zur Charakterisierung und Garantie sicherer Verfeinerungen erforderlich macht.

Methodik
Um das Refinement-Paradoxon zu adressieren, führt das Paper eine Formalisierung von Morgans Konzept eines „Shadow“ (Schatten) in das IIIf-Framework ein. Die Methodik erfolgt durch folgende Schritte:

Integration einer Fallstudie: Die Autoren nutzen eine Flugradar-Systemspezifikation (die zuvor im IIIf formalisiert wurde) als laufendes Beispiel. Dieses System umfasst Flugzeugpositionen, Routen und kritische Orte. Die initiale Spezifikation zeigt auf, wie implizite Informationsflüsse entstehen, wenn ein Flugzeug einen kritischen Ort umgeht, wodurch die Existenz dieser Kritikalität durch beobachtbare Unregelmäßigkeiten im Flugpfad offenbart wird.
Formalisierung von Nichtinterferenz (NI): NI wird innerhalb des IIIf als eine Äquivalenzrelation über Zustandsübergänge definiert. Zwei Zustände sind für einen Angreifer (mit Sicherheitsfreigabe $a$ ) ununterscheidbar, wenn ihre beobachtbaren Komponenten (deren Sicherheitslabels $\leq a$ sind) identisch sind. NI gilt, wenn für jedes Paar ununterscheidbarer Anfangszustände deren nachfolgende Ausführungstraces ebenfalls ununterscheidbar bleiben.
Definition des Shadows: Inspiriert von Morgans epistemischer Logik wird ein „Shadow“ als die Menge aller möglichen Werte definiert, die eine sicherheitskritische Zustandskomponente aus der Perspektive des Angreifers annehmen könnte.
- Initialisierung: Eine Shadow-Komponente wird mit dem „Universum“ ihres Typs initialisiert (alle möglichen Werte), was maximale Unwissenheit repräsentiert.
- Verkleinerung (Shrinking): Während der Zustandsübergänge „schrumpft“ der Shadow (die Menge der möglichen Werte reduziert sich) nur dann, wenn der Übergang dem Angreifer Informationen über die geheime Komponente offenbart.
- Invariante: Ein sicheres System muss die Invariante $IFC_a$ erfüllen, wobei der Shadow einer geheimen Komponente während der Ausführung nicht schrumpft. Wenn der Shadow schrumpft, impliziert dies, dass der Angreifer Wissen über das Geheimnis erlangt hat, was auf eine Verletzung von NI hindeutet.
Äquivalenzbeweis: Das Paper stellt formal (auf dem Papier, aufgrund der Typquantifizierungsgrenzen in der Higher Order Logic) fest, dass die Shadow-Invariante $IFC_a$ mit der Nichtinterferenz ( $NI_a$ ) äquivalent ist. Konkret wird gezeigt, dass die Negation von NI (Existenz eines unzulässigen Informationsflusses) äquivalent zur Existenz einer Komponente ist, deren Shadow schrumpft.
Charakterisierung sicherer Verfeinerung: Die Autoren definieren eine Bedingung für sichere Verfeinerung. Eine Verfeinerung von einem abstrakten System $A$ zu einem konkreten System $C$ bewahrt die Sicherheit, wenn die Verfeinerungsabbildung $E$ , restriktiv auf die Shadow-Komponenten von $C$ , injektiv und kompatibel mit dem abstrakten Shadow ist.

Kernbeiträge

Shadow-Formalisierung in IIIf: Das Paper erweitert das IIIf um eine formale Definition von „Shadow“-Komponenten für Infrastrukturzustände, was die Verfolgung der Ungewissheit eines Angreters bezüglich geheimer Zustandskomponenten ermöglicht.
Äquivalenz von Shadow und NI: Es beweist, dass die Shadow-Invariante ( $IFC_a$ ) äquivalent zur Nichtinterferenz-Eigenschaft ( $NI_a$ ) im Kontext des IIIf-Zustandsübergangsmodells ist.
Sichere Verfeinerungstheorema (Theorem 2): Der primäre Beitrag ist ein Theorem, das die sichere Verfeinerung charakterisiert. Es besagt, dass wenn eine Verfeinerungsabbildung $E$ auf den Shadow-Komponenten des konkreten Systems injektiv und kompatibel mit dem abstrakten Shadow ist, die Shadow-Invariante (und somit NI) von dem abstrakten zum konkreten System bewahrt wird.
Lösung des Refinement-Paradoxons: Die Methodik bietet einen Mechanismus, um zu verifizieren, dass ein Verfeinerungsschritt keine neuen Informationsflüsse einführt, die NI verletzen würden, und adressiert damit einen bekannten Mangel des standardmäßigen IIIf RR-Zyklus.

Ergebnisse

Anwendung auf das Flugradar-System: Die Autoren wenden die Shadow-Definition auf die Flugradar-Fallstudie an.
- In einer unsicheren Version (ohne Versteckmechanismen) schrumpft der Shadow der kritischen Lagekomponente, wenn ein Flugzeug einen kritischen Bereich umgeht, was die Verletzung von $IFC_a$ und NI beweist.
- In einer gesicherten Version (unter Verwendung einer critpos-Komponente, um die tatsächliche Umfahrung zu verbergen) hält die Shadow-Invariante, was die Abwesenheit unzulässiger Flüsse bestätigt.
Verfeinerungsanalyse: Das Paper demonstriert, dass das Hinzufügen einer neuen Komponente (z. B. „Geschwindigkeit“), die basierend auf verborgenen Positionen berechnet wird, eine unsichere Verfeinerung darstellt, da sie den Shadow schrumpfen lässt und somit die Injektivitäts-/Kompatibilitätsbedingungen von Theorem 2 verletzt. Umgekehrt zeigt es, dass das Hinzufügen von Komponenten, die nicht von Geheimnissen abhängen und korrekt durch die Verfeinerungsabbildung behandelt werden, die Sicherheit bewahrt.
Metatheoretische Grenzen: Die Autoren merken an, dass die Äquivalenz zwischen Shadow und NI zwar argumentiert werden kann, die vollständige Formalisierung des Äquivalenztheorems über alle Infrastrukturtypen hinweg jedoch durch das Typsystem von Isabelle/HOL begrenzt ist, da dies eine Quantifizierung über unterschiedlich typisierte Komponenten des Zustands erfordert.

Bedeutung und Ansprüche
Das Paper beansprucht, die Sicherheits-Engineering-Fähigkeiten des IIIf-Frameworks durch die Integration von Information Flow Control zu erweitern. Seine Bedeutung liegt in:

Adressierung des Refinement-Paradoxons: Es bietet eine konkrete Methodik, um sicherzustellen, dass Sicherheitseigenschaften (speziell NI) während des Verfeinerungsprozesses bewahrt werden – eine Fähigkeit, die dem Framework zuvor fehlte.
Überbrückung von Abstraktion und Implementierung: Durch die Nutzung des Shadow-Konzepts kann das Framework nun formal über die „Ungewissheit“ eines Angreifers argumentieren und sicherstellen, dass Verfeinerungen nicht unbeabsichtigt diese Ungewissheit reduzieren (d. h. Informationen preisgeben).
Praktische Verifizierung: Der Ansatz ermöglicht die Verifizierung komplexer, heterogener Systeme (die physische und logische Aspekte kombinieren), bei denen das Standard-Model-Checking versagt.

Die Autoren bleiben bescheiden hinsichtlich des Umfangs und räumen ein, dass die Äquivalenzbeweise aufgrund typentheoretischer Einschränkungen derzeit primär „auf dem Papier“ etabliert sind und die Methodik spezifisch auf das IIIf-Infrastrukturmodell zugeschnitten ist, statt auf eine allgemeine Programmiersprachenlogik. Die Arbeit baut auf den grundlegenden Konzepten von Morgan auf, passt diese jedoch an ein Zustandsübergangssystem mit expliziten Akteuren und Richtlinien an, wodurch die Notwendigkeit einer dedizierten epistemischen Logik vermieden wird, indem das bestehende IIIf-Modell der Zugriffsrechte von Akteuren genutzt wird.