Reduction-Based Formal Analysis of BGP Instances

Today’s Internet interdomain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfigurations by individual autonomous systems (ASes). These misconfigurations are often difficult to manually diagnose beyond a small number of nodes due to the state explosion problem. To aid the diagnosis of potential anomalies, researchers have developed various formal models and analysis tools. However, these techniques do not scale well or do not cover the full set of anomalies. Current techniques use oversimplified BGP models that capture either anomalies within or across ASes, but not the interactions between the two. To address these limitations, we propose a novel approach that reduces network size prior to analysis, while preserving crucial BGP correctness properties. Using Maude, we have developed a toolkit that takes as input a network instance consisting of ASes and their policy configurations, and then performs formal analysis...

• Type: Journal
• Year: 2012
• Where: TACAS
• Authors: Anduo Wang, Carolyn L. Talcott, Alexander J. T. Gurney, Boon Thau Loo, Andre Scedrov
• Keywords: Algorithms, Border Gateway Protocol, Correctness Properties, State Explosion Problem, TACAS 2012