Sommersemester 2014

Desaster in der Software-Sicherheit

Desaster in der Software-Sicherheit

Veranstaltungstyp:	Proseminar
Veranstaltungsnr.:	2400080
Zielgruppe:	Bachelor Informatik
Lehrstuhl:	Anwendungsorientierte Formale Verifikation; Logik und Formale Methoden
Dozierende:	Prof. B. Beckert Prof. P. H. Schmitt Thorsten Bormer Daniel Bruns Sarah Grebing Mihai Herda Vladimir Klebanov Christoph Scheben Mattias Ulbrich
SWS-Anzahl:	2
ECTS:	3
Semester:	Sommersemester 2014
Raum:	wird hier rechtzeitig bekanntgegeben
Termine:	22.04.2014, 13-14 Uhr in SR 236, Auftaktveranstaltung (weitere Termine nach Vereinbarung)
Anmeldung:	Bei Frau Meinhart, Raum 223, simone.meinhart@kit.edu

Thema

Spätestens nach den Enthüllungen durch Edward Snowden ist Sicherheit in Software-Systemen wieder ein großes Thema in den Medien. Trotz der üblichen Qualitätssicherungsmassnahmen in der Softwaretechnik hat es in der Vergangenheit schon vor diesen Enthüllungen Angriffe auf Software-Systeme gegeben.

Neben den üblichen Qualitätssicherungsmassnahmen wie bspw. Testen, existieren noch weitere modellbasierte und formale Methoden, die es erlauben Sicherheitslücken aufzudecken.

In diesem Proseminar werden verschiedene Angriffe auf Systeme und auch Methoden zum Aufdecken von Sicherheitslücken betrachtet.

Vorträge

1. SCADA (MH)

Supervisory Control and Data Acquisition(SCADA)[1] Systeme überwachen und steuern industrielle Prozesse (z. B. Fabriken und Energiekraftwerke) und Infrastruktur (z. B. Energie-, Wasser-, und Gasnetzwerke). Angriffe auf solche Systeme können enorme Schäden verursachen [2]. Mit Hilfe von modellbasierter Intrusion-Detection [3,4] kann man nicht autorisierte Zugriffe entdecken und verhindern.

[1] - [2] - [3] - [4]
2. Stuxnet (SG)

Stuxnet ist der komplexeste bisher bekannte Computervirus. Er wurde gezielt Entwickelt um Industrieanlagen zu beschädigen und hat die Haltung vieler Unternehmen zum Schutz von Industrieanlagen verändert. In diesem Vortrag geht es darum, ausgewählte Teile des Viruses vorzustellen.

Literatur
3. Angriff auf das Needham-Schroeder-Protokoll (t.b.a.)

Das Needham-Schroeder Public Key Protocol galt lange als sicheres Vorgehen um Schlüssel auszutauschen. Jedoch konnte mittels formaler Methoden wie Model Checking nachgewiesen werden, dass Man-In-The-Middle-Angriffe auf das Protokoll möglich sind. Mit den gleichen Verfahren kann auch nachgewiesen werden, dass eine leicht veränderte Version des Protokolls sicher ist. In diesem Vortrag geht es darum, den Nachweis des Angriffs und den Nachweis der Sicherheit des Veränderten Protokolls vorzustellen.

Literatur
4. Seitenkanal-Angriffe auf Netzwerke (t.b.a.)

Verschlüsselung ist eine gängige Technik, um Datenübertragung in öffentlichen Netzen zu sichern. Bei unsachgemäßem Gebrauch, können Angreifer jedoch verschlüsselte Inhalte anhand der Paketlänge u.ä. ganz oder teilweise entschlüsseln. Z. B. war es in einer älteren Skype-Version möglich, aus den verschlüsselten Datenpaketen mittels Spracherkennungsmethoden genügend Informationen zu gewinnen um Gespräche zum größten Teil zu rekonstruieren. In diesem Vortrag geht es darum, den Angriff auf verschlüsselte Datenströme sowie Gegenmaßnahmen vorzustellen.

(Artikel nur innerhalb des Uni-Netzes verfügbar)
5. Cross-Site-Scripting (CS)

