Wintersemester 2014/15
Desaster in der Software-Sicherheit
| Veranstaltungstyp: | Proseminar |
|---|---|
| Zielgruppe: | Bachelor Informatik |
| Lehrstuhl: | Anwendungsorientierte Formale Verifikation; Logik und Formale Methoden |
| Dozierende: |
Prof. B. Beckert |
| SWS-Anzahl: | 2 |
| ECTS: | 3 |
| Semester: | Wintersemester 2014/2015 |
| Raum: | wird hier rechtzeitig bekanntgegeben |
| Termine: |
22.10.2014, 13-14 Uhr in SR 236, Auftaktveranstaltung Termine der Hauptvorträge: 28.01.15, 13:00-19:30 Uhr, Raum 348 (7 Vorträge) 29.01.15, 15:45-17:15 Uhr, Raum 301 (2 Vorträge) 04.02.15, 09:45-11:15 Uhr, Raum 010 (2 Vorträge) |
| 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.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.
Folien
Einführungsveranstaltung vom 22.10.2014 (Organisatorisches und Ablauf des Proseminars).Vorträge
- 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.
Literatur: [1] - [2] - [3] - [4] - 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: [1] - Angriff auf das Needham-Schroeder-Protokoll (SG)
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: [1] - Seitenkanal-Angriffe auf Netzwerke (SG, VK)
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.
Literatur: [1] (Artikel nur innerhalb des Uni-Netzes verfügbar) - [2] - 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.
Literatur: [1] u.a. - 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.
Literatur: [1] (innerhalb des KIT-Netzes) - [2] - [3] - 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.
- 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 - Angriffe auf Zufallszahlengeneratoren (VK)
Zufallszahlen sind wichtig für viele sicherheitskritische Anwendungen. Erzeugung von "guten" Zufallszahlen auf weitgehend deterministischer Hardware ist aber ein schwieriges Problem. Was man bei Pseudo-Zufallszahlengeneratoren alles falsch machen kann, hat dieses Thema zum Inhalt.
Literatur: [1] und, in wesentlich geringerem Umfang, [2], [3] - Angriffe auf elektronische Wahlverfahren (TB)
Elektronische Wahlen bringen neben ihren Vorteilen etwa in der Auszählung der Stimmen auch eine Vielzahl von neuen Problemen gegenüber der herkömmlichen Papierwahl mit sich. Der Einsatz elektronischer Wahlsysteme in der Praxis zeigt, dass die aktuellen Lösungen oft nicht ausgereift sind.
In diesem Vortrag sollen Anforderungen an ein Wahlverfahren skizziert und mögliche Probleme elektronischer Wahlverfahren beispielhaft dargestellt werden. Eine Möglichkeit die Korrektheit der Auszählung bei einer elektronischen Wahl sicherzustellen, ist mit Hilfe kryptographischer Verfahren einen Beleg zu generieren, anhand dessen überprüft werden kann, ob eine Stimme korrekt gezählt wurde. Beispiele für solche Wahlverfahren sind Bingo Voting, oder Prêt à Voter.
- Analyse von Softwareproblemen im Zusammenhang mit Flugunfällen (CG)
Software spielt eine zentrale Rolle in der Flugzeugsteuerung und daher auch bei Vorfällen und Unfällen im Flugbetrieb, wie z. B. das unkontrollierte Manöver einer Boeing 777-200 am 1. August 2005 oder beim Überlauf der Startbahn eines Bombardier Learjet 60 in 2008. Zu diesem Thema soll eine Fallstudie vorgestellt werden, welche diese und andere Vorfälle auf den Zusammenhang mit Software-Fehlern analysiert. In der Fallstudie werden Vorschläge gegeben, um Software-Robustheit zu verbessern. Diese sollen recherchiert und weiter ausgearbeitet werden.
Literatur: [1] [2] - Exploit Generation (CG)
Ein Exploit ist ein Programm oder eine Sequenz von Benutzeranweisungen, welches Schwachstellen in Software ausnutzt um unbeabsichtigtes oder ungewolltes Verhalten der Software zu verursachen. Da man mit formalen Softwareanalysetechniken Softwarefehler finden kann können diese auch verwendet werden um Exploits zu generieren. Zu diesem Thema kann entweder eine existierende Technik im Detail präsentiert werden, oder eine Übersicht an Techniken gegeben werden.
[1] [2] [3]