Toward a Lightweight Model of BGP Safety
For the past ten years, researchers have used the Stable Paths Problem (SPP) to analyze the stability properties of the Border Gateway Protocol (BGP). Analysis of SPP has revealed several combinations of topologies and routing configurations (or gadgets) where BGP cannot converge to a unique stable solution. Researchers typically analyze SPP by hand, using a trial-and-error process to generate small SPP instances that exhibit undesirable properties and prove sufficient conditions for SPP solvability. In this paper, the authors present a formal, machine-readable SPP model encoded in the Alloy lightweight modeling language.