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.

Communication networks have become a critical infrastructure of our digital society. However, the increasing complexity and stringent dependability requirements starkly contrast with today's manual and error-prone approach to operate networks, highlighting the need for better and more scalable and reliable network analysis and configuration approaches. The goal of the WHATIF project was to develop automated methods to manage and operate networks, ensuring policy compliance and quality of service even in the face of failures, with the desirable outcome of minimizing downtimes and alleviating the burden on human operators. In summary, WHATIF addresses the need for (semi-)automatic tools that can assist with fail-safe network configurations and guarantee correct and efficient network operations even under failures.  

Designing such automated networks, however, is challenging. First, since the reliability and performance of networks are mission-critical for many applications, the solutions must be rigorous and provide correctness properties. Second, the solutions should be able to react quickly to failures and demand changes. Since many network verification problems are computationally hard, designing efficient automated networks is non-trivial. In principle, it seems that to conduct a what-if analysis of a communication network under multiple failures, a combinatorial (i.e., exponential) number of different failure scenarios needs to be considered. 

The WWTF project WHATIF has conceived innovative techniques and developed automatic and efficient tools to enhance network verification and resilience. This research addressed critical network management and verification challenges, contributing practical solutions. A key project outcome is AalWiNeS, an automated tool for verifying network properties. It is based on a novel automata-based abstraction of the network's data plane and offers both formal guarantees and increased speed. AalWiNes spawned multiple publications. In addition to the scientific contribution, our demonstrator of AalWiNes has been presented to several companies in Austria and abroad.

Another major contribution from the project is R-MPLS, a link protection mechanism for MPLS networks, which are widely deployed by Internet Service Providers today. R-MPLS enhances  network resilience and efficiency and has been presented at ACM CoNEXT, attracting interest from industry stakeholders and we also filed a preliminary patent. In a nutshell, R-MPLS leverages the label-stacking capability of MPLS networks to encode multi-failure formally guaranteed protection paths. The efficiency of R-MPLS is fostered by the fact that protection routes are computed in a distributed manner while having computational, memory, and communication costs similar to those of standard solutions.

In order to rigorously evaluate our approaches as well as to facilitate AI/ML approaches in combination to formal methods, we also made a significant methodological contribution, developing MPLS-Kit, a tool for automated generating realistic MPLS data planes. MPLS-Kit supports efficiently generating MPLS data planes using industry-standard control protocols on various network topologies. It facilitates the prototyping and instantiation of MPLS protocols and Fast Reroute mechanisms, supports packet-level simulations, and provides statistics for applications such as congestion, latency, and resilience analysis. The generated data planes can be exported for input by formal verification tools for further analysis.

In addition to studying and optimizing a given network configuration, we also contributed methods and tools to support networks to update and evolve in a correct manner. To this end, we contribute an efficient method for scheduling network updates using Binary Decision Diagrams (BDDs), published in the IEEE/ACM Transactions on Networking (the leading journal in networking), and a fast solution for reachability analysis in pushdown systems using CEGAR techniques, published at ATVA, making significant contributions not only to the networking domain but also well-known formal methods conferences.

Overall, the WWTF project WHATIF has made meaningful contributions to network verification and resilience. The project's outcomes advance theoretical understanding and provide practical tools and methods that enhance the reliability and efficiency of network systems, addressing essential needs in modern network management.

Open Access Publikationen:

M. Chiesa, A. Kamisiński, J. Rak, G. Rétvári and S. Schmid, "A Survey of Fast-Recovery Mechanisms in Packet-Switched Networks," in IEEE Communications Surveys & Tutorials, vol. 23, no. 2, pp. 1253-1301, Secondquarter 2021, doi: 10.1109/COMST.2021.3063980.
keywords: {Routing;IP networks;Multiprotocol label switching;Resilience;Internet;Tutorials;Delays;Fast reroute;network resilience;data plane}

Schweiger, O., Foerster, K., & Schmid, S. (2021). Improving the Resilience of Fast Failover Routing: TREE (Tree Routing to Extend Edge disjoint paths). Proceedings of the Symposium on Architectures for Networking and Communications Systems. https://doi.org/10.48550/arXiv.2111.14123

I. v. Duijn et al., "Automata-Theoretic Approach to Verification of MPLS Networks Under Link Failures," in IEEE/ACM Transactions on Networking, vol. 30, no. 2, pp. 766-781, April 2022, doi: 10.1109/TNET.2021.3126572. keywords: {Tools;Multiprotocol label switching;Handheld computers;Routing;Automata;IP networks;Runtime;Network verification;MPLS;prefix rewriting systems}

Bankhamer, Gregor et al. “Randomized Local Fast Rerouting for Datacenter Networks with Almost Optimal Congestion.” ArXiv abs/2108.02136 (2021): n. pag. https://doi.org/10.48550/arXiv.2108.02136

Scherrer, Simon et al. “Enabling Novel Interconnection Agreements with Path-Aware Networking Architectures.” 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN) (2021): 116-128. https://doi.org/10.48550/arXiv.2104.02346

Henzinger, Monika et al. “On the Complexity of Weight-Dynamic Network Algorithms.” 2021 IFIP Networking Conference (IFIP Networking) (2021): 1-9. https://doi.org/10.48550/arXiv.2105.13172