Fast and Quantitative What-if Analysis for Dependable Communication Networks (WHATIF)
Kommunikationsnetze sind zu einer kritischen Infrastruktur unserer digitalen Gesellschaft geworden. Die zunehmende Komplexität und die strengen Zuverlässigkeitsanforderungen stehen jedoch in starkem Gegensatz zu den heutigen manuellen und fehleranfälligen Ansätzen zur Verwaltung von Netzwerken. Dies verdeutlicht die Notwendigkeit besserer, skalierbarer und zuverlässiger Methoden zur Netzwerkanalyse und -konfiguration. Ziel des WHATIF Projekts war es, automatisierte Verfahren zur Verwaltung und zum Betrieb von Netzwerken zu entwickeln, um die Einhaltung von Richtlinien und die Dienstgüte auch im Falle von Ausfällen sicherzustellen. Ein wünschenswertes Ergebnis ist dabei die Minimierung von Ausfallzeiten und die Entlastung menschlicher Betreiber. Zusammenfassend adressiert WHATIF den Bedarf an (teil-)automatisierten Werkzeugen, die fehlersichere Netzwerkkonfigurationen unterstützen und korrekten sowie effizienten Netzwerkbetrieb auch unter Störungen gewährleisten.
Die Entwicklung solcher automatisierter Netzwerke ist jedoch eine Herausforderung. Erstens müssen die Lösungen rigoros sein und Korrektheitseigenschaften bieten, da Zuverlässigkeit und Leistung von Netzwerken für viele Anwendungen kritisch sind. Zweitens sollten die Lösungen in der Lage sein, schnell auf Ausfälle und Veränderungen der Anforderungen zu reagieren. Da viele Probleme der Netzwerkverifikation rechnerisch komplex sind, ist die Entwicklung effizienter automatisierter Netzwerke nicht trivial. Grundsätzlich scheint es, dass für die Durchführung einer "What-If"-Analyse eines Kommunikationsnetzwerks unter mehreren Ausfällen eine kombinatorische (d.h. exponentielle) Anzahl verschiedener Ausfallszenarien berücksichtigt werden muss.
Das WWTF-Projekt WHATIF hat innovative Techniken entwickelt und automatische, effiziente Werkzeuge zur Verbesserung der Netzwerkverifikation und -resilienz konzipiert. Diese Forschung hat kritische Herausforderungen im Bereich der Netzwerkverwaltung und -verifikation adressiert und praxisorientierte Lösungen beigetragen. Ein zentrales Ergebnis des Projekts ist AalWiNeS, ein automatisiertes Werkzeug zur Verifikation von Netzwerkeigenschaften. Es basiert auf einer neuartigen Automaten-basierten Abstraktion der Datenebene des Netzwerks und bietet sowohl formale Garantien als auch erhöhte Geschwindigkeit. AalWiNeS hat mehrere wissenschaftliche Publikationen hervorgebracht. Neben dem wissenschaftlichen Beitrag wurde unser Demonstrator von AalWiNeS mehreren Unternehmen in Österreich und im Ausland präsentiert.
Ein weiterer bedeutender Beitrag des Projekts ist R-MPLS, ein Mechanismus zum Schutz von Verbindungen in MPLS-Netzwerken, die heute von Internetdienstanbietern weit verbreitet eingesetzt werden. R-MPLS verbessert die Netzwerkresilienz und Effizienz und wurde auf der ACM CoNEXT vorgestellt, wo es Interesse bei Branchenvertretern weckte. Zudem haben wir ein vorläufiges Patent eingereicht. Kurz gesagt, nutzt R-MPLS die Label-Stacking-Fähigkeit von MPLS-Netzwerken, um Schutzpfade für mehrere Ausfälle mit formalen Garantien zu kodieren. Die Effizienz von R-MPLS wird dadurch gefördert, dass Schutzrouten dezentral berechnet werden, wobei die rechnerischen, Speicher- und Kommunikationskosten denen standardmäßiger Lösungen ähnlich sind.
Um unsere Ansätze rigoros zu evaluieren und den Einsatz von KI/ML-Methoden in Kombination mit formalen Verfahren zu erleichtern, haben wir auch einen bedeutenden methodischen Beitrag geleistet: die Entwicklung von MPLS-Kit, einem Werkzeug zur automatisierten Erstellung realistischer MPLS-Datenebenen. MPLS-Kit unterstützt die effiziente Generierung von MPLS-Datenebenen unter Verwendung industrienormativer Steuerungsprotokolle auf verschiedenen Netzwerktopologien. Es erleichtert das Prototyping und die Implementierung von MPLS-Protokollen sowie Fast-Reroute-Mechanismen, unterstützt Simulationen auf Paketebene und liefert Statistiken für Anwendungen wie Stau-, Latenz- und Resilienzanalysen. Die generierten Datenebenen können für die Eingabe in formale Verifikationswerkzeuge exportiert werden, um eine weitergehende Analyse zu ermöglichen.
Neben der Untersuchung und Optimierung einer bestehenden Netzwerkkonfiguration haben wir auch Methoden und Werkzeuge entwickelt, die Netzwerke dabei unterstützen, sich korrekt zu aktualisieren und weiterzuentwickeln. Zu diesem Zweck haben wir eine effiziente Methode für die Planung von Netzwerkaktualisierungen mit Hilfe von Binary Decision Diagrams (BDDs) beigetragen, die in den IEEE/ACM Transactions on Networking (der führenden Fachzeitschrift im Bereich Netzwerke) veröffentlicht wurde. Außerdem haben wir eine schnelle Lösung für die Erreichbarkeitsanalyse in Pushdown-Systemen unter Verwendung von CEGAR-Techniken entwickelt, die auf der Konferenz ATVA vorgestellt wurde. Damit leisten wir nicht nur bedeutende Beiträge zum Bereich Netzwerke, sondern auch zu renommierten Konferenzen im Bereich formale Methoden.
Insgesamt hat das WWTF-Projekt WHATIF wesentliche Beiträge zur Netzwerkverifikation und -resilienz geleistet. Die Ergebnisse des Projekts fördern das theoretische Verständnis und bieten praktische Werkzeuge und Methoden, die die Zuverlässigkeit und Effizienz von Netzwerksystemen verbessern und wichtige Anforderungen des modernen Netzwerkmanagements adressieren.