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

doi:10.1145/2018436.2018510

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 proceeding › Conference contribution

7 Scopus citations

Abstract

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 language	English (US)
Title of host publication	Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11
Pages	440-441
Number of pages	2
DOIs	https://doi.org/10.1145/2018436.2018510
State	Published - 2011
Event	ACM SIGCOMM 2011 Conference, SIGCOMM'11 - Toronto, ON, Canada Duration: Aug 15 2011 → Aug 19 2011

Publication series

Name	Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11

Other

Other	ACM SIGCOMM 2011 Conference, SIGCOMM'11
Country/Territory	Canada
City	Toronto, ON
Period	8/15/11 → 8/19/11

All Science Journal Classification (ASJC) codes

Computer Graphics and Computer-Aided Design

Keywords

Design
Experimentation
Languages

Access to Document

10.1145/2018436.2018510

Cite this

@inproceedings{4821830398c7479a9f58256cf33e8e85,

title = "FSR: Formal analysis and implementation toolkit for safe inter-domain routing",

abstract = "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.",

keywords = "Design, Experimentation, Languages",

author = "Yiqing Ren and Wenchao Zhou and Anduo Wang and Limin Jia and Gurney, {Alexander J.T.} and Loo, {Boon Thau} and Jennifer Rexfordz",

year = "2011",

doi = "10.1145/2018436.2018510",

language = "English (US)",

isbn = "9781450307970",

series = "Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11",

pages = "440--441",

booktitle = "Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11",

note = "ACM SIGCOMM 2011 Conference, SIGCOMM'11 ; Conference date: 15-08-2011 Through 19-08-2011",

}

Ren, Y, Zhou, W, Wang, A, Jia, L, Gurney, AJT, Loo, BT & Rexfordz, J 2011, FSR: Formal analysis and implementation toolkit for safe inter-domain routing. in Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11. Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11, pp. 440-441, ACM SIGCOMM 2011 Conference, SIGCOMM'11, Toronto, ON, Canada, 8/15/11. https://doi.org/10.1145/2018436.2018510

TY - GEN

T1 - FSR

T2 - ACM SIGCOMM 2011 Conference, SIGCOMM'11

AU - Ren, Yiqing

AU - Zhou, Wenchao

AU - Wang, Anduo

AU - Jia, Limin

AU - Gurney, Alexander J.T.

AU - Loo, Boon Thau

AU - Rexfordz, Jennifer

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - Design

KW - Experimentation

KW - Languages

UR - http://www.scopus.com/inward/record.url?scp=80053156790&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80053156790&partnerID=8YFLogxK

U2 - 10.1145/2018436.2018510

DO - 10.1145/2018436.2018510

M3 - Conference contribution

AN - SCOPUS:80053156790

SN - 9781450307970

T3 - Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11

SP - 440

EP - 441

BT - Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM'11

Y2 - 15 August 2011 through 19 August 2011

ER -

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

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this