Fast SMT-Based Fault Tolerance Verification for Wide Area Networks

Abstract

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×.