Verification of Robust Properties for Access Control Policies

1. Problemstellung

Herkömmliche Methoden zur Verifikation von Zugriffskontrollrichtlinien (Access Control Policies) basieren auf der Annahme, dass die Richtlinie vollständig und vollständig bestimmt ist, bevor die Verifikation beginnen kann.

• Der aktuelle Stand: Bestehende Werkzeuge (wie Margrave, Zelkova oder ASP-basierte Ansätze) übersetzen Richtlinien in mathematische Modelle oder logische Theorien und prüfen, ob eine Eigenschaft in diesem spezifischen, fertigen Modell gilt.
• Das Defizit: In der Praxis werden Richtlinien jedoch iterativ entwickelt, aus unabhängig gepflegten Komponenten zusammengesetzt und erweitert, wenn sich Organisationsstrukturen ändern. Oft müssen Sicherheitsbeschränkungen durchgesetzt werden, bevor alle Rollenverteilungen oder Delegationsentscheidungen finalisiert sind.
• Die Herausforderung: Bestehende Werkzeuge können nicht bestimmen, ob eine Eigenschaft strukturell garantiert ist, unabhängig davon, wie ausstehende Entscheidungen (pending decisions) später gelöst werden oder wie die Richtlinie erweitert wird. Eine Erweiterung der Richtlinie zwingt dazu, die gesamte Verifikation von vorne zu beginnen (mangelnde Kompositionalität).

Das Paper adressiert das Problem der robusten Eigenschaftsverifikation: Wie kann man bestimmen, was die Struktur einer Richtlinie unabhängig von der Lösung ausstehender Entscheidungen und unabhängig von zukünftigen Erweiterungen garantiert?

2. Methodik und Semantischer Rahmen

Der Autor entwickelt einen Rahmenwerk basierend auf der Basis-Erweiterungs-Semantik (Base-Extension Semantics), einer Form der beweis-theoretischen Semantik.

A. Der Support-Judgment ($\Vdash_P \phi$)

Das zentrale Konzept ist das Urteil „$\Vdash_P \phi$", das aussagt, dass die Richtlinie $P$ die robuste Eigenschaft $\phi$ besitzt. Im Gegensatz zur klassischen Semantik, die Wahrheit in einem statischen Modell prüft, wird die Gültigkeit hier durch das inferentielle Verhalten der Richtlinie über alle möglichen Erweiterungen hinweg definiert.

Die Semantik definiert logische Konnektoren für robuste Eigenschaften:

1. Implikation ($\Rightarrow$): $\Vdash_P \phi \Rightarrow \psi$ gilt, wenn jede Erweiterung von $P$, die $\phi$ unterstützt, auch $\psi$ unterstützt. Dies ist eine inferentielle Bedingung, keine materielle Implikation.
2. Robuste Disjunktion ($\oplus$): $\Vdash_P \phi \oplus \psi$ gilt, wenn für jede atomare Aussage $A$ und jede Erweiterung $Q$ von $P$: Wenn sowohl $\phi$ als auch $\psi$ in $Q$ jeweils $A$ implizieren, dann ist $A$ in $Q$ ableitbar. Dies erlaubt es, Sicherheitsgarantien zu treffen, bevor entschieden ist, welcher von mehreren Kandidaten (z. B. für eine Rolle) ausgewählt wird.
3. Robuste Konjunktion ($\otimes$): $\Vdash_P \phi \otimes \psi$ gilt, wenn jede Erweiterung, die sowohl $\phi$ als auch $\psi$ gleichzeitig als Hypothesen annimmt, eine atomare Aussage $A$ ableitet, die auch ohne diese Kombination ableitbar wäre. Dies fängt Fehler auf, die nur auftreten, wenn mehrere Bedingungen gleichzeitig gelten.
4. Negation ($\neg$): Definiert als $\phi \Rightarrow 0$, wobei $0$ für „Richtlinienkorruption" (der Zustand, in dem jede atomare Aussage ableitbar ist) steht. $\Vdash_P \neg \phi$ bedeutet, dass jede Erweiterung, die $\phi$ unterstützt, die gesamte Sicherheitsgarantie der Richtlinie zerstört.

B. Kompositionalität und Monotonie

Ein zentrales Ergebnis ist der Monotonie-Satz (Proposition 6): Wenn $\Vdash_P \phi$ gilt und $P$ zu einer größeren Richtlinie $Q$ erweitert wird ($Q \supseteq P$), dann gilt auch $\Vdash_Q \phi$.

