TU Darmstadt / ULB / TUprints

Automated Security Analysis of Virtualized Infrastructures

Bleikertz, Sören (2017)
Automated Security Analysis of Virtualized Infrastructures.
Technische Universität Darmstadt
Ph.D. Thesis, Primary publication

[img]
Preview
Text
Dissertation-Bleikertz-2017.pdf
Copyright Information: In Copyright.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Automated Security Analysis of Virtualized Infrastructures
Language: English
Referees: Waidner, Prof. Dr. Michael ; Groß, Dr. Thomas
Date: 2017
Place of Publication: Darmstadt
Date of oral examination: 17 May 2017
Abstract:

Virtualization enables the increasing efficiency and elasticity of modern IT infrastructures, including Infrastructure as a Service. However, the operational complexity of virtualized infrastructures is high, due to their dynamics, multi-tenancy, and size. Misconfigurations and insider attacks carry significant operational and security risks, such as breaches in tenant isolation, which put both the infrastructure provider and tenants at risk.

In this thesis we study the question if it is possible to model and analyze complex, scalable, and dynamic virtualized infrastructures with regard to user-defined security and operational policies in an automated way. We establish a new practical and automated security analysis framework for virtualized infrastructures. First, we propose a novel tool that automatically extracts the configuration of heterogeneous environments and builds up a unified graph model of the configuration and topology. The tool is further extended with a monitoring component and a set of algorithms that translates system changes to graph model changes. The benefits of maintaining such a dynamic model are time reduction for model population and closing the gap for transient security violations.

Our analysis is the first that lifts static information flow analysis to the entire virtualized infrastructure, in order to detect isolation failures between tenants on all resources. The analysis is configurable using customized rules to reflect the different trust assumptions of the users. We apply and evaluate our analysis system on the production infrastructure of a global financial institution. For the information flow analysis of dynamic infrastructures we propose the concept of dynamic rule-based information flow graphs and develop a set of algorithms that maintain such information flow graphs for dynamic system models. We generalize the analysis of isolation properties and establish a new generic analysis platform for virtualized infrastructures that allows to express a diverse set of security and operational policies in a formal language. The policy requirements are studied in a case-study with a cloud service provider. We are the first to employ a variety of theorem provers and model checkers to verify the state of a virtualized infrastructure against its policies. Additionally, we analyze dynamic behavior such as VM migrations.

For the analysis of dynamic infrastructures we pursue both a reactive as well as a proactive approach. A reactive analysis system is developed that reduces the time between system change and analysis result. The system monitors the infrastructure for changes and employs dynamic information flow graphs to verify, for instance, tenant isolation. For the proactive analysis we propose a new model, the Operations Transition Model, which captures the changes of operations in the virtualized infrastructure as graph transformations. We build a novel analysis system using this model that performs automated run-time analysis of operations and also offers change planning. The operations transition model forms the basis for further research in model checking of virtualized infrastructures.

Alternative Abstract:
Alternative AbstractLanguage

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.

German
URN: urn:nbn:de:tuda-tuprints-66100
Classification DDC: 000 Generalities, computers, information > 004 Computer science
Divisions: 20 Department of Computer Science
Date Deposited: 11 Aug 2017 09:49
Last Modified: 09 Jul 2020 01:47
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/6610
PPN: 415689910
Export:
Actions (login required)
View Item View Item