Kausale Beweisführung in NetKAT

• Antragstellerin: Dr. Georgiana Caltais
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2018 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 398056821

Das aktuelle Projekt zielt darauf ab eine Methodologie zu entwickeln für die Integration einer "kausalen" formalen Frameworks im Kontext von Software-definierten Netzwerken (SDN), das auf kontrafaktischer Argumentation beruht. SDN sind eine wichtige Entwicklung in der Industrie da sie das Abstraktionslevel über das hardware-orientierter Anwendungen hebt und damit die schnelle Inbetriebnahme neuer Anwendungen und Dienste ermöglicht.Wir planen NetKAT zu verwenden. Dabei handelt es sich um eine SDN-Programmiersprache die auf Grund ihrer soliden mathematischen Grundlagen an Beliebtheit gewinnt. Diese Grundlagen erleichtern die Entwicklung wettbewerbsfähiger Tools für die rigorose Analyse ihrer zugehörigen Programme. NetKAT ist so weit gereift, dass es möglich ist verschieden interessante Fragen zu beantworten, zum Beispiel im Bereich der Erreichbarkeit: "Kann Host A mit Host B kommunizieren? Kann jeder Host mit jedem anderen Host kommunizieren?" oder im Bereich der Security: "Gehen alle nicht-vertrauenswürdigen Daten durch das System zur Aufspürung von Eindringen, das sich auf C befindet?" Außerdem wird diese SDN Programmiersprache (NetKAT) bereits in der Praxis als Teil des Frenetic Netzwerk-Management Tool-Pakets verwendet.Das Ergebnis des erfolgreichen Projektes wird ein mathematisches Gerüst zur Fehlerfindung in Netzwerken enthalten. Wir zielen auf effiziente Fehlerfindung und Klärung von Ursachen von Fehlern in NetKAT-Anwendungen. Was ist der Aulöser und was ist die Ursache des fehlerhaften Verhaltens? Dies ebnet den Weg um Verantwortlichkeit in NetKAT formal zu beschreiben - auch aus industrieller Sicht eine wichtige Eigenschaft. Wir planen Fragen bezüglich realer Netzwerke zu bearbeiten, Tools zur automatisierten Verifikation zu entwickeln und relevante Benchmark-Tests zu erarbeiten.Die vorgeschlagene Methodologie wird Algebra und Coalgebra verwenden - zwei formale Frameworks die bereits erfolgreich für die Modellierung und effiziente Analyse von sicherheitskritischen Systemen und insbesondere auch NetKAT verwendet werden. Die bestehenden (co-)algebraischen formalen Grundlagen von NetKAT repräsentieren den perfekten Grundriss um Kausalität und die dazugehörigen Beweismechanismen zu integrieren. Zeitnahes Handeln ist notwendig um bahnbrechende Ergebnisse in diesem Forschungsgebiet zu erzielen.Das Projekt wird in enger Zusammenarbeit mit angesehenen Wissenschaftlern dieses Forschungsgebietes durchgeführt. Davon profitieren sowohl unsere Forschungsgruppe als auch die Studenten der Universität Konstanz, die die Arbeit in einer exzellenten und internationalen Umgebung erleben können.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Großbritannien, Island, Schweden
• Kooperationspartnerinnen / Kooperationspartner: Professor Dr. Luca Aceto; Dr. Hana Chockler; Professorin Dr. Anna Ingolfsdottir; Professor Dr. Stefan Leue; Professor Dr. Mohammad Mousavi; Dr. Alexandra Silva