Formale Spezifikation politikbezogener Funktionen einer Trusted Computing Base
von Felix Neumann.
Wissenschaftliche Arbeit zur Erlangung des akademischen Grades “Master of Science”. Geschrieben am FG für Verteilte Systeme und Betriebssysteme der Technischen Universität Ilmenau.
Zusammenfassung
In der IT-Sicherheit stehen zunehmend professionelle und zielgerichtete Angriffe dem Problem gegenüber, dass heute verbreitete Computersysteme die von ihnen geforderten Sicherheitseigenschaften nicht erfüllen können. Eine Ursache hierfür liegt im unkontrollierten Wachstum der sicherheitskritischen Komponenten solcher Systeme, der sogenannten Trusted Computing Base (TCB). Dem kann durch TCB-Engineering begegnet werden, also der gezielten Steuerung der Größe und Komplexität einer TCB. Dabei werden die Funktionen der TCB aus ihren formalen Anforderungen hergeleitet; diese gehen Sicherheitsmodell bzw. Sicherheitspolitik des Systems hervor. Ein Problem ist es nun, eine adäquate Spezifikationsnotation für die TCB-Funktionen zu finden. Sie muss einerseits nah am mathematischen Modell sein, um eine Validierung zu ermöglichen, und andererseits eine verifizierbar korrekte Realisierung erlauben.
Die vorliegende Masterarbeit entwickelt daher eine Methode zur formalen Spezifikation der TCB-Funktionen auf Basis eines Sicherheitsmodells. Die Entwicklung der Methode erfolgt anforderungsorientiert. Mit ihr erstellte Spezifikationen setzen das zugrunde liegende Sicherheitsmodell vollständig um und sind konsistent zu diesem. Sie sind zustandsbasiert, formal und beweisbar widerspruchsfrei. Sie sind verständlich für solche Personen, die mit der Spezifikationsnotation vertraut sind, und wiederverwendbar für ähnliche Sicherheitsmodelle. Zudem verfügen sie über argumentierbar geringe Größe und Komplexität und sind für eine Realisierung nutzbar.
Die hierfür genutzte Spezifikationsnotation ist Event-B, die Spezifikationsmethode wurde jedoch soweit wie möglich losgelöst von dieser konkreten Notation entwickelt und lässt sich daher leicht auf andere Notationen zur formalen und zustandsbasierten Spezifikation übertragen. Die Methode greift in hohem Maße auf Unterstützung durch automatische Werkzeuge zurück. Die Ergebnisse der Masterarbeit wurden erfolgreich auf ein RBAC-Beispielmodell angewendet und die Widerspruchsfreiheit der daraus entstandenen Spezifikation ist vollständig bewiesen.