Extending the Limits of Formal Methods in Network Operations
Abstract
The Internet has become an essential part of today’s society. Critical systems like banking or emergency services depend on the Internet to be highly available. Despite network operators designing highly resilient networks, outages remain a common occurrence, especially those triggered by human errors. Indeed, networks have grown in size and complexity, making network operations notoriously challenging.
Academia has proposed systems that apply formal methods to assist in network operations and prevent misconfigurations before they are deployed, but the industry has been hesitant to adopt them thus far. We attribute the slow adoption to missing capabilities of these formal tools, as they lack support for critical use cases, network properties, and routing protocols.
This dissertation extends the limits of formal methods in network operations. We present four distinct works that tackle key limitations of existing network verifiers, configuration synthesizers, and reconfiguration systems by extending their capabilities and bringing formal methods in network operations closer to industry-wide adoption.
First, we present the BGP State Iterator to explore the space of control-plane routing states directly. Its exploration can be guided by the specification or user-provided heuristics, enabling new use cases such as probabilistic control-plane verification. Second, we present Velo, the first verifier to reason about worst-case link loads under unexpected failures and routing events. We find that routing events significantly impact link loads in the network, and we design an algorithm to navigate the space of all such events efficiently. Third, we present Chameleon to safely reconfigure BGP networks while guaranteeing the absence of routing anomalies at any time, including any transient states, without noticeable overhead. Finally, we present a systematic analysis of the complexity of configuration synthesis. Indeed, we confirm that synthesis is intractable in general, but we also outline a path towards scalable configuration synthesis.
People
BibTex
@phdthesis{schneider2025extending,
author = {Schneider, Tibor Jan},
title = {{Extending the Limits of Formal Methods in Network Operations}},
year = 2025,
month = dec,
publisher = {ETH Zurich},
doi = {10.3929/ETHZ-C-000790286},
url = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/790286/thesis-rc.pdf},
school = {ETH Zurich}
}Research Collection: 20.500.11850/790286