Accelerating BGP Configuration Verification Through Reducing Cycles in SMT Constraints

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.