Satisfiability Modulo Theories (SMT) based network configuration verification tools are powerful tools in preventing network configuration errors. However, their fundamental limitation is efficiency, because they rely on generic SMT solvers to solve SMT problems, which are in general NP-complete. In this paper, we show that by leveraging network domain knowledge, we can substantially accelerate SMT-based network configuration verification. Our key insights are: given a network configuration verification formula, network domain knowledge can (1) guide the search of solutions to the formula by avoiding unnecessary search spaces; and (2) help simplify the formula, reducing the problem scale. We leverage these insights to design a new SMT- based network configuration verification tool called NetSMT. Extensive evaluation using real-world topologies and synthetic network configurations shows that NetSMT achieves orders of magnitude improvements compared to state-of-the-art methods.

In this paper, we show that by capturing the causal relationship among the computation of routers, one can transform the distributed program composed of routing processes into a sequential program, which allows the use of various sequential program analysis theories and tools for diagnosing and repairing routing configuration errors. This insight sheds light on future research on automatic network configuration diagnosis and repair. To demonstrate its feasibility and generality, we give the preliminary design of two methods for routing configuration error diagnosis: (1) data flow analysis using minimal unsatisfiable core and error invariants; and (2) control flow analysis using selective symbolic execution. Using real-world topologies and synthetic configurations, we show that both methods can effectively find errors in routing configurations while incurring reasonable overhead.