[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing
Wang, Anduo and Jia, Limin and Zhou, Wenchao and Ren, Yiqing and Loo, Boon Thau and Rexford, Jennifer and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn - 2012 - PDF

Inter-domain routing stitches the disparate parts of the Internet together, making protocol stability a critical issue to both researchers and practitioners. Yet, researchers create safety proofs and counter-examples by hand, and build simulators and prototypes to explore protocol dynamics. Similarly, network operators analyze their router configurations manually, or using home-grown tools. In this paper, we present a comprehensive toolkit for analyzing and implementing routing policies, ranging from high-level guidelines to specific router configurations. Our Formally Safe Routing (FSR) toolkit performs all of these functions from the same algebraic representation of routing policy. We show that routing algebra has a natural translation to both integer constraints (to perform safety analysis with SMT solvers) and declarative programs (to generate distributed imple- mentations). Our extensive experiments with realistic topologies and policies show how FSR can detect problems in an AS’s iBGP configuration, prove sufficient conditions for BGP safety, and empirically evaluate convergence time.