Computer networks connect people across the world and are a critical infrastructure for many of the services that a modern society depends on. With the rapidly growing use of computer networks, the demand for higher bandwidth and lower latency to support a new generation of applications, as well as the need for failure protection mechanisms, modern computer networks have evolved into complex heterogeneous systems. These networks are tricky to manage and operate correctly, and there are many examples of subtle configuration errors taking down entire networks.

Formal methods have been proposed as a way to reduce the risk of network outages by creating mathematically well-defined models of the networks and applying algorithmic techniques to pro-actively verify conformance with the specifications or synthesize correct-by-construction configurations.

In this thesis, we contribute to the formal treatment of the widely deployed MPLS networks with a focus on quantitative properties and resiliency mechanisms. We present a formal model of the MPLS network data plane and use this model to develop a practical technique for increasing the resilience of MPLS networks by synthesizing loop-free recursive failover protections. Moreover, we extend prior work on model checking MPLS networks with failover protections to also consider quantitative properties with shortest and longest trace analysis. This work builds on the connection between MPLS networks and pushdown automata. To address the scalability of MPLS network model checking, we significantly improve the performance of pushdown automata reachability checking by developing new on-the-fly algorithms and an efficient tool implementation. We increase the trustworthiness of the model checking results by formally proving the correctness of the used algorithms in the proof assistant Isabelle/HOL, extracting executable code, and performing differential testing against this formally verified oracle.
Finally, we address the importance of providing accurate data for the formal models through a case study with a network analytics company, where we present a robust and efficient method for inferring the otherwise unknown ratios that the routers use when load balancing traffic among multiple paths.

Members of the assessment committee
Members of the assessment committee are Associate Professor Michele Albano (Chairman), Aalborg University (Denmark), Associate Professor Laurent Vanbever, ETH Zürich (Switzerland), and Partner Researcher Nikolaj Bjørner, Microsoft Research (USA). Supervisor for the thesis has been Professor Jiří Srba, Aalborg University. The moderator will be Professor Kim Guldstrand Larsen. All interested parties are welcome.