Practical Verification Techniques for Wide-Area Routing

Protocol and system designers use verification techniques to analyze a system's correctness properties. Network operators need verification techniques to ensure the "Correct" operation of BGP. BGP's distributed dependencies cause small configuration mistakes or oversights to spur complex errors, which sometimes have devastating effects on global connectivity. These errors are often difficult to debug because they are sometimes only exposed by a specific message arrival pattern or failure scenario. This paper presents an approach to BGP verification that is primarily based on static analysis of router configuration.