Configurations of routing protocols in wide area networks (WANs) are highly sophisticated and prone to bugs, leading to severe network outages and security breaches. SMT-based network verification can assist operators in checking the configurations, but they still face scalability challenges when reasoning about failures: to check whether a property holds when no more than k links fail, a verifier needs to explore a tremendous space of failure scenarios. To this end, this paper proposes VeriBoost, a method that can leverage the topology features of WANs to reduce the space of failure scenarios, thereby improving the scalability of SMT-based verification on WANs. VeriBoost achieves the reduction by pruning links that are irrelevant to a property, and compressing multiple links whose failures have an equivalent impact on the property. Experiments on real WAN topologies show that it speeds up SMT-based verification by 2–47×.
