[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Reduction-based Formal Analysis of BGP Instances
Wang, Anduo and Talcott, Carolyn L. and Gurney, Alexander J. T. and Loo, Boon Thau and Scedrov, Andre - 2012 - PDF

Today’s Internet interdomain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfig- urations 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 tech- niques do not scale well or do not cover the full set of anomalies. Current tech- niques use oversimplified BGP models that capture either anomalies within or across ASes, but not the interactions between the two. To address these limita- tions, we propose a novel approach that reduces network size prior to analysis, while preserving crucial BGP correctness properties. Using Maude, we have de- veloped a toolkit that takes as input a network instance consisting of ASes and their policy configurations, and then performs formal analysis on the reduced instance for safety (protocol convergence). Our results show that our reduction- based analysis allows us to analyze significantly larger network instances at low reduction overhead.