Zugriffsberechtigungen können in Form von Zugriffsregeln beschrieben werden. Zugriffsrichtlinien stellen eineMenge von Zugriffsregeln dar. Es sind komplexe Spezifikationen, die sämtliche Zugriffsinformationen beinhalten. Zur Formulierung werden entsprechend ausdrucksstarke Sprachen benötigt. Eine schwierige Aufgabe ist die Analyse und der Vergleich von Zugriffsrichtlinien. Ein Vergleich erfolgt bezüglich der Zugriffseinschränkungen und Zugriffsgewährungen, die durch Anwenden der Zugriffsrichtlinien in dynamischen Umgebungen entstehen. Es werden die Resultate von Regelanwendungen verglichen. Eine Fragestellung ist beispielsweise, ob eine Zugriffsrichtlinie restriktiver ist als die andere, d.h. sie beinhaltet mehr Zugriffseinschränkungen und erlaubt nur einen Teil der Zugriffe. Diese Eigenschaft wird auch als "Contextual Policy Containment" bezeichnet. In dieser Arbeit wird ein Verfahren von Dougherty, Fisler und Krishnamurthi zum Vergleich von Zugriffsrichtlinien in einer dynamischen Umgebung in PVS formalisiert. Dies beinhaltet die Beschreibung des Umgebungsmodells, der Zugriffsregeln und der Algorithmen zum Vergleich von Richtlinien. Mittels PVS werden die beschriebenen Modelleigenschaften formalisiert, die Algorithmen analysiert, und die Korrektheit der Verfahren untersucht. Die Formalisierung liefert weiterführende Ergebnisse. Bereits im Rahmen der Modellierung des dynamischen Systems und der Richtlinien sind einige Unstimmigkeiten und ungenaue Definitionen erkennbar. Bei der Verifikation, insbesondere in den Beweisen zur Korrektheit und Vollständigkeit der Algorithmen, werden Fehler des Modells sichtbar. Die entsprechenden Formeln können im ursprünglichen Modell mit PVS nicht bewiesen werden. Eine Analyse der entsprechenden Beweise liefert Erkenntnisse über Fehlerquellen. Das ursprüngliche Modell wird korrigiert. Es wird die Modellierung der Umgebung und die Definition von Vergleichskriterien geändert. Nach den änderungen kann die Korrektheit und Vollständigkeit der Algorithmen nachgewiesen werden. Es deutet allerdings darauf hin, dass ein grundlegendes Vergleichskriterium ebenfalls nicht korrekt ist. Die Korrektheit dieser Vergleichseigenschaft ist allerdings eine Voraussetzung zur Anwendung der Algorithmen. Auch dieser Sachverhalt wird erst durch Beweise in PVS deutlich. Es ist offensichtlich, dass diese wichtigen Erkenntnisse erst durch eine Formalisierung und durch maschinelle Beweisunterstützung erkennbar werden. Es wird deutlich, dass fehlerhafte manuelle Beweisskizzen, die auf den ersten Blick richtig erscheinen, durch PVS-Beweise und insbesondere durch Analyse von Beweisen widerlegt und auch korrigiert werden können.

Online Copy

Erhältlich als PDF-Datei (665 KB)

BibTeX Entry

@MastersThesis{Groener07, author = "Gerd Gröner", title = "Formalisierung und Analyse von Zugriffsberechtigungen in PVS" school = "Universität Ulm", year = 2007, }