A General Approach to Network Configuration Verification

Problem

• The control plane of traditional (non-SDN) networks is a complex distributed system; how to process information and select paths to use for traffic depends on local configuration files, which have thousands of lines of low-level directives. It is hard to reason about the network behavior, and can lead to costly outages when there're configuration errors.

• Existing approaches / tools in two dimension i) network design coverage ii) data plane coverage, but the fundamental question of whether it's possible to build a verification tool that achieves both high network design coverage and high data plane coverage while remaining scalable enough to enable verification of many real network is still open.

Insight

• The main challenge in developing Mainsweeper was scaling such general tool. The paper addresses this challenge by combing a bunch of ideas from networking and verification literature

  • 1) The paper uses a graph-based (v.s path-based) model where rich logical constraints on its edges and nodes encode all possible interactions of route messages

  • 2) The paper uses combinatorial search (v.s message set computation) and use modern SAT / SMT solvers to solve large instances of such problem.

  • 3) The paper turns to the stable path problem, where paths can be described by constraints on edges.

  • 4) The paper designs highly effective optimizations (e.g. slicing to remove things that cannot affect the final outcome, and hoisting to lifts repeated computations out of their logical context and precomputes them once) for solving larger networks.

Key strength

• The evaluations are solid: Minesweeper is applied to many real and synthetic networks (i.e. 152 small- and medium-sized networks). The optimizations to scale it to larger networks reduce verification time by a factor of up to 460x, impressive.

• The paper classifies existing approaches into categories, and identify the drawbacks accordingly. This well-motivates the design of the approach.

• Feels like the approach is also pretty generalized, encoding important features of the network configurations.

Key weakness

• The verification approach doesn't verify properties about transient states of the networks; it only describes the stable solutions to which the control plane will converge.

• Minesweeper does not model features that introduce dependencies across destinations; it only consider control plane elements that influence the forwarding decisions pertaining to a single symbolic packet at a time.

Comments

• What about SDN type of workloads? How is verification done in that space? (i.e. just in the centralized controller?)