Accelerating BGP Configuration Verification Through Reducing Cycles in SMT Constraints
Xiaozhe Shao, Zibin Chen, Daniel E. Holcomb, Lixin Gao · IEEE/ACM Transactions on Networking · 2022
Network verification has been proposed to help network operators eliminate the outage or security issues caused by misconfigurations. Recent studies have proposed SMT-based approaches to verify network properties with respect to network configurations. These approaches translate the verification problem into a Satisfiability Module Theories (SMT) problem. Although these approaches are attractive because of their broad coverage, they can scale to moderate-size networks only. In this paper, we propose BiNode to accelerate the network verification process. The key idea is to formulate the SMT constraints in a manner that reduces/eliminates the cyclic dependencies between its variables. By doing so, we expedite the solving of the SMT problem. We implement and evaluate the performance of BiNode through an off-the-shelf SMT solver. The experimental results show that BiNode can reduce verification time by an order of magnitude through reducing/eliminating the cyclic dependencies among SMT variables.