Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Herzlich willkommen zur letzten Sitzung des Semesters. Scheinen einige schon in Ferien zu

sein. Zur Feier des Tages habe ich, ich bin stolz, dass ich das erste Mal jetzt hinkriege,

meine Notizen vergessen. Mal sehen, wie es geht. So, wir beginnen damit, dass ich Werbung mache.

Und noch mal meinen Rechner aufklappe, damit ich die Ansagen nicht vergesse,

dass die Herrlerin mir aufgetragen hat. Moment.

So, also zuerst die angekündigte Werbung. Und zwar für die Wahlpflichtveranstaltung

oder Wahlveranstaltung des Lehrstuhls 8. Nächstes Semester. So, ich muss jetzt auswendig können.

Also wir bieten an, wie jedes Wintersemester eine Veranstaltung namens Ontologien im Semantic Web.

Es geht im Wesentlichen um einen Kurs in Beschreibungslogik plus ein paar anderen

Dingen, also in Ontologiesprachen, die man verwendet, um Dokumente zum Beispiel im Web,

aber auch eigentlich noch stärker heutzutage stand alone zu semantisieren. Semantisieren heißt,

ich nehme Wikipedia und wenn da steht Angela Merkel ist Kanzlerin der Bundesrepublik Deutschland,

dann habe ich da Konzepte dran stehen, die mir erklären, was ein Kanzler ist und in welcher

Relation er zum Parlament steht und wer ihn wählt und so weiter. Also das mache ich selbst. Ich könnte

jetzt Uhrzeiten angeben, die kann ich sogar auswendig. Typischerweise sind diese Veranstaltungen so

gemütlich, dass wir uns die Uhrzeiten so ein bisschen untereinander absprechen können,

machen wir regelmäßig. Also wenn Sie im Unibus Zeiten sehen, zu denen Sie nicht können,

dann melden Sie mich an oder tauchen Sie kurz zur ersten Veranstaltung auf, so was in der Richtung,

setzen wir einen Doodle auf und versuchen das entsprechend zu arrangieren.

Dann, formale Methoden der Softwaretechnik, ebenfalls eine regelmäßige Veranstaltung.

Da geht es um Verifikation von Software. Formale Methoden heißt immer, ich benutze,

ich mache das Wort nicht sagen, mathematisch und betonen, um Software zu analysieren,

insbesondere auf Korrektheit. Das zerfällt in zwei Teilen und zwar Verifikation sequenzieller

Software und Verifikation paraleler oder reaktiver Software. Für das erste verwenden wir ein Tool

namens Daphne. Zu unserer Schande muss ich gestehen, das ist ein Tool von Microsoft,

aber es funktioniert eben vergleichsweise gut. Insbesondere hat es eine gute Anwendung an diesen

Microsoft Z3 SMT-Solver. Das ist also praktisch eine Sprache, in der man Java ähnlich programmiert.

Man annotiert dann das Programm mit Korrektheitsbedingungen und wenn man das richtig gemacht

hat und ein bisschen Gefühl dafür entwickelt, was man da hinschreiben kann und was nicht,

dann wird also das Tool, was dahinter steht, die Korrektheit dann automatisch, also Korrektheit

bezüglich dieser Annotationen automatisch verifiziert. Für den reaktiven Teil, wo es also um

nebenläufige Systeme geht, verwenden wir wesentlich ehrenhafter eine Open Source Variante von SMV,

dem sogenannten New SMV. Das ist ein Model Checker, der also in der Lage ist, in einem

bestimmten Formalismus aufgeschriebene parallele Systeme, wo ich halt Prozesse, in denen man da

herlaufen lasse, die Variablen manipulieren, so ungefähr zu checken gegen temporale Spezifikationen.

Du machst doch, wenn ich irgendwann mal eine Request abschicke, kommt auch irgendwann mal ein

Acknowledgement zurück und sowas. Und neu, also ich vergaß, wen das nach der Familie ist unter

Deo Schlietag. Und als neue Veranstaltung gibt es eine Veranstaltung namens Kryptologie und

Verifikation von Protokollen. Das heißt, da geht es um alle NSA-relevanten Probleme. Also erstens

Kryptologie, wie gehe ich vor, wenn ich Dinge verschlüsseln will, was für Algorithmen kann ich

anwenden. Und zweitens Protokollverifikation, was eben so ein zweites Problem ist, ja gut selbst,

wenn ich annehme, dass meine Kryptographie an sich einwandfrei funktioniert und keiner in der

Lage ist, meinen Schlüssel zu knacken und sowas, ja dann gibt es ja immer noch bekannte Probleme,

die darin bestehen, dass einfach der Ablauf des Schlüsselaustausches, des Nansenaustausches,

was wird verschlüsselt, was wird Klartext verschickt, an wen, ja nicht, das ist alles,

was eben in seinem Krypto-Protokoll festgelegt ist. Das kann man auch falsch machen und das wird seit

Ewigkeiten immer wieder falsch gemacht. Berühmt ist das Beispiel, das sogenannte Needham-Schroeder-Protokoll,

das also für einen Schlüsselaustausch, das also lange Zeit hochgehalten worden ist, bis jemand

festgestellt hat, naja, da gibt es einen Man in the Middle Attacke und wenn der sich richtig verhält,