Open Topics
Available Theses Topics (mostly in German)
Kryptographische Beweisbarkeit verschiedener Schutzziele in der IT-Sicherheit
Um Anwendungen sicher zu gestalten, muss zunächst festgelegt werden, welche Anforderungen an die Sicherheit der Anwendung bestehen. Dafür werden häufig Schutzziele, vor allem Vertraulichkeit, Integrität und Verfügbarkeit, verwendet [Bis05]. Es gibt aber auch noch eine erweiterte Liste an Schutzzielen [BFP14], z.B. Unbeobachtbarkeit und Zurechenbarkeit, womit die Anforderungen weiter spezifiziert werden können. In dieser Arbeit soll zunächst ein Überblick über die verschiedenen erweiterten Schutzziele in der IT-Sicherheit gegeben werden. Die Schutzziele sollen nach Möglichkeit in einer geeigneten Beispielanwendung veranschaulicht werden. Eventuell sind mehrere Anwendungen notwendig, um alle Schutzziele sinnvoll zu erfassen. Darauf aufbauend soll untersucht werden, wie die Erfüllung der einzelnen Schutzziele kryptographisch bewiesen oder mindestens argumentiert werden könnte (für einen Einstieg in kryptographische Beweise siehe z.B. [KL20]). Gerne können an dieser Stelle auch Beweisskizzen mit Bezug zur gegebenen Beispielanwendung zur Veranschaulichung verwendet werden. Außerdem soll für jedes Schutzziel argumentiert werden, inwieweit ein Angriff verhindert werden kann und mit welcher Wahrscheinlichkeit das Schutzziel erfüllt wird, wenn der vorgestellte Sicherheitsbeweis korrekt geführt wurde. Hierbei soll insbesondere auch eine Unterscheidung zwischen informationstheoretischer und praktischer Sicherheit erfolgen.
Referenzen:
[Bis05] Matt Bishop. Introduction to computer security. Addison-Wesley Boston, 2005.
[BFP14] Ulrike Baumann, Elke Franz, and Andreas Pfitzmann. Kryptographische Systeme. Springer Berlin Heidelberg, 2014.
[KL20] J. Katz and Y. Lindell. Introduction to Modern Cryptography. CRC Press, 2020.
Automatischer Vergleich zwischen Protokollbeschreibung und Code - Machbarkeitsstudie
In kryptographischen Protokollen ist es wünschenswert, bestimmte Protokolleigenschaften möglichst theoretisch zu beweisen. Selbst wenn derartige Beweise vorliegen, können bei der praktischen Umsetzung in Programmcode Fehler passieren, die für unerwartete Sicherheitslücken sorgen. Es gibt bereits verschiedene Tools, die unter anderem mit Hilfe von künstlicher Intelligenz die Korrektheit von Programmcode beurteilen sollen (z.B. [PSS98;Kan+20;Sam+21]). Es wirkt naheliegend, darauf aufbauend auch automatisch prüfen zu wollen, ob der Programmcode einer gegebenen Protokollspezifikation entspricht. In der Literatur gibt es bereits Ansätze, um ein ähnliches Ziel zu erreichen (siehe z.B. [APS14]). Hierbei wird allerdings entweder das Modell mit der Protokollspezifikation oder der Code generiert, statt beide Teile zu vergleichen.
Diese Arbeit soll in den folgenden Schritten herausarbeiten, ob eine solche Prüfung generell möglich ist und wie sie gegebenenfalls umgesetzt werden könnte:
- Zunächst soll ein Überblick über bestehende Tools zur Überprüfung von Korrektheit von Softwarecode gegeben werden. Hierbei soll auch eine Kategorisierung nach der zugrunde liegenden Technik vorgenommen werden.
- Darauf aufbauend sollen mögliche Anforderungen an das Tool für den Vergleich zwischen Programmcode und Protokollspezifikation herausgearbeitet werden.
- Im Anschluss sollen diese Ergebnisse genutzt werden, um eine Einschätzung zu geben, wie dieses Tool am besten umgesetzt werden könnte. Es sollte dabei detailliert darauf eingegangen werden, welche Techniken das Tool benutzt, wie das Protokoll dargestellt werden müsste und welche Anforderungen der zu vergleichende Programmcode gegebenenfalls erfüllen muss.
Es kann, aber muss nicht, auch eine Art Prototyp entworfen werden, um die Anforderungen zu verdeutlichen. Sollte das Ergebnis sein, dass das Tool mit künstlicher Intelligenz umgesetzt werden soll, kann außerdem noch eine Liste mit Anforderungen an das Datenset und die allgemeine Aufbereitung der Daten zusammengestellt werden.
Referenzen:
[APS14] Matteo Avalle, Alfredo Pironti, and Riccardo Sisto. Formal verification of security protocol implementations: a survey. In: Formal Aspects of Computing 26 (2014), pp. 99–123.
[Kan+20] Aditya Kanade et al. Learning and Evaluating Contextual Embedding of Source Code. In: Proceedings of the 37th International Conference on Machine Learning. Ed. by Hal Daumé III and Aarti Singh. Vol. 119. Proceedings of Machine Learning Research. PMLR, July 2020, pp. 5110–5121.
[PSS98] Amir Pnueli, O Shtrichman, and M Siegel. The Code Validation Tool(CVT). In: International Journal on Software Tools for Technology Transfer(STTT) 2.2 (1998), pp. 192–201.
[Sam+21] Michael Sammler et al. RefinedC: automating the foundational verification of C code with refined ownership types. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2021. Virtual, Canada: Association for Computing Machinery, 2021, pp. 158–174.
Vergleich von automatischen Tools zur Verifizierung von Sicherheitsbeweisen
Da rigorose Beweise über die Sicherheit von kryptographischen Protokollen oft aufwändig sind (für erste einfache Beispiele siehe [KL20]), gibt es einige automatische Tools, die solche Sicherheitsbeweise zumindest verifizieren oder sogar (teilweise) selbst erstellen können. Beispiele für solche Tools sind ProVerif [Bla+18], Scyther [Cre08] und Tamarin Prover [Mei+13]. Einen Vergleich zwischen Scyther und Tamarin findet man z.B. unter [LPL24].
Ziel dieser Arbeit ist es, eine umfassendere Übersicht über vorhandene Softwaretools zum Beweisen von Sicherheitseigenschaften zu geben. Hierbei sollen sowohl quantitative Werte wie Ausführungszeit und die Korrektheit der Ergebnisse als auch qualitative Werte wie die Bedienbarkeit und Übersichtlichkeit verglichen werden. Um letzteres verständlich zu machen, soll ein kryptographisches Protokoll in einigen ausgewählten Tools untersucht werden. Dafür ist zunächst eine Beschreibung des Protokolls in einer formalen Sprache passend zu den Tools notwendig, welche ebenfalls knapp erläutert werden soll. Geeignete kryptographische Protokolle sind z.B. Schlüsselaustauschprotokolle (z.B. Diffie-Hellman [DH76] oder Needham-Schroeder-Lowe [NS78;Low96]) mit anschließender Verwendung des Schlüssels.
Die verschiedenen formalen Sprachen sollen ebenso als Teil der Übersicht verglichen werden. Hierfür eignet es sich, zunächst das gewählte Protokoll allgemein zu beschreiben und es dann in mehrere formale Sprachen zu übersetzen.
Referenzen:
[Bla+18] Bruno Blanchet et al. ProVerif 2.00: automatic cryptographic protocol verifier, user manual and tutorial. In: Version from (2018), pp. 05–16.
[Cre08] Cas JF Cremers. The scyther tool: Verification, falsification, and analysis of security protocols: Tool paper. In: International conference on computer aided verification. Springer. 2008, pp. 414–418.
[DH76] W. Diffie and M. Hellman. New directions in cryptography. In: IEEE Transactions on Information Theory 22.6 (1976), pp. 644–654.
[KL20] J. Katz and Y. Lindell. Introduction to Modern Cryptography. CRC Press, 2020.
[Low96] Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Springer. 1996, pp. 147–166.
[LPL24] Thi Minh Chau Le, Xuan Thang Pham, and Vinh Thinh Le. Advancing Security Protocol Verification: A Comparative Study of Scyther, Tamarin. In: Journal of Technical Education Science 19.Special Issue 01 (Feb. 2024), pp. 43–53.
[Mei+13] Simon Meier et al. The TAMARIN prover for the symbolic analysis of security protocols. In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. Springer. 2013, pp. 696–701.
[NS78] Roger M Needham and Michael D Schroeder. Using encryption for authentication in large networks of computers. In: Communications of the ACM 21.12 (1978), pp. 993–999.
Systematic Literature Review and Evaluation of Differential Privacy for Mobility Traces
Location-aware services are increasingly used, for instance in fitness trackers, search engines or autonomous vehicles. However, spatial data can reveal sensitive information about individuals such as their home address, workplace or hobbies. This risk is pronounced for mobility trace data: A time series of a single individual's location. Mobility traces are highly correlated, e.g. because individuals exhibit similar movement patterns every day. It is also fine-grained: The location is reported in the scale of seconds. Accordingly, preserving the privacy of users is challenging.
The state of the art method for preserving privacy in data releases is differential privacy [1]. Intuitively, differential privacy bounds the information gain caused by an individual's participation in a data set. While differential privacy typically assumes that there is exactly one data point per individual, the concept has also been expanded to location data and mobility traces.
This thesis aims to systematically review the literature on differentially private approaches to using or publishing mobility trace data. The decision whether data releases, e.g. when publishing research data, or data usage, e.g. when implementing a location-aware service, is focused is left to the candidate's discretion. This thesis's second objective is evaluating selected approaches either theoretically or empirically. This decision is also left to the candidate. A theoretic evaluation might involve the creation of a taxonomy of all reviewed approaches and comparing their formal properties and assumptions. An empiric evaluation entails implementing some approaches and applying them to open data sets in an experimental setting. In overall, this thesis should focus on identifying and comparing different strategies to achieve differential privacy given the unique challenges of mobility traces.
[1]: Dwork, C. (2006). Differential privacy. In M. Bugliesi, B. Preneel, V. Sassone, & I. Wegener (Eds.), Automata, languages and programming (pp. 1–12). Springer Berlin Heidelberg.