Formalisierung und Analyse von Zugriffsberechtigungen in PVS

Zugriffsberechtigungen können in Form von Zugriffskontrollpolitiken beschrieben werden. Dies sind komplexe Spezifikationen, die alle benötigten Zugriffsinformationen beinhalten. Zur Formulierung werden entsprechend ausdrucksstarke Sprachen benötigt.

Eine schwierige Aufgabe ist der Vergleich von Politiken. Politiken werden bezüglich der Zugriffseinschränkungen verglichen, die durch Anwenden der Politiken in dynamischen Umgebungen entstehen. Eine mögliche Fragestellung ist beispielsweise, ob eine Politik restriktiver ist als die andere, d.h. sie beinhaltet mehr Zugriffseinschränkungen. Diese Eigenschaft wird auch als "Contextual Policy Containment" bezeichnet.

In dieser Arbeit wird ein Verfahren zum Vergleich von Zugriffspolitiken in einer dynamischen Umgebung in PVS formalisiert. Dies beinhaltet die Beschreibung des Umgebungsmodells, der Zugriffspolitiken und der Algorithmen zum Politikvergleich. Mittels PVS werden Modelleigenschaften und die Korrektheit des Verfahrens verifiziert.

Die Formalisierung führt zu weitergehenden Ergebnissen. Es kann die Korrektheit vieler Eigenschaften nachgewiesen werden, ebenso wurden einige Unstimmigkeiten entdeckt, die wichtige Erkenntnisse für Erweiterungsmöglichkeiten liefern.