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.|
|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|
|Pages:||1814 - 1827|
|Type of Material:||Journal Article|
|Journal/Proceeding Title:||IEEE/ACM Transactions on Networking|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.