Modul Spezielle Kapitel Software-Engineering, Informatik (Master) (SPO 7)
Dieses Modul besteht aus den beiden Lehrveranstaltungen Codierungstheorie und angewandte Kryptographie. Im Rahmen dieses Moduls soll ein Verständnis sowohl für die Zielsetzung, als auch für die Methoden dieser beiden Gebiete erreicht werden. Die Teilnehmer sollen durch den Kurs in der Lage sein, die Methoden der beiden Gebiete zu verstehen und anwenden und die Sicherheit von Systemen einschätzen zu können. Insbesondere sollen Sie eine Beurteilungsgrundlage bekommen, um die Bedeutung von aktuellen Informationen/Nachrichten über die Sicherheit von Systemen richtig einschätzen zu können.
In der Codierungstheorie wird die Fragestellung behandelt, wie trotz fehlerhafter Übertragung korrekte Ergebnisse erzielt werden können. Dabei sind die zugrundeliegenden Fehler bzw. Fehlermodelle von der Übertragungstechnik abhängig. In der Kryptographie versucht man die Sicherheitsziele trotz bewusster Manipulationen durch einen Angreifer zu erreichen. Im einen Fall hat man es also mit gezielten Manipulationen, im anderen Fall mit mehr zufällig verteilten Fehlern zu tun. Diese zwei Gebiete haben also unterschiedliche, aber doch verwandte Zielrichtungen. Es kommen teilweise die gleichen Methoden zum Einsatz. Ein typisches Beispiel für den engen Zusammenhang stellt das moderne Verschlüsselungsverfahren AES dar. Bei einer der Teilfunktionen wird ein Code aus der Codierungstheorie verwendet um eine Funktion mit hoher Durchmischung (Diffusion) für den Einsatz in der Kryptographie zu bekommen.
In dieser Vorlesung werden die grundlegenden Methoden der Kryptographie vorgestellt. Dabei wird nach den einführenden Grundlagen der Schwerpunkt auf die Mechanismen gelegt, die typischerweise bei modernen Anwendungen zum Einsatz kommen.
Wesentliche Themen sind symmetrische Verschlüsselungsverfahren, insbesondere Blockchiffren (DES, AES), Modes of Operation (z.B. EBC, CBC), Hash-Funktionen, Message-Authentication-Codes, Public-Key-Verfahren (z.B. RSA, Diffie-Helman, ElGamal), Key-Management und elektronische Unterschriften.
Im weiteren Verlauf werden verschiedene, aktuelle Anwendungen der IT-Sicherheit, die auf dem Einsatz kryptographischer Verfahren beruhen, behandelt: E/Mail-Sicherheit (z.B. PGP, S-MIME), WWW-Sicherheit (SSL), Netzwerksicherheit (IP-SEC), Sicherheit von Web-Servern (Authentifikations-Mechanismen). Anhand dieser Beispiele werden wesentliche Grundprinzipien der IT-Sicherheit erläutert.
Ausführliche Folien werden im Intranet angeboten. Die Foliensätze der einzelnen Themen enthalten jeweils gesondert Literaturhinweise.
Einen Überblick bietet:
- Claudia Eckert: IT-Sicherheit. Konzepte - Verfahren - Protokolle, München, Oldenbourg Wissenschaftsverlag, 2013, 8. Auflage, ISBN 978-3-486-58270-3.
Die Lehrveranstaltung wird zu ca. 2/3 als Vorlesung durchgeführt. In der übrigen Zeit werden betreute Übungen durchgeführt, um die Techniken an praktischen Rechenbeispielen zu vertiefen.
Diese Vorlesung vermittelt das Grundwissen über Codes und Codierungen und die gängigen Algorithmen aus dem Gebiet der Quellen-, Kanal- und Leitungscodierung. Im Einzelnen werden Themen aus den folgenden Bereichen behandelt: Informations- und Codierungstheorie, Datenkompression, Fehlererkennende und -korrigierende Codes, Grenzen der Datenübertragung.
- PowerPoint-Folien
- Tafelmitschrift
- Übungsblätter
Vorlesungsteilnahme
SAT-Solving ist eines der wichtigsten allgemeinen Verfahren zur Lösung schwerer (oft NP-vollständiger) kombinatorischer Probleme. Diese treten in der Praxis in einer Vielzahl von Anwendungen auf, z.B.:
- Planungs- und Scheduling-Probleme in Lieferketten
- Konfiguration komplexer, variantenreicher Produkte, z.B. PKWs, LKWs, Flugzeuge
- Prüfung (Verifikation) von Hardware- und Software
- Erstellung von Spielplänen, z.B. in der Bundesliga
Dieses Modul soll Studierenden die theoretischen und schwerpunktmäßig praktischen Aspekte des SAT-Solving vermitteln. Behandelt werden:
- Grundlagen, historische Entwicklung
- Codierungen, z.B. cardinality constraints
- Phasenübergänge bei Zufallsproblemen
- Lokale Suche (GSAT, WalkSAT, ..., ProbSAT)
- Resolution, Davis-Putnam-Algorithmus, DPLL-Algorithmus, Look-Ahead-Algorithmus
- Effiziente Implementierungen, Datenstrukturen
- Heuristiken im DPLL-Algorithmus
- CDCL-Algorithmus, Klausellernen, Implikationsgraphen
- Restarts und Heuristiken im CDCL-Algorithmus
- Preprocessing, Inprocessing
- Generierung von Beweisen und deren Prüfung
- Paralleles SAT Solving (Guiding Paths, Portfolios, Cube-and-Conquer)
- Fortgeschrittene Anwendungen: Bounded Model Checking, Planen, satisfiability-modulo-theories
Auch die Einbindung von industriellen Anwendern (z.B. von Mercedes-Benz) ist vorgesehen.
In dieser Übung werden Verfahren der Vorlesung "Practical SAT Solving" anhand von Fragestellungen aus der Praxis erprobt und SAT-Solver zur Lösung von kombinatorischen Problemen eingesetzt.