On the feasibility of static analysis for BGP convergence

Internet service providers can enforce a fine grained control of interdomain routing by cleverly configuring the Border Gateway Protocol. However, the price to pay for the flexibility of BGP is the lack of convergence guarantees. Network protocol design literature introduced several sufficient conditions that routing policies should satisfy to guarantee convergence. However, to our knowledge, none of these conditions has yet been exploited to automatically check BGP policies for convergence. This paper presents two fundamental contributions. First, we describe a heuristic algorithm that statically detects potential oscillations in a BGP network. We prove that our algorithm has several highly desirable properties: i) it exceeds state of the art algorithms in that it is able to correctly report more configurations as stable, ii) it can be implemented efficiently enough to enable static analysis of Internet scale BGP configurations, iii) it is free from false negatives, and iv) it can help in spotting the troublesome points in a detected oscillation. We also propose an architecture for a modular tool that exploits our heuristic algorithm to process native router configurations and return information about the potential presence of oscillations. Such a tool can effectively integrate syntactic checkers and assist operators in verifying configurations. We validate our approach using a prototype implementation and show that it scales well enough to enable Internet scale convergence checks.