Desaster in der Software-Sicherheit (WiSe 2015/16)
| Veranstaltungstyp: | Proseminar | ||
|---|---|---|---|
| Zielgruppe: | Bachelor Informatik | ||
| Lehrstuhl: | Anwendungsorientierte Formale Verifikation; Logik und Formale Methoden | ||
| Dozierende: |
Prof. B. Beckert |
||
| SWS-Anzahl: | 2 | ||
| ECTS: | 3 | ||
| Semester: | Wintersemester 2015/2016 | ||
| Raum: | Gebäude 50.34, SR 236 | ||
| Termine: |
21.10.2015, 13-14 Uhr in SR 236, Auftaktveranstaltung 10.12.2015, 16:00 - 18:30 Uhr in SR 301 (Gebäude 50.34), Zwischenvorträge 01.02.2016, 09:30 - 15:30 Uhr in SR 301 und SR 010 (ab 12:30 Uhr), Hauptvorträge 08.02.2016, 10:00 - 16:30 Uhr in SR 148 (Gebäude 50.20) und SR 010 (ab 13:00 Uhr), Hauptvorträge |
||
| Anmeldung: | Persönlich oder per E-Mail bei Frau Meinhart, Raum 223, simone.meinhart@kit.edu | ||
| Platzvergabe: |
Reihenfolge nach Eingang der Anmeldung
Alle Plätze vergeben (21.08.2015)
|
||
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
Vorträge
- Buffer-Overflow Angriffe (AW)
Pufferüberläufe (englisch buffer overflow) gehören zu den häufigsten Sicherheitslücken in aktueller Software, die sich u. a. über das Internet ausnutzen lassen können. Im Wesentlichen werden bei einem Pufferüberlauf durch Fehler im Programm zu große Datenmengen in einen dafür zu kleinen reservierten Speicherbereich – den Puffer – geschrieben, wodurch nach dem Ziel-Speicherbereich liegende Speicherstellen überschrieben werden.
-- de.wikipedia.orgBuffer Errors sind nach [1] der häufigste Schwachstelle mit kritischer Einstufung. In diesem Seminarthema sollen Buffer Overflow Angriffe erläutert werden. Dabei sollten folgende Fragen beantwortet werden:
- Was ist ein Buffer Overflow?
- Wie werden solche Schwachstellen ausgenutzt?
- Welche Techniken zur automatischen Finden von solchen Schwachstellen existieren?
- Patriot Rocket Disaster (MH)
Am 25. Februar 1991 versagte das Patriot-Raketenabwehrsystem, das während des ersten Golfkrieges in Dhahran, Saudi Arabia stationiert war. Eine ankommende irakische Scud-Raketen wurde vom System nicht erkannt und nicht abfangen. Diese Rakete traf daraufhin eine Baracke der US-Army und töte 28 Menschen. Schuld an diesem Fehlverhalten war ein Softwarebug: Sein Grund ist ein Problem beim Speichern von Zeit in einem 24-bit Register. Sie wurde als Fixed-Point-Zahl mit einer Akkuranz von 1/10s gespeichert. Die Präzision des Registers reichte jedoch nicht aus, um die Zeit so zu speichern und der Fehler konnte sich über die Zeit akkumulieren, bis die Abweichung nach einigen Stunden schließlich zu groß war und das System nicht mehr funktionierte. In diesem Seminar soll die Literatur zu diesem Desaster recherchiert werden und über den konkreten Vorfall hinaus, Bugs mit Dezimalberechnungen beleuchtet werden und ggf. die Möglichkeiten, diese im Entwurf zu vermeiden.
- Android Malware (VK)
Malware ist ein Computerprogramm, das entwickelt wurde, um vom Benutzer unerwünschte und gegebenenfalls schädliche Funktionen auszuführen. Mit der steigenden Popularität von mobilen Android-Geräten steigt auch die Verbreitung von Android-Malware und das Interesse an Antimalware-Maßnahmen. Das Seminar soll sich mit Android-Malware und Techniken zu deren Entdeckung oder Prävention beschäftigen. Der Fokus liegt dabei auf Techniken, die statische Programmanalyse verwenden.
- Knightmare on Wall Street (DG)
Das Börsenparkett wird heutzutage von automatisierten Handelssystemen dominiert. 2012 kam es an der New Yorker Börse zur Katastrophe als ein fehlerhaftes System unkontrolliert Kauf- und Verkaufanweisungen verbreitete. Der Betreiber Knight Capital Group verlor dadurch rund 440 Millionen USD innerhalb von 45 Minuten. Der Fehler bestand darin, dass eine bisher nicht genutzte Softwarekomponente durch ein Update des Systems aus Versehen aktiviert wurde. Da diese Komponente nicht genutzt wurde, war sie auch nicht für Tests berücksichtigt worden.
- Taint Analysis für Android Apps (SG)
Mobile Geräte, wie Beispielsweise Mobiltelefone enthalten sehr viele private und sensible Informationen des Benutzers. Gleichzeitig bieten sie eine Plattform an, auf der Software von fremden Herstellern ausgeführt werden können und sollen. Auf welche Weise Apps auf sensible Informationen zugreifen können und wie sie damit umgehen ist in der Regel kaum zu durchblicken. Das Ziel von Taint Analyse ist es, Software statisch zu analysieren um so Informationlecks aufzuspüren. Hierfür werden Eingabeinformationen als sensibel markiert und ihr Weg durch die Programmausführung beobachtet. Ziel dieser Proseminararbeit ist es, am Beispiel des Frameworks FlowDroid, Taint Analysis als Methode zu Informationsflussanalyse vorzustellen, sowie deren Vorteile und Limitierungen im Vergleich zu anderen Methoden herauszuarbeiten.
Literatur: [1]
- Secure Multi-Execution (SG)
Statische Methoden zur Programmanalyse zeichnen sich durch meist präzise Analyseergebnisse aus, sowie durch Vollständigkeitseigenschaften. Insbesondere sind solche Methoden besonders dann geeignet, wenn der Quellcode eines Programms vorzeitig vorliegt. Viele Webseiten liefern mittels Java Script jedoch Programme aus, die sofort nach dem Laden ausgeführt werden sollen. Meist ist die einzige Alternative zur Ausführung eines fremden Programmes das Abschalten von Java-Script, was viele Webseiten unbenutzbar macht. Alternativ bietet die Methode Secure Multi-Execution eine Möglichkeit, dynamisch sicherzustellen, dass Java-Script Code keine persönlichen Daten an fremde Server übermittelt. Dennoch ist die Methode schnell genug um innerhalb eines Browsers angewendet werden zu können und korrekt in dem Sinne, dass keine Geheimnisse verraten werden können. Ziel dieser Seminararbeit ist es die Methode “Secure Multi-Execution” vorzustellen und die Theorie dahinter ausreichend zu erläutern, sowie Anwendungsbereiche vorzustellen. (Voraussetzung ist Interesse an mathematischen Formalismen!)
- Storing Passwords (AW)
Immer wieder werden Internetseiten korrumpiert und sensible Informationen wie die Kundenpasswörter rausgetragen. Das letzte öffentlichwirksame Beispiel ist der Hack von Ashley Madison, einer Datingseite [1]:
“[..], dass es Jahrhunderte dauern würde, alle 36 Millionen Passwörter der Nutzer zu knacken. Wie sich jetzt herausstellte, schafft man das bei über 15 Millionen der Passwörter in ein paar Wochen.”
Das sichere Speichern von Passwörter, die auch nach einem Angriff nicht brechen, ist ein wichtiger Kern jeder Webseite mit einer Userauthentifzierung. Im Kern dieser Seminar soll der Seminarist die sichere Speicherung von Passwörtern erarbeiten.
- Replacing Testing with Formal Verification (MU)
In früheren Zeiten war Testen das einzig probate Mittel zur Sicherstellung funktionaler Korrektheit von neu entwickelten Prozessoren. Im Jahr 1994 wurde durch das Auftreten des FDIV-Bugs (ein 500 Mio$ teures Desaster) bei den damalig aktuellen Pentium-Prozessoren klar, dass Testen alleine auch realistiche Fehler nicht immer aufdecken kann. Seither hat es viel Forschung gegeben zur formalen Verifikation von Hardware, die Firma Intel hat viele der Forschungsergebnisse in die Praxis umgesetzt. Ziel dieser Seminararbeit ist es, die Problematik vorzustellen (anhand von FDIV z. B.) und einige wenige verwendete Techniken ausführlicher vorzustellen.
Literaturrecherche ist Teil der Arbeit, Ausgangsliteratur ist: Springer
- Treiberverifikation mit SLAM (SaG)
Eine Quelle für Blue Screens (Systemausfälle aufgrund von fatalen Systemfehlern) unter Windows ist fehlerhafte Treibersoftware. Um sicherzustellen, dass das Zusammenspiel zwischen der Treibersoftware und dem Betriebssystem funktioniert gibt es im Microsoft Driver Development Kit einen Static Driver Verifier. Mit diesem kann die Treibersoftware überprüft werden. Ziel des Seminarvortrags ist es, das im Microsoft-Projekt SLAM entwickelte Verifikationsprinzip vorzustellen, mit dem es möglich ist Treibersoftware statisch zu überprüfen. Außerdem sollen die Erweiterungen der Technik erläutert werden.
- ASLR, its Failures, and Related Measures (VK)
Address Space Layout Randomization (ASLR) ist eine Technik, die die Ausnutzung von Sicherheitslücken in Computersystemen erschwert. Durch ASLR werden Adressbereiche den Programmen auf zufälliger Basis zugewiesen, wodurch ein Angreifer mehr Aufwand betreiben muss, um die Speicherstellen zu finden (z. B. den Stack), die für die Ausnutzung der Sicherheitslücke wichtig sind. Das Seminar soll die Technik vorstellen, sowie sich mit deren Effektivität, Schwächen, und Weiterentwicklungen auseinandersetzen.
- Cryptocurrencies and Attacks on Them (VK)
Kryptowährungen sind moderne digitale Zahlungsmittel. Bei ihnen werden Prinzipien der Kryptographie angewandt, um ein verteiltes, dezentrales und sicheres, digitales Zahlungssystem zu realisieren. In dem Seminar soll das Konzept Kryptowährung kurz vorgestellt werden, und dann Angriffe auf das Konzept oder bestimmte Teile der Infrastruktur erörtert. Ein möglicher Schwerpunkt wären dabei Schwachstellen in kryptographischen Protokollen, die durch Verwendung von Zufallszahlen von schlechter Qualität entstehen.
- How much testing is enough? (TB)
Softwaretests sind ein wichtiger Bestandteil der Software-Qualitätssicherung. Um die Qualität einer Testsuite zu beurteilen, werden dabei oft Metriken verwendet, die angeben, welcher Teil des Programms durch die Tests abgedeckt wird. Welche Aussagekraft hat aber ein erfolgreicher (oder fehlgeschlagener) Testlauf mit einer bestimmten Testabdeckung bezüglich der Zahl der in der Software vorhandenen Defekte? Wie viele Testfälle bzw. Testläufe sind notwendig, um mit einer gewissen Wahrscheinlichkeit davon ausgehen zu können, dass die Software in der Praxis fehlerfrei arbeitet? Dieser Seminarvortrag soll Verfahren vorstellen, die es erlauben solche Abschätzungen vorzunehmen.
- Voting Paradoxes (MK)
Wahlverfahren sind Methoden, individuelle Präferenzen zu einer aggregierten Wahlentscheidung zu kombinieren. Dies ist häufig nicht so einfach und birgt eine oftmals unerwartete Komplexität, die zu paradoxen Effekten führen kann. Beispielsweise entschied das Bundesverfassungsgericht am 3. Juli 2008, dass das damalige Bundestagswahlverfahren verfassungswidrig war. Es konnte passieren, dass eine größere Zahl an Zweitstimmen für eine Partei dieser eine geringere Zahl an Sitzen verschaffen konnte (negatives Stimmgewicht), was gegen das Grundgesetz verstößt. Infolgedessen wurde im Bundeswahlgesetz 2011 die Möglichkeit von Ausgleichsmandaten eingeführt. Im Rahmen des Proseminars sollen ausgewählte grundlegende Kriterien für korrekte Wahlverfahren analysiert und deren Zusammenhang dargestellt werden.
Literatur
"Automated Reasoning in Social Choice Theory: Some Remarks" (Siddharth Chatterjee and Arunava Sen, 2014)
"Logic and Social Choice Theory" (Ulle Endriss, 2011) - Sichere elektronische Wahlen (MK)
Heutzutage werden vielerorts demokratische Wahlen elektronisch und teilweise sogar inklusive einer Stimmabgabe per Internet durchgeführt. Prominente Beispiele sind Estland, Brasilien und Indien. Elektronische Wahlen sollen den demokratischen Prozess einer vernetzten Gesellschaft ermöglichen bzw. verbessern. Jedoch birgt die Durchführung elektronischer Wahlen auch einige potentielle Gefahren, die das Vertrauen in die Wahlen und ihr Ergebnis ernsthaft gefährden können. Im Rahmen des Proseminars soll eine Übersicht über Gefahren elektronischer Wahlen gegeben sowie eine einfache Angriffsmöglichkeit auf verschiedene existierende E-Voting-Systeme veranschaulicht werden.
Literatur
"Principles and requirements for a secure e-voting system" (Dimitris A. Gritzalis, 2002)
"Clash Attacks on the Verifiability of E-Voting Systems" (Ralf Küsters, Tomasz Truderung and Andreas Vogt, 2012)