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 Rexford

doi:10.1145/2043164.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 Rexford

Research output: Contribution to journal › Article › peer-review

3 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)
Pages (from-to)	440-441
Number of pages	2
Journal	Computer Communication Review
Volume	41
Issue number	4
DOIs	https://doi.org/10.1145/2043164.2018510
State	Published - Aug 15 2011

All Science Journal Classification (ASJC) codes

Software
Computer Networks and Communications

Keywords

Formal verification
Formally safe routing
Safety analysis

Access to Document

10.1145/2043164.2018510

Cite this

@article{b49520596196457cbc50857eed6344cf,

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 = "Formal verification, Formally safe routing, Safety analysis",

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

note = "Publisher Copyright: {\textcopyright} 2011 Owner/author(s).",

year = "2011",

month = aug,

day = "15",

doi = "10.1145/2043164.2018510",

language = "English (US)",

volume = "41",

pages = "440--441",

journal = "Computer Communication Review",

issn = "0146-4833",

publisher = "Association for Computing Machinery (ACM)",

number = "4",

}

TY - JOUR

T1 - FSR

T2 - Formal analysis and implementation toolkit for safe inter-domain routing

AU - Ren, Yiqing

AU - Zhou, Wenchao

AU - Wang, Anduo

AU - Jia, Limin

AU - Gurney, Alexander J.T.

AU - Loo, Boon Thau

AU - Rexford, Jennifer

PY - 2011/8/15

Y1 - 2011/8/15

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 - Formal verification

KW - Formally safe routing

KW - Safety analysis

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

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

U2 - 10.1145/2043164.2018510

DO - 10.1145/2043164.2018510

M3 - Article

AN - SCOPUS:85090994899

SN - 0146-4833

VL - 41

SP - 440

EP - 441

JO - Computer Communication Review

JF - Computer Communication Review

IS - 4

ER -

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

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this