Fast and Quantitative What-if Analysis for Dependable Communication Networks (WHATIF)

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 Publications:

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.

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

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

Schmid, S., Schnepf, N., Srba, J. (2021). Resilient Capacity-Aware Routing. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12651. Springer, Cham. https://doi.org/10.1007/978-3-030-72016-2_22

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.   

Stefan Schmid, Morten Konggaard Schou, Jiří Srba, and Juan Vanerio. 2022. R-MPLS: recursive protection for highly dependable MPLS networks. In Proceedings of the 18th International Conference on emerging Networking EXperiments and Technologies (CoNEXT '22). Association for Computing Machinery, New York, NY, USA, 276–292. https://doi.org/10.1145/3555050.3569140

Philipp Zabka, Klaus-T. Foerster, Stefan Schmid, Christian Decker, Empirical evaluation of nodes and channels of the lightning network, Pervasive and Mobile Computing, Volume 83, 2022, 101584, ISSN 1574-1192, https://doi.org/10.1016/j.pmcj.2022.101584

Wenkai Dai, Klaus-Tycho Foerster, and Stefan Schmid. 2023. A Tight Characterization of Fast Failover Routing: Resiliency to Two Link Failures is Possible. In Proceedings of the 35th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA '23). Association for Computing Machinery, New York, NY, USA, 153–163. https://doi.org/10.1145/3558481.3591080

Kim G. Larsen, Anders Mariegaard, Stefan Schmid, Jiří Srba, AllSynth: A BDD-based approach for network update synthesis, Science of Computer Programming, Volume 230, 2023, 102992, ISSN 0167-6423, https://doi.org/10.1016/j.scico.2023.102992

Juan Vanerio, Lily Hügerich, and Stefan Schmid. 2024. Tero: Offloading CDN Traffic to Massively Distributed Devices. In Proceedings of the 25th International Conference on Distributed Computing and Networking (ICDCN '24). Association for Computing Machinery, New York, NY, USA, 186–198. https://doi.org/10.1145/3631461.3631556

Winkler, K., Paz, A., Galeana, H.R. et al. The Time Complexity of Consensus Under Oblivious Message Adversaries. Algorithmica 86, 1830–1861 (2024). https://doi.org/10.1007/s00453-024-01209-4