Comprehensive Network Configuration Verification via Effective Environment Reduction

Verifying network configurations under all possible environments is critical for uncovering latent configuration bugs. However, due to the vastness of the environment space and the limitations of existing approaches, current tools either fail to scale or explore only a tiny fraction of the full environment space, missing many potential issues. In this paper, we show that it is unnecessary to explore the full environment space. Instead, we introduce an effective reduction of the environment space, under which the network preserves all routing and forwarding behaviors exhibited under the full environment space. We develop a theory of network behavior equivalence between the full and effectively reduced environment spaces, and propose an efficient algorithm to compute such an effective reduction. We implement our approach in a tool called Bulwark. Experiments on both real-world and synthetic networks show that Bulwark uncovers numerous new misconfigurations and delivers orders-of-magnitude speedups over state-of-the-art verifiers.