FSR: Formal analysis and implementation toolkit for safe inter-domain routing

Yiqing Ren, Wenchao Zhou, Anduo Wang, Limin Jia, Alexander J.T. Gurney, Boon Thau Loo, Jennifer Rexfordz

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


We present the demonstration of 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 very natural translation to both integer constraints (to perform safety analysis using SMT solvers) and declarative programs (to generate distributed implementations). Our demonstration with realistic topologies and policies shows how FSR can detect problems in an AS's iBGP configuration, prove sufficient conditions for BGP safety, and empirically evaluate convergence time.

Original languageEnglish (US)
Title of host publicationProceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11
Number of pages2
StatePublished - 2011
EventACM SIGCOMM 2011 Conference, SIGCOMM'11 - Toronto, ON, Canada
Duration: Aug 15 2011Aug 19 2011

Publication series

NameProceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11


OtherACM SIGCOMM 2011 Conference, SIGCOMM'11
CityToronto, ON

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design


  • Design
  • Experimentation
  • Languages


Dive into the research topics of 'FSR: Formal analysis and implementation toolkit for safe inter-domain routing'. Together they form a unique fingerprint.

Cite this