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

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr10830
Full metadata record
DC FieldValueLanguage
dc.contributor.authorWang, Anduo-
dc.contributor.authorJia, Limin-
dc.contributor.authorZhou, Wenchao-
dc.contributor.authorRen, Yiqing-
dc.contributor.authorLoo, Boon Thau-
dc.contributor.authorRexford, Jennifer-
dc.contributor.authorNigam, Vivek-
dc.contributor.authorScedrov, Andre-
dc.contributor.authorTalcott, Carolyn-
dc.date.accessioned2021-10-08T19:49:10Z-
dc.date.available2021-10-08T19:49:10Z-
dc.date.issued2012-12en_US
dc.identifier.citationWang, 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.2187924en_US
dc.identifier.issn1063-6692-
dc.identifier.urihttps://www.cs.princeton.edu/~jrex/papers/fsr.pdf-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr10830-
dc.description.abstractInterdomain 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.en_US
dc.format.extent1814 - 1827en_US
dc.language.isoen_USen_US
dc.relation.ispartofIEEE/ACM Transactions on Networkingen_US
dc.rightsAuthor's manuscripten_US
dc.titleFSR: Formal Analysis and Implementation Toolkit for Safe Interdomain Routingen_US
dc.typeJournal Articleen_US
dc.identifier.doi10.1109/TNET.2012.2187924-
dc.identifier.eissn1558-2566-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/journal-articleen_US

Files in This Item:
File Description SizeFormat 
FormalAnalysisImplementation.pdf762.53 kBAdobe PDFView/Download


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