demonstration

Free access

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

Authors:

Alexander J.T. Gurney,

Boon Thau Loo,

Jennifer RexfordAuthors Info & Claims

SIGCOMM '11: Proceedings of the ACM SIGCOMM 2011 conference

Pages 440 - 441

https://doi.org/10.1145/2018436.2018510

Published: 15 August 2011 Publication History

PDF eReader

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.

References

[1]

Gao, L., and Rexford, J. Stable Internet routing without global coordination. In ACM SIGMETRICS (2000).

Digital Library

Google Scholar

[2]

Griffin, T. G., Shepherd, F. B., and Wilfong, G. The stable paths problem and interdomain routing. IEEE/ACM Trans. on Networking 10 (2002).

Digital Library

Google Scholar

[3]

Griffin, T. G., and Sobrinho, J. L. Metarouting. In ACM SIGCOMM (2005).

Digital Library

Google Scholar

[4]

Loo, B. T., Condie, T., Garofalakis, M., Gay, D. E., Hellerstein, J. M., Maniatis, P., Ramakrishnan, R., Roscoe, T., and Stoica, I. Declarative networking. In Communications of the ACM 52 (2009).

Digital Library

Google Scholar

[5]

Muthukumar, S. C., Li, X., Liu, C., Kopena, J. B., Oprea, M., and Loo, B. T. Declarative toolkit for rapid network protocol simulation and experimentation. In ACM SIGCOMM (demo) (2009).

Google Scholar

[6]

Network Simulator 3. http://www.nsnam.org/.

Google Scholar

[7]

Sobrinho, J. An algebraic theory of dynamic network routing. IEEE/ACM Trans. on Networking 13 (2005).

Digital Library

Google Scholar

[8]

Wang, A., Jia, L., Zhou, W., Ren, Y., Loo, B. T., Rexford, J., Nigam, V., Scedrov, A., and Talcott, C. FSR: Formal analysis and implementation toolkit for safe inter-domain routing. University of Pennsylvania Tech. Report MS-CIS-11-10 (2011), http://repository.upenn.edu/cis_reports/954/.

Google Scholar

[9]

Yices. http://yices.csl.sri.com/.

Google Scholar

Cited By

View all

Zhou WTao TLoo BMao Y(2013)Declarative secure distributed information systemsComputer Languages, Systems and Structures10.1016/j.cl.2012.09.00239:1(1-24)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1016/j.cl.2012.09.002
Di Cosmo F(2023)Decidability Borders of Verification of Communicating Datalog AgentsMulti-Agent Systems10.1007/978-3-031-43264-4_39(507-513)Online publication date: 14-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-43264-4_39
Amaral PBernardo LPinto P(2020)Achieving Correct Hop-by-Hop Forwarding on Multiple Policy-Based Routing PathsIEEE Transactions on Network Science and Engineering10.1109/TNSE.2019.29155157:3(1226-1238)Online publication date: 1-Jul-2020
https://doi.org/10.1109/TNSE.2019.2915515
Show More Cited By

Index Terms

FSR: formal analysis and implementation toolkit for safe inter-domain routing
1. Networks
  1. Network architectures

Recommendations

FSR: formal analysis and implementation toolkit for safe inter-domain routing
SIGCOMM '11

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 ...
FSR: formal analysis and implementation toolkit for safe interdomain routing

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 ...
Integrating requirements analysis and safety analysis
RE '95: Proceedings of the Second IEEE International Symposium on Requirements Engineering

Summary form only given. In developing software for safety critical systems, it is necessary to carry out both requirements analysis and safety analysis. During requirements analysis, the behavioural and functional requirements of the system's software ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SIGCOMM '11: Proceedings of the ACM SIGCOMM 2011 conference

August 2011

502 pages

ISBN:9781450307970

DOI:10.1145/2018436

General Chairs:
Srinivasan Keshav
University of Waterloo, Canada
,
Jörg Liebeherr
University of Toronto, Canada
,
Program Chairs:
John Byers
Boston University, USA
,
Jeffrey Mogul
HP Labs, USA

ACM SIGCOMM Computer Communication Review Volume 41, Issue 4
SIGCOMM '11
August 2011
480 pages
ISSN:0146-4833
DOI:10.1145/2043164
Issue’s Table of Contents

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 August 2011

Check for updates

Author Tags

Qualifiers

Demonstration

Conference

SIGCOMM '11

Sponsor:

SIGCOMM

SIGCOMM '11: ACM SIGCOMM 2011 Conference

August 15 - 19, 2011

Ontario, Toronto, Canada

Acceptance Rates

SIGCOMM '11 Paper Acceptance Rate 32 of 223 submissions, 14%;

Overall Acceptance Rate 462 of 3,389 submissions, 14%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
315
Total Downloads

Downloads (Last 12 months)71
Downloads (Last 6 weeks)13

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zhou WTao TLoo BMao Y(2013)Declarative secure distributed information systemsComputer Languages, Systems and Structures10.1016/j.cl.2012.09.00239:1(1-24)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1016/j.cl.2012.09.002
Di Cosmo F(2023)Decidability Borders of Verification of Communicating Datalog AgentsMulti-Agent Systems10.1007/978-3-031-43264-4_39(507-513)Online publication date: 14-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-43264-4_39
Amaral PBernardo LPinto P(2020)Achieving Correct Hop-by-Hop Forwarding on Multiple Policy-Based Routing PathsIEEE Transactions on Network Science and Engineering10.1109/TNSE.2019.29155157:3(1226-1238)Online publication date: 1-Jul-2020
https://doi.org/10.1109/TNSE.2019.2915515
Di Cosmo F(2019)The Impact of Propositional Messages on Termination of Declarative Distributed SystemsSelected Reflections in Language, Logic, and Information10.1007/978-3-031-50628-4_4(44-79)Online publication date: 5-Aug-2019
https://dl.acm.org/doi/10.1007/978-3-031-50628-4_4
Ma JLe FRusso ALobo J(2018)Declarative Framework for Specification, Simulation and Analysis of Distributed ApplicationsIEEE Transactions on Knowledge and Data Engineering10.1109/TKDE.2016.251560428:6(1489-1502)Online publication date: 31-Dec-2018
https://dl.acm.org/doi/10.1109/TKDE.2016.2515604
Sosnovich AGrumberg ONakibly G(2015)Analyzing Internet Routing Security Using Model CheckingProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_9(112-129)Online publication date: 24-Nov-2015
https://dl.acm.org/doi/10.1007/978-3-662-48899-7_9
Loo BZhou W(2012)Declarative NetworkingSynthesis Lectures on Data Management10.2200/S00403ED1V01Y201202DTM0234:1(1-129)Online publication date: 31-Jan-2012
https://doi.org/10.2200/S00403ED1V01Y201202DTM023
Lobo JMa JRusso ALe F(2012)Declarative Distributed ComputingCorrect Reasoning10.1007/978-3-642-30743-0_31(454-470)Online publication date: 2012
https://doi.org/10.1007/978-3-642-30743-0_31

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

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

FSR: formal analysis and implementation toolkit for safe interdomain routing

Integrating requirements analysis and safety analysis