Sommersemester 2019 und Wintersemester 2019 / 2020
Simon Dierl, M.Sc.
Malte Mues, M.Sc.
Prof. Dr. Falk Howar
IT-Sicherheit ist im Moment ein omnipräsentes Thema: Immer größere Teile der Infrastruktur, die wir täglich nutzen, wird durch IT basierte Systeme gemanagt. Dadurch wird es in Zukunft immer wichtiger diese kritischen IT-Systeme vor unbefugten Zugriff und Missbrauch zu schützen.
Um IT-Systeme wirksam verteidigen zu können, muss man jedoch zunächst verstehen, in welcher Art und Weise diese überhaupt manipuliert werden können. Wie Schneier im ersten Kapitel seines Buches „Beyond Fear“ [13] darstellt, ist Sicherheit in erster Linie ein Trade-off zwischen Aufwand zur Manipulation und Aufwand zum Schutz vor Manipulation. Je nachdem, wie ein Anwender die Kosten auf beiden Seiten einschätzt, fühlt er sich bei der Verwendung des Systems sicher oder nicht.
Angehende IT-Sicherheitsexperten können deshalb nur sinnvolle Konzepte zum Schutz vor IT-Angriffen entwerfen, wenn sie in einem ersten Schritt lernen, wie ein Angreifer zu arbeiten und zu denken. Ein in der IT-Sicherheits-Community verbreiteter Ansatz, mit dem diese Fähigkeiten erworben werden, sind Capture the Flag (CTF)-Challenges [2, 5, 6]. In solchen Challenges übernehmen angehende Experten die Rolle eines Angreifers und müssen Sicherheitslücken in speziell präparierten Systemen finden und ausnutzen, um sich Zugang zu geschützten Informationen (der Flag) zu verschaffen.
Zunehmend werden in der Industrie Werkzeuge aus dem Bereich der formalen Methoden eingesetzt, um Sicherheitslücken automtisiert zu finden (z.B. [3]).
Das Ziel der PG ist es, mehrere didaktische Capture the Flag Challenges aufzubauen, die sowohl von manuell als auch automatisiert (mit Hilfe von formalen Methoden) gelöst werden können. Dabei soll der didaktische Fokus des Challenges sowohl auf der Vermitllung der jeweiligen Art von Schwachstelle, als auch auf der Vermittlung der passenden formalen Methode für die automatisierte Lösung liegen.
Um didaktische Capture the Flag Challenges zu entwerfen, sind drei Schritte notwendig. Zunächst muss man potentielle Schwachstellen identifizieren, dann theoretisch untersuchen, wie man diese entdecken und schließen kann bzw. vermeidet und zuletzt eine wirkungsvolle Abwehr umsetzen.
Bevor man sich mit der Entwicklung von Werkzeugen zur automatisierten Detektion von Sicherheitslücken auseinandersetzen kann, muss man verstehen, welche Klassen von Sicherheitslücken es gibt und wie Angriffe gegen diese funktionieren. Dazu sollen die Teilnehmerinnen und Teilnehmer der PG zunächst verschiedene didaktische CTFs aufarbeiten. Ein Beispiel für eine solche didaktische CTF ist der vom Open Web Application Security Project (OWASP) entwickelte Juice Shop; ein anderes Beispiel ist die didaktische CTF-Challenge der University of Birmingham [2].
Neben dem Wissen, welches in CTF erlebbar gemacht wird, gibt es auch verschiedene best practices, die in der Literatur beschrieben sind. Manche davon, wie die Prüfung von SQL-Eingaben, haben es zwar in das allgemeine Bewusstsein gebracht, sind aber trotz aller humoristischen Betrachtung nach wie vor ein ernstzunehmendes Problem (vgl. OWASP Top 10 List [11]). Weitere große Datenbanken, die zur Bestimmung von Mustern in Sicherheitslücken gesichtet werden sollen, sind das Common Vulnerabilities and Exposures (CVE)-Verzeichnisund das Common Weakness Enumeration (CWE)-Verzeichnis.
Nachdem man erkannt hat, was Sicherheitslücken sind, muss man diese zuverlässig finden, um sie ausnutzen oder vermeiden zu können. Hier gibt es verschiedene Ansätze im Bereich der (semi-)formalen Methoden, die in der PG betrachtet werden sollen. Für Automatenlernen mit der LearnLib [10] wurde z. B. erfolgreich gezeigt, dass diese geeignet ist, um Fehler in Protokollen zu finden [7]. Für Methoden, die auf Automatenlernen basieren, bleibt zu zeigen, dass die gelernten Modelle valide Hypothesen des echten Systemverhaltens sind, um zu voll formalen Methoden zu gelangen. Erste Schritte in diese Richtung wurden in [9] gezeigt.
Byron Cook diskutiert die Effektivität von formalen Methoden zur Detektion von Sicherheitslücken in Softwarekonfigurationen bei der Firma Amazon Web Services (AWS) [3]. Die PG könnte z. B. dem Beispiel von AWS folgen und versuchen, ein formales Model für TomCat- und Datenbankkonfigurationen zu entwerfen. Mit diesem könnten falsch konfigurierte Services identifiziert werden.
Byron Cooks Gruppe bei AWS hat ebenfalls gezeigt, dass Bounded Model Checking geeignet ist, um Sicherheitslücken zu finden bzw. Code zu härten [4]. Ein offenes Problem dabei, welches auch für Symbolic Execution Engines gilt, ist die Modellierung der Umgebung der analysierten Software. Je nach der zu analysierenden Software kann die Umgebung Hardware-Komponenten, Memory Mapper oder andere Bibliotheksfunktionen sein. Z. B. modelliert die symbolische Ausführung in KLEE [1] Aufrufe in die Standardbibliothek mit symbolischen Funktionen.
Die PG soll untersuchen, inwiefern diese Modelle automatisch aus vorhandenen Artefakten erzeugt werden können, um die Verifikation zu beschleunigen und die Anwendung in neuen Umgebungen zu vereinfachen, z. B. durch den Einsatz von Automatenlernen (s. o.). Es soll ebenfalls untersucht werden, ob Modellierung genutzt werden kann, um Umgebungsmodelle für eines der oben genannten Verfahren zu erstellen. Beispiele dazu wären die Beschreibung von Dateisystemen durch formale Spezifikationen in SibylFS [12] oder die Nutzung von Hybridautomaten [8] zur Beschreibung des Verhaltens von Hardwarekomponenten.
Neben den auf (semi-)formalen Methoden basierenden Werkzeugen sollen auch bestehende Sicherheits- und Penetrationstest-Anwendungen in der PG berücksichtigt werden. Die Studierenden sollen den Umgang mit BlackArch, Kali Linux, Metasploit und anderen klassischen Penetrationstest-Werkzeugen erlernen, die auf Heuristiken oder Brute-Force-Methoden basieren. Zusätzlich sollen vorhandene Source Code-Analyse-Tools wie Valgrind oder Compiler-Plugins in GCC und LLVM genutzt werden.
Das Ziel ist, all diese Werkzeuge zusammen mit formalen Methoden so in den Kontext zu setzen, dass die entstehende Kombination Penetrationstests automatisch ausführt. Sie soll möglichst viele Schwachstellen mit möglichst geringer Beteiligung des Nutzers finden.
Die reine Werkzeugentwicklung macht nur Sinn, wenn die Teilnehmer auch den geschaffenen Mehrwert zeigen können. Eine Möglichkeit zur Evaluation der Leistungsverbesserung ist die SARD Benchmark Suite des National Institute of Standards and Technology. Diese enthält bereits eine Sammlung von verschiedenen bekannten Softwaredefekten und auch eine virtuelle Maschine, in welcher Software mit dokumentierten Sicherheitslücken vorinstalliert wurde. Eine weitere Sammlung von CTF-VMs findet sich auf VulnHub.
Die bestehenden CTF Challenges sind meistens dazu gedacht, dass Menschen mit diesen für IT-Sicherheit sensibilisiert und ausgebildet werden sollen. Das Ziel der PG ist jedoch, dass die Studierenden versuchen möglichst viel von dem Prozess zu automatisieren und reproduzierbar zu machen. Dazu sollen die Studierenden aus den gesammelten Sicherheitslücken solche auswählen, die gut von verschiedenen Werkzeugen erkannt werden und daraus eine CTF-Challenge zur Evaluation von automatisierten Penetrationstestwerkzeugen bauen. Anschließend sollen die Studierenden ihre Werkzeugkette an den CTF-Challenges demonstrieren.
Folgende fundierten Kenntnisse sind für die Teilnahme an der Projektgruppe notwendig :
Folgende Kenntnisse sind für die Teilnahme an der Projektgruppe hilfreich, werden jedoch nicht vorausgesetzt:
Die Grundlagen für hilfreiche Kenntnisse werden im Laufe des Projekts vermittelt.
Die Minimalziele der PG sind:
Die Ergebnisse der Projektarbeit und die dabei erstellte Software sollen der Fakultät für Informatik uneingeschränkt für Lehr- und Forschungszwecke zur freien Verfügung stehen. Darüber hinaus sind keine Einschränkungen der Verwertungsrechte an den Ergebnissen der Projektgruppe und keine Vertraulichkeitsvereinbarungen vorgesehen. Die Teilnehmer der Projektgruppe erkennen jedoch die Dual-Use-Problematik bei der Entwicklung von Penetrationstest-Werkzeugen an und verpflichten sich, die Ergebnisse ausschließlich innerhalb der Grenzen des Strafgesetzbuches zu verwenden.