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. We argue that: (1) because BGP's configuration affects its fundamental behavior, verification is a program analysis problem, (2) BGP's complex, dynamic interactions are difficult to abstract and impossible to enumerate, which precludes existing verification techniques, (3) because of BGP's flexible, policy-based configuration, some aspects...

• Type: Journal
• Year: 2004
• Where: CCR
• Authors: Nick Feamster
• Keywords: BGP Verification, CCR 2004, Small Configuration Mistakes, Verification Techniques