Network Can Help Check Itself: Accelerating SMT-based Network Configuration Verification Using Network Domain Knowledge
Xing Fang, Feiyan Ding, Bang Huang, Ziyi Wang, Gao Han, Rulan Yang, Lizhao You, Qiao jun Xiang, Linghe Kong, Yutong Liu, Jiwu Shu · 2024
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.