Alexander Gurney

Reduction-based formal analysis of BGP instances

Citation Anduo Wang, Carolyn Talcott, Alexander J. T. Gurney, Boon Thau Loo and Andre Scedrov. 2012. Reduction-based formal analysis of BGP instances. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Tallinn.
Abstract 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 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.
Paper
PDF (313k)
Technical report
PDF (544k)