Es werden maximal die 10 unten aufgeführten Themen nach dem Prinzip First Come, First Served vergeben. Um am Seminar teilzunehmen, schicken Sie eine Mail mit ZWEI Themenwünschen an philip.lenzen@informatik.uni-augsburg.de.
Folgende Seminarthemen werden angeboten:
Themenblock 1: Exploits
1. Angriffe auf Signaturen von PDF-Dokumenten
Das "Portable Document Format" (PDF) ist de-facto Standard für elektronische Dokumente, unter anderem für elektronische Verträge und Rechnungen im Staats- und Finanzwesen. Zur Sicherung der Authentizität und Integrität von PDF-Dokumenten werden Digitale Signaturen eingesetzt. Allerdings ist eine Vielzahl an PDF-Viewern verwundbar hinsichtlich neuartiger Angriffe auf Signaturen, die Forscher der Ruhr-Universität Bochum entdeckt haben. Diese sollen im Rahmen dieser Arbeit näher untersucht werden.
2. Automatische Heap-basierte Exploit-Generierung
Typische Ansätze der automatisierten Generierung von Exploits (Befehlsketten, die aufgrund von Speicherkorruption beliebigen Angreifercode ausführen können), erzeugen meist Stack-Overflow und Format-String Exploits (z.B. [1]). Neuere Forschungsarbeiten beschäftigen sich unter anderem auch mit der Manipulation des Heap Layouts, um bpsw. Heap-Overflow Exploits generieren zu können. Diese Arbeit soll die verschiedenen Techniken und deren Limitierungen der Stack- und Heap-Exploit-Generierung genauer untersuchen.
Themenblock 2: Application Security
3. Sicherheitsmetriken für Control-Flow Integrity
Ein großer Teil der Sicherheitslücken in modernen Systemen basieren auf Speicherkorruption in low-level Programmiersprachen wie C oder C++. Durch Übernahme des Kontrollflusses kann ein Angreifer unerwünschtes Verhalten bis hin zur Ausführung beliebigen Codes erzwingen. Dagegen wurden verschiedene Defensivmechanismen basierend auf Control-Flow Integrity entwickelt, und für diese wiederum diverse Metriken zum Bewerten der Sicherheitsgarantien. Einige davon sollen im Rahmen dieser Arbeit verglichen werden.
4. Symbolic Execution in der Sicherheitsanalyse
Symbolische Ausführung ist eine Technik zur Programmanalyse, bei der das Programmverhalten durch mathematische Constraints über symbolischen statt konkreten Eingabewerten repräsentiert wird. Typischerweise wird diese Technik zur Testfallgenerierung und Fehlererkennung eingesetzt - allerdings kann sie auch in der Sicherheitsanalyse eingesetzt werden. Diese Arbeit soll unterschiedliche Ansätze der symbolischen Ausführung genauer beleuchten.
Themenblock 3: Blockchain Security
5. Hybrides Fuzzing von Smart Contracts
Smart Contracts sind Programme, die innerhalb einer Blockchain ausgeführt werden können, um komplexe Funktionalität umzusetzen. Einmal veröffentlicht, können sie jedoch nicht mehr geändert werden. Um Bugs vor der Veröffentlichung finden zu können, wird unter anderem Fuzzing eingesetzt, welches mittels Zufallseingaben Fehler provoziert. Im Rahmen dieser Arbeit sollen verschiedene Smart Contract Fuzzer untersucht werden.
6. Interoperabilität heterogener Blockchains
Der Siegeszug der Blockchain offenbart zwei Probleme dieser Technologie: Einerseits treten Skalierbarkeitsprobleme bei großen "permissionless" Blockchains auf, anderererseits entwickeln sich isolierte "permissioned" Blockchains (die z.B. in der Industrie genutzt werden) zu einer Form der zentralisierten Datenbank. Aus beiden Gründen ist Interoperabilität zwischen unterschiedlichen Blockchains notwendig, die jedoch die grundsätzlichen Sicherheitseigenschaften der einzelnen Blockchains nicht verletzt. Dafür entwickelte Verfahren und Techniken sollen in dieser Arbeit genauer betrachtet werden.
Themenblock 4: Trust & Privacy
7. Schutz physischer Interfaces in Cyber-Physical Systems
Statt rein mechanischer Systeme finden sich heutzutage vor allem Verbundsysteme aus softwaretechnischen und mechanischen bzw. elektronischen Komponenten, sogenannte cyber-physische Systeme, in Bereichen wie der Hausautomatisierung, Verkehrs- und Versorgungsinfrastruktur. Speziell die Schnittstellen zwischen softwaretechnischen und mechanischen Komponenten ermöglichen neue Angriffsvektoren für lokale und Remote-Angreifer. In dieser Arbeit sollen verschiedene Ansätze zur Absicherung physischer Interfaces für eingebettete Systeme untersucht werden.
8. Schutz der Intellectual Property in Machine-Learning-Modellen
Machine Learning, allen voran Neuronale Netze, erlebten in den letzten Jahren einen Hype. Da immer mehr Unternehmen aus unterschiedlichen Bereichen mittels "KI" versuchen, ihre Produkte innovativ zu gestalten, wird aktiv an Möglichkeiten geforscht, die Modelle robuster gegen sogenannte Adversarial Attacks zu machen. Speziell im Kontext der Industrie sind aber auch Privacy-Überlegungen relevant, um das geistige Eigentum (sowohl in den Trainingsdaten als auch im Netz selbst) zu schützen. Im Rahmen dieser Arbeit sollen verschiedene Ansätze zum Schutz der Intellectual Property in Machine Learning Modellen untersucht werden.
Themenblock 5: Verifikation
9. Automatische Protokollverifikation mit Tamarin
Sicherheitsprotokolle weisen immer wieder subtile Fehler auf, die oft erst nach Jahren des Einsatzes gefunden werden. Eine Möglichkeit, solche Fehler zu vermeiden, ist die formale Verifikation mit spezialisierten Tools, die automatisch analysieren, ob Angriffe möglich sind. Tamarin ist ein aktuelles Werkzeug zur Modellierung und Verifikation von Sicherheitsprotokollen. Die Arbeit soll untersuchen, wie und welche Security Protokolle mit Tamarin modelliert/verifiziert werden können, und ein wenig auf die Grundlagen eingehen.
10. Formale Verifikation von Smart Contracts
In den letzten Jahren haben Blockchain Technologien vermehrt die Aufmerksamkeit von Industrie und Forschung auf sich gezogen.
Für die Sicherheit von Blockchain-basierten Prozessen ist die Korrektheit von sogenannten Smart Contracts essenziell, weshalb verschiedene Methoden erarbeitet wurden, solche Smart Contracts zu verifizieren.
[2] betrachtet beispielsweise die formale Verifikation von Smart Contracts mit dem Tool Isabelle/HOL, aufbauend auf einem formalen Modell der Ethereum Virtual Machine (EVM). Ziel der Arbeit ist es, einen Überblick über aktuelle Ansätze zur formalen Verifikation zu geben und dabei insbesondere genauer auf den in [2] vorgestellten Ansatz einzugehen.
