Skip to main content

FSR: Formal Analysis and Implementation Toolkit for Safe Interdomain Routing

Author(s): Wang, Anduo; Jia, Limin; Zhou, Wenchao; Ren, Yiqing; Loo, Boon Thau; et al

To refer to this page use:
Abstract: Interdomain 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 counterexamples by hand and build simulators and prototypes to explore protocol dynamics. Similarly, network operators analyze their router configurations manually or using homegrown 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 implementations). Our extensive experiments with realistic topologies and policies show how FSR can detect problems in an autonomous system's (AS's) iBGP configuration, prove sufficient conditions for Border Gateway Protocol (BGP) safety, and empirically evaluate convergence time.
Publication Date: Dec-2012
Citation: Wang, Anduo, Limin Jia, Wenchao Zhou, Yiqing Ren, Boon Thau Loo, Jennifer Rexford, Vivek Nigam, Andre Scedrov, and Carolyn Talcott. "FSR: Formal Analysis and Implementation Toolkit for Safe Interdomain Routing." IEEE/ACM Transactions on Networking 20, no. 6 (2012): pp. 1814-1827. doi:10.1109/TNET.2012.2187924
DOI: 10.1109/TNET.2012.2187924
ISSN: 1063-6692
EISSN: 1558-2566
Pages: 1814 - 1827
Type of Material: Journal Article
Journal/Proceeding Title: IEEE/ACM Transactions on Networking
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.