UCLA

Network router configuration errors are a common cause of network failures. Verifying configurations using static analysis can prevent errors from occurring, but existing verifiers, especially for the control plane, have two problems: they cannot scale to large networks, and they cannot localize errors to their source in the configurations. This dissertation proposed the use of modular techniques for verifying control plane properties in the network. While previous verifiers model the behavior of the network holistically, modular verification guarantees useful network properties while executing checks on individual routers and connections, allowing it to scale better and achieve better localization. First, I present Campion, a tool for modularly checking equivalence between a pair of router configurations by looking at corresponding components, allowing it to localize the source of the differences to lines and structures in the configuration. Next, I present a tool that verifies network-wide BGP properties using only local checks on configurations. The technique uses local constraints to bridge the gap from local properties to network properties. Both of these techniques have been deployed and have found numerous previously unknown bugs in real-world networks.