Cross-Site-Scripting ist eine Technik, die Schwachstellen in Webapplikationen ausnutzt um Dritte anzugreifen. Sie ist eine der am häufigsten verwendeten Angriffsformen im Internet. In diesem Vortrag geht es darum die Angriffsform selbst sowie eine systematische Vorgehensweise (basierend auf statischer Analyse) zur Vermeidung von XSS-Schwachstellen in Webapplikationen vorzustellen.

Literatur: Secure Programming with Static Analysis (Brian Chess, Jacob West)
6. Seitenkanal-Angriffe mittels Prozessor-Cache (VK)

Ein Prozessor-Cache ist ein unverzichtbarer Bestandteil modernenr Computer. Da ein Cache jedoch eine geteilte Ressource ist, bietet er für böswillige Prozesse ein Möglichkeit, Geheimnisse anderer Prozesse auszuspionieren. Dadurch ist es dem Angreifer z. B. möglich, geheime AES-Schlüssel zu erbeuten. Im Seminarvortrag sollen die angriffe sowie Gegenmassnahmen präsentiert werden.

7. Informationslecks bei e-Passports (MU)

Moderne Pässe besitzen einen eingebetteten RFID-chip (radio-frequency identification, auf dem biometrische Daten der Inhaberin gespeichert sind. Der Zugriff auf diesen Chip erfolgt drahtlos, was ein Sicherheitsrisiko bedeuten kann, da eine Angreiferin mit dem Chip kommunizieren kann, ohne dass die Inhaberin es mitbekommt. Obwohl es Vorkehrungen gibt, unautorisierten Zugrtiff auf den Chip zu verhindern, wird hier gezeigt, dass es leicht ist, die Anwesenheit eines Passes zu entdecken und, mehr noch, seine Nationalität. Für die Tests, die das zu Tage brachten wurden auch formale Modelle von e-Passports-Protokollen verwendet.

Paper 1 -- Paper 2
8. Unerlaubter Information Flow in der Praxis (TB)

Der Schutz sensibler Benutzerdaten ist eine wichtige Aufgabe sicherer Software. Trotz üblicher Qualitätssicherungsmassnahmen in der Softwareentwicklung gelingt es Angreifern in der Praxis aber, etwa durch Ausnutzen von Designfehlern in Protokollen oder Implementierungsfehlern, an Daten zu gelangen, die nicht für sie bestimmt sind. Ein aktuelles, prominentes Beispiel für einen solchen Implementierungsfehler ist der Heartbleed Bug, der es einem Angreifer erlaubt, sensible Daten im durch die OpenSSL-Bibliothek genutzten Speicher auszulesen.

Um solchen Fehlern zu begegnen, kann der erlaubte Transfer von Informationen in Programmen durch Informationsflusseigenschaften beschrieben und mit Hilfe von formalen Methoden nachgewiesen werden.

Ziel des Vortrags ist es Konzepte zur formalen Beschreibung von Informationsflusseigenschaften von Programmen, sowie formale Methoden zum Nachweis solcher Eigenschaften vorzustellen. Eine Übersicht bietet [1]; eine konkrete Nachweismöglichkeit wird in [2] beschrieben.

9. Fehler im Collision Avoidance-Manöver (SaG)

Um einen Zusammenstoss zwischen zwei Flugzeugen zu verhindern existieren verschiedene Kollisions-Vermeidungs Flugmanöver. Der korrekte Ablauf dieser komplexen Protokolle ist unerlässlich für die Sicherheit im Flugverkehr. Mit dem Verifikationswerkzeug KeYmaera für Hybride Systeme wurde nachgewiesen, dass eines dieser Manöver, das roundabout-collision avoidance Manöver, fehlerhaft ist.

Weitere Informationen
10. Angriffe auf Zufallszahlengeneratoren (t.b.a.)

Aufgabenstellung

Für jeden Vortrag sind von den Studierenden die folgenden Aufgabenpunkte zu erledigen:

• Verstehen des Stoffes.
• Auswahl der Themen, die in dem Vortrag präsentiert werden sollen.
• Entscheidung wie die Themen präsentiert werden sollen.
• Erstellung der Folien für die Präsentation und gegebenfalls anderer Materialien.
• Der Vortrag selbst.