More Web Proxy on the site http://driver.im/

research-article

Open access

Lightyear: Using Modularity to Scale BGP Control Plane Verification

Authors:

Steven Benaloh,

Karthick Jayaraman,

Todd Millstein,

George VargheseAuthors Info & Claims

ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

Pages 94 - 107

https://doi.org/10.1145/3603269.3604842

Published: 01 September 2023 Publication History

Abstract

Current network control plane verification tools cannot scale to large networks because of the complexity of jointly reasoning about the behaviors of all network nodes. We present a modular approach to control plane verification, where end-to-end network properties are verified via a set of purely local checks on individual nodes and edges. The approach targets verification of reachability properties for BGP configurations, and provides guarantees in the face of arbitrary external route announcements and, for some properties, arbitrary node/link failures. We have proven the approach correct and implemented it in a tool Lightyear. Experimentally we show Lightyear scales dramatically better than prior control plane verifiers. Further, Lightyear has been used for six months to verify properties of a major cloud provider network containing hundreds of routers and tens of thousands of edges, finding and fixing bugs in the process. To our knowledge no prior control-plane verification tool has been shown to scale to that size and complexity. Our modular approach also makes it easy to localize configuration errors and enables incremental re-verification.

References

[1]

Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast Multilayer Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 201--219. https://www.usenix.org/conference/nsdi20/presentation/abhashkumar

[2]

Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. 2023. Modular Control Plane Verification via Temporal Invariants. Proc. ACM Program. Lang. 7, PLDI, Article 108 (jun 2023), 26 pages.

Digital Library

[3]

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). Association for Computing Machinery, New York, NY, USA, 113--126.

Digital Library

[4]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM '17). Association for Computing Machinery, New York, NY, USA, 155--168.

Digital Library

