Virtualisierung ermöglicht eine höhere Effizienz und Elastizität von modernen IT Infrastrukturen, ein- schließlich Infrastructure as a Service. Jedoch ist die operationale Komplexität von virtualisierten Infra- strukturen aufgrund ihrer Dynamik, “Multi-Tenancy” und ihrer Größe sehr hoch. Fehlkonfigurationen und Angriffe von Insidern tragen zu erheblichen operationalen und Sicherheitsrisiken bei. Beispielsweise führen Verletzungen in der Tenant-Isolierung zu Risiken sowohl für den Infrastrukturbetreiber als auch für den Nutzer.

In dieser Dissertation untersuchen wir die Frage, ob es möglich ist komplexe, skalierbare und dynamische virtualisierte Umgebungen zu modellieren und hinsichtlich benutzerdefinierter operationaler und sicher- heitsrelevanter Richtlinien in einem automatischen Verfahren zu überprüfen. Wir etablieren ein neues praktisches und automatisches Framework für die Sicherheitsanalysen von virtualisierten Infrastrukturen. Zuerst stellen wir ein System vor, welches die Konfiguration von heterogenen Umgebungen automatisch extrahieren kann und ein einheitliches Graphenmodell der Konfiguration und der Topologie aufbaut. Zusätzlich wird das System mit einer Komponente zur Überwachung der Umgebung sowie Algorithmen ausgebaut, welche es erlauben, Änderungen in der Umgebung in Änderungen im Graphenmodell zu über- setzen. Die Vorteile eines solchen dynamischen Modells sind zum einen Zeiteinsparungen im Aufbau des Modells, als auch das Schliessen der Lücke im Erkennen von vorübergehenden Sicherheitsverletzungen. Unsere Analyse ist die erste, welche statische Informationsflussanalyse auf die gesamte virtualisierte Umgebung überträgt, somit können Verletzungen in der Tenant-Isolierung in allen Ressourcen entdeckt werden. Die Analyse ist mittels benutzerdefinierter Regeln konfigurierbar, welche die unterschiedli- chen Sicherheitsannahmen der Benutzer widerspiegeln. Wir verwenden und evaluieren unser System in der Produktionsumgebung eines globalen Finanzinstitutes. Im Rahmen der Informationsflussanalyse von dynamischen Infrastrukturen stellen wir das Konzept der dynamischen, regelbasierten Informa- tionsflussgraphen vor und entwickeln Algorithmen, welche Informationsflussgraphen für dynamische Systemmodelle verwalten.

Wir generalisieren die Analyse von Isolationseigenschaften und etablieren eine generische Analyseplatt- form für virtualisierte Infrastrukturen, welche es erlaubt eine breite Menge von operationalen und sicherheitsrelevanten Richtlinien in einer formalen Sprache auszudrücken. Die Anforderungen an die aus- zudrückenden Richtlinien werden in einer Fallstudie mit einem Cloud-Provider untersucht. Erstmals wird eine Reihe von etablierten automatischen Theorembeweisern sowie Modellprüfern für die Analyse von virtualisierten Infrastrukturen gegenüber spezifizierten Richtlinien angewendet. Außerdem überprüfen wir dynamisches Verhalten, wie zum Beispiel die Migration von VMs.

Im Falle der Analyse von dynamischen Infrastrukturen verfolgen wir sowohl einen reaktiven als auch einen proaktiven Ansatz. Unser neu entwickeltes reaktives Analysesystem reduziert die Zeit zwischen Systemän- derung und Analyseergebnis. Das System überwacht die Infrastruktur auf Änderungen und verwendet einen dynamischen Informationsflussgraphen unter anderem zur Überprüfung von Tenant-Isolierung. Im Rahmen des proaktiven Ansatzes entsteht ein neuartiges Modell, das Operations Transition Model, welches durch Operationen verursachte Änderungen in virtualisierten Infrastrukturen mittels Graphtransformatio- nen abbildet. Ein neues auf dem Modell aufbauendes Analysesystem überprüft automatisch Operationen zur Laufzeit und ermöglicht es außerdem, Änderungen in virtualisierten Umgebungen zu planen. Das Operations Transition Model bildet die Basis für weitere Forschungen im Bereich der Modellüberprüfung von virtualisierten Infrastrukturen.