• Bedeutung: Einmal verifizierte robuste Eigenschaften bleiben bei Erweiterungen erhalten. Administratoren müssen nicht bei jeder Änderung die gesamte Richtlinie neu verifizieren.

3. Berechnung und Reduktion auf Logikprogrammierung

Obwohl die Definition des Support-Urteils über eine unendliche Familie möglicher Erweiterungen quantifiziert (was zunächst unentscheidbar erscheint), zeigt das Paper, dass dies auf eine endliche Beweis-Suche (Proof-Search) in einer Logikprogrammierungssprache reduziert werden kann.

• Sprache: Es wird eine Horn-Klausel-Sprache mit atomaren zweiten Ordnung-Quantoren verwendet.
• Encoding ($\lceil \cdot \rceil$): Robuste Eigenschaften werden in Ziele (Goals) für die Beweis-Suche übersetzt.
  • Beispiel: Die robuste Disjunktion $\phi \oplus \psi$ wird kodiert als $\forall X. ((\lceil \phi \rceil \supset X) \supset (\lceil \psi \rceil \supset X) \supset X)$.
  • Dies nutzt den Mechanismus der Eigenvariablen (fresh atoms) in der uniformen Beweis-Suche, um die universelle Quantifizierung über alle möglichen Atome und Erweiterungen operativ abzubilden.
• Ergebnis: Die Verifikation robusten Eigenschaften reduziert sich auf das Ausführen eines Ziels in einem endlichen Logikprogramm.

4. Wichtige Beiträge

1. Identifikation des Problems: Die Einführung des Konzepts der „robusten Eigenschaftsverifikation" als beweis-theoretisches Problem für Zugriffskontrollrichtlinien.
2. Semantischer Rahmen: Definition des Support-Urteils $\Vdash_P \phi$ mit neuen Konnektoren ($\Rightarrow, \oplus, \otimes, \neg$), die Inferenz, Kompositionalität und Endlichkeit erfüllen.
3. Reduktion und Korrektheit: Beweis der Soundness und Vollständigkeit (Theorem 12) der Reduktion von der semantischen Definition auf die Beweis-Suche in einer zweiten Ordnung Logikprogrammierungssprache.
4. Praktische Anwendbarkeit: Demonstration, dass robuste Verifikation eine endliche, ausführbare Prozedur ist, die Kompositionalität bietet und somit den Lebenszyklus von Richtlinien (vor der Finalisierung) abdeckt.

5. Ergebnisse und Signifikanz

• Theoretische Leistung: Das Paper liefert eine formale Grundlage, um über Richtlinien zu reasoning, die noch nicht vollständig spezifiziert sind. Es verbindet proof-theoretic Semantics (insbesondere Base-Extension Semantics) mit Zugriffskontrollverifikation.
• Praktischer Nutzen:
  • Effizienz: Durch die Monotonie-Eigenschaft müssen bei Erweiterungen der Richtlinie nur die direkt betroffenen Eigenschaften neu geprüft werden.
  • Frühe Verifikation: Sicherheitsgarantien können bereits in der Entwurfsphase gegeben werden, bevor Rollen oder Delegationsentscheidungen final sind.
  • Komplementarität: Der Ansatz ergänzt bestehende Werkzeuge (wie SMT-basierte Zelkova oder BDD-basierte Margrave), die auf fertigen Richtlinien arbeiten. Er deckt die Lücke der iterativen Entwicklung ab.
• Beispiel: Das Paper nutzt ein Konferenz-Management-System als durchgehendes Beispiel, um zu zeigen, wie Konflikt-of-Interest-Beschränkungen und Trennung der Pflichten (Separation of Duty) robust verifiziert werden können, selbst wenn die Zuordnung des Konferenzvorsitzenden noch aussteht.

Fazit

Alexander V. Gheorghiu präsentiert einen Paradigmenwechsel in der Verifikation von Zugriffskontrollrichtlinien. Anstatt nur zu prüfen, ob eine Eigenschaft in einem aktuellen, statischen Modell gilt, prüft das neue Framework, ob die Struktur der Regeln eine Eigenschaft garantiert, unabhängig von zukünftigen Änderungen. Durch die Reduktion auf Logikprogrammierung wird dieses theoretisch mächtige Konzept in eine praktisch anwendbare, endliche Verifikationsmethode überführt, die Kompositionalität und Skalierbarkeit für sich entwickelnde Sicherheitssysteme bietet.