[5]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2018. Control Plane Compression. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication (SIGCOMM '18). Association for Computing Machinery, New York, NY, USA, 476--489.

Digital Library

[6]

Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2019. Abstract Interpretation of Distributed Network Control Planes. Proc. ACM Program. Lang. 4, POPL, Article 42 (dec 2019), 27 pages.

Digital Library

[7]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337--340.

Digital Library

[8]

Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP Configuration Faults with Static Analysis. In Proceedings of the 2Nd Conference on Symposium on Networked Systems Design & Implementation - Volume 2 (NSDI'05). USENIX Association, Berkeley, CA, USA, 43--56. http://dl.acm.org/citation.cfm?id=1251203.1251207

Digital Library

[9]

Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. 2016. The spirit of ghost code. Formal Methods in System Design 48, 3 (2016), 152--174.

Digital Library

[10]

Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. In Proceedings of the 2016 ACM SIGCOMM Conference (SIGCOMM '16). ACM, New York, NY, USA, 300--313.

Digital Library

[11]

Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576--580.

Digital Library

[12]

Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. 2019. Validating Datacenters at Scale. In Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM '19). Association for Computing Machinery, New York, NY, USA, 200--213.

Digital Library

[13]

Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, and Charlie Kaufman. 2014. Automated Analysis and Debugging of Network Connectivity Policies. Technical Report MSR-TR-2014-102. Microsoft.

[14]

C. B. Jones. 1983. Specification and design of (parallel) programs. In Proceedings of IFIP '83, R. E. A. Manson (Ed.). IFIP, North-Holland, 321--332.

[15]

Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation (NSDI'12). USENIX Association, Berkeley, CA, USA, 9--9. http://dl.acm.org/citation.cfm?id=2228298.2228311

Digital Library

[16]

Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. 2012. Veriflow: Verifying Network-wide Invariants in Real Time. SIGCOMM Comput. Commun. Rev. 42, 4 (Sept. 2012), 467--472.

Digital Library

[17]

Leslie Lamport. 1994. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16, 3 (1994), 872--923.

Digital Library

[18]

Nuno P. Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). USENIX Association, Oakland, CA, 499--512. https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/lopes

Digital Library

[19]

Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P Brighten Godfrey, and Samuel Talmadge King. 2011. Debugging the data plane with anteater. ACM SIGCOMM Computer Communication Review 41, 4 (2011), 290--301.

Digital Library

[20]

Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, and George Varghese. 2016. Scaling network verification using symmetry and surgery. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 69--83.

Digital Library

[21]

Amir Pnueli. 1984. In Transition From Global to Modular Temporal Reasoning about Programs. In Logics and Models of Concurrent Systems (NATO ASI Series), Krzysztof R. Apt (Ed.), Vol. 13. Springer, 123--144.

[22]

Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable network configuration verification through model checking. (2020).

Digital Library

[23]

Tim Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. 2022. Kirigami, the Verifiable Art of Network Cutting. (2022).

[24]

Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. SIGPLAN Not. 51, 10 (Oct. 2016), 765--780.

Digital Library

[25]

Hongkun Yang and Simon S Lam. 2015. Real-time verification of network properties using atomic predicates. IEEE/ACM Transactions on Networking 24, 2 (2015), 887--900.

Digital Library

[26]

Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca. 2020. Accuracy, Scalability, Coverage: A Practical Configuration Verifier on a Global WAN. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM '20). Association for Computing Machinery, 599--614.

Digital Library

[27]

Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca. 2020. Accuracy, Scalability, Coverage: A Practical Configuration Verifier on a Global WAN. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM '20). Association for Computing Machinery, New York, NY, USA, 599--614.

Digital Library

[28]

Zen [n. d.]. Zen. https://github.com/microsoft/Zen. ([n. d.]).

Cited By

Nazari AZhang YRaghothaman MChen H(2024)Localized Explanations for Automatically Synthesized Network ConfigurationsProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696888(52-59)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696888
Chen H(2024)Interpretable Network Synthesis via Localized SpecificationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673889(51-53)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673889
Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Show More Cited By

Index Terms

Lightyear: Using Modularity to Scale BGP Control Plane Verification
1. Networks
  1. Network properties
    1. Network reliability

Recommendations

Neighbor-specific BGP: more flexible routing policies while improving global stability
SIGMETRICS '09

The Border Gateway Protocol (BGP) offers network administrators considerable flexibility in controlling how traffic flows through their networks. However, the interaction between routing policies in different Autonomous Systems (ASes) can lead to ...
Modeling and analyzing the convergence property of the BGP routing protocol in SPIN

The Border Gateway Protocol (BGP) is an interdomain routing protocol such that each autonomous system can independently formulate its routing policies. However, BGP does not always converge, because its routing policies may conflict and cause BGP to ...
Quantifying the BGP routes diversity inside a tier-1 network
NETWORKING'06: Proceedings of the 5th international IFIP-TC6 conference on Networking Technologies, Services, and Protocols; Performance of Computer and Communication Networks; Mobile and Wireless Communications Systems

Many large ISP networks today rely on route-reflection [1] to allow their iBGP to scale. Route-reflection was officially introduced to limit the number of iBGP sessions, compared to the $\frac{n\times(n-1)}{2}$ sessions required by an iBGP full-mesh. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference

September 2023

1217 pages

ISBN:9798400702365

DOI:10.1145/3603269

Chairs:
Henning Schulzrinne,
Vishal Misra,
Program Chairs:
Eddie Kohler,
David Maltz

Copyright © 2023 Owner/Author(s).

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGCOMM: ACM Special Interest Group on Data Communication

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2023

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ACM SIGCOMM '23

Sponsor:

SIGCOMM

ACM SIGCOMM '23: ACM SIGCOMM 2023 Conference

September 10, 2023

NY, New York, USA

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
967
Total Downloads

Downloads (Last 12 months)657
Downloads (Last 6 weeks)68

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nazari AZhang YRaghothaman MChen H(2024)Localized Explanations for Automatically Synthesized Network ConfigurationsProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696888(52-59)Online publication date: 18-Nov-2024
https://dl.acm.org/doi/10.1145/3696348.3696888
Chen H(2024)Interpretable Network Synthesis via Localized SpecificationsProceedings of the 2024 SIGCOMM Workshop on Formal Methods Aided Network Operation10.1145/3672199.3673889(51-53)Online publication date: 4-Aug-2024
https://dl.acm.org/doi/10.1145/3672199.3673889
Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
He SCunha IKatz-Bassett EVallina-Rodríguez NSuarez-Tángil GLevin DPelsser C(2024)RPSLyzer: Characterization and Verification of Policies in Internet Routing RegistriesProceedings of the 2024 ACM on Internet Measurement Conference10.1145/3646547.3689018(365-374)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3646547.3689018
Thijm TBeckett RGupta AWalker D(2024)Kirigami, the Verifiable Art of Network CuttingIEEE/ACM Transactions on Networking10.1109/TNET.2024.336037132:3(2447-2462)Online publication date: Jun-2024
https://doi.org/10.1109/TNET.2024.3360371
Fang XDing FHuang BWang ZHan GYang RYou LXiang QKong LLiu YShu J(2024)Network Can Help Check Itself: Accelerating SMT-based Network Configuration Verification Using Network Domain KnowledgeIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621215(2119-2128)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621215
Abdous SDiwangkara SGhorbani S(2024)Tempus: Probabilistic Network Latency VerificationIEEE Access10.1109/ACCESS.2024.349873712(169896-169909)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3498737
Liu XZhang PLi HSun W(2023)Modular Data Plane Verification for Compositional NetworksProceedings of the ACM on Networking10.1145/36291451:CoNEXT3(1-22)Online publication date: 28-Nov-2023
https://dl.acm.org/doi/10.1145/3629145

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents