research-article

Efficient synthesis of network updates

Authors:

Jedidiah McClurg,

Hossein Hojjat,

Nate FosterAuthors Info & Claims

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 196 - 207

https://doi.org/10.1145/2737924.2737980

Published: 03 June 2015 Publication History

Abstract

Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN programmers because networks are distributed systems with hundreds or thousands of interacting nodes. Even if initial and final configurations are correct, naively updating individual nodes can lead to incorrect transient behaviors, including loops, black holes, and access control violations. This paper presents an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. We formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. We describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating that our tool scales to updates involving over one-thousand nodes.

References

[1]

M. Al-Fares, A. Loukissas, and A. Vahdat. A Scalable, Commodity Data Center Network Architecture. In SIGCOMM, 2008.

Digital Library

[2]

E. Al-Shaer and S. Al-Haj. FlowChecker: Configuration Analysis and Verification of Federated OpenFlow Infrastructures. In SafeConfig, 2010.

Digital Library

[3]

M. Alizadeh, A. Greenberg, D. Maltz, J. Padhye, P. Patel, B. Prabhakar, S. Sengupta, and M. Sridharan. Data Center TCP (DCTCP). In SIGCOMM, pages 63–74, 2010.

Digital Library

[4]

G. Berry and G. Boudol. The Chemical Abstract Machine. In POPL, pages 81–94, 1990.

Digital Library

[5]

A. Bradley. SAT-Based Model Checking without Unrolling. In VMCAI, 2011.

Digital Library

[6]

M. Casado, N. Foster, and A. Guha. Abstractions for Software-Defined Networks. CACM, 57(10):86–95, Oct. 2014.

Digital Library

[7]

H. Chockler, A. Ivrii, A. Matsliah, S. Moran, and Z. Nevo. Incremental Formal Verification of Hardware. In FMCAD, pages 135–143, 2011.

Digital Library

[8]

N. Foster, R. Harrison, M. Freedman, C. Monsanto, J. Rexford, A. Story, and D. Walker. Frenetic: A Network Programming Language. In ICFP, pages 279–291, 2011.

Digital Library

[9]

P. Francois and O. Bonaventure. Avoiding Transient Loops during the Convergence of Link-state Routing Protocols. IEEE/ACM Transactions on Networking, 15(6):1280–1292, 2007.

Digital Library

[10]

P. Francois, O. Bonaventure, B. Decraene, and P.-A. Coste. Avoiding Disruptions during Maintenance Operations on BGP Sessions. IEEE Transactions on Network and Service Management, 4(3):1–11, 2007.

Digital Library

[11]

A. Guha, M. Reitblatt, and N. Foster. Machine-Verified Network Controllers. In PLDI, June 2013.

Digital Library

[12]

P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. Concurrent Data Representation Synthesis. In PLDI, pages 417–428, June 2012.

Digital Library

[13]

C.-Y. Hong, S. Kandula, R. Mahajan, M. Zhang, V. Gill, M. Nanduri, and R. Wattenhofer. Achieving High Utilization with Software-Driven WAN. In SIGCOMM, pages 15–26, Aug. 2012.

Digital Library

[14]

S. Jain, A. Kumar, S. Mandal, J. Ong, L. Poutievski, A. Singh, S. Venkata, J. Wanderer, J. Zhou, M. Zhu, J. Zolla, U. Hölzle, S. Stuart, and A. Vahdat. B4: Experience with a Globally-deployed Software Defined WAN. In SIGCOMM, 2013.

Digital Library

[15]

X. Jin, H. Liu, R. Gandhi, S. Kandula, R. Mahajan, M. Zhang, J. Rexford, and R. Wattenhofer. Dynamic Scheduling of Network Updates. In SIGCOMM, pages 539–550, 2014.

Digital Library

[16]

J. P. John, E. Katz-Bassett, A. Krishnamurthy, T. Anderson, and A. Venkataramani. Consensus Routing: The Internet as a Distributed System. In NSDI, pages 351–364, 2008.

Digital Library

[17]

N. P. Katta, J. Rexford, and D. Walker. Incremental Consistent Updates. In HotSDN, pages 49–54. ACM, 2013.

Digital Library

[18]

P. Kazemian, G. Varghese, and N. McKeown. Header Space Analysis: Static Checking for Networks. In NSDI, 2012.

Digital Library

[19]

P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real Time Network Policy Checking Using Header Space Analysis. NSDI, pages 99–112, 2013.

Digital Library

[20]

A. Khurshid, W. Zhou, M. Caesar, and P. Godfrey. VeriFlow: Verifying Network-wide Invariants in Real Time. ACM SIGCOMM CCR, 2012.

Digital Library

[21]

S. Knight, H. Nguyen, N. Falkner, R. Bowden, and M. Roughan. The Internet Topology Zoo. IEEE Journal on Selected Areas in Communications, 29(9):1765–1775, Oct. 2011.

[22]

A. Lazaris, D. Tahara, X. Huang, L. Li, A. Voellmy, Y. Yang, and M. Yu. Tango: Simplifying SDN Programming with Automatic Switch Behavior Inference, Abstraction, and Optimization. 2014.

[23]

H. H. Liu, X. Wu, M. Zhang, L. Yuan, R. Wattenhofer, and D. Maltz. zUpdate: Updating Data Center Networks with Zero Loss. In SIGCOMM, pages 411–422. ACM, 2013.

Digital Library

[24]

A. Ludwig, M. Rost, D. Foucard, and S. Schmid. Good Network Updates for Bad Packets: Waypoint Enforcement Beyond Destination-Based Routing Policies. In HotNets, 2014.

Digital Library

[25]

R. Mahajan and R. Wattenhofer. On Consistent Updates in Software Defined Networks. In SIGCOMM, Nov. 2013.

Digital Library

[26]

H. Mai, A. Khurshid, R. Agarwal, M. Caesar, P. Godfrey, and S. T. King. Debugging the Data Plane with Anteater. In SIGCOMM, 2011.

Digital Library

[27]

R. Majumdar, S. Tetali, and Z. Wang. Kuai: A Model Checker for Software-defined Networks. In FMCAD, 2014.

Digital Library

[28]

N. McKeown, T. Anderson, H. Balakrishnan, G. Parulkar, L. Peterson, J. Rexford, S. Shenker, and J. Turner. OpenFlow: Enabling Innovation in Campus Networks. ACM SIGCOMM CCR, 2008.

Digital Library

[29]

M. E. Newman, S. H. Strogatz, and D. J. Watts. Random Graphs with Arbitrary Degree Distributions and their Applications. 2001.

[30]

A. Noyes, T. Warszawski, and N. Foster. Toward Synthesis of Network Updates. In SYNT, July 2013.

[31]

Open Networking Foundation. OpenFlow 1.4 Specification, 2013.

[32]

S. Raza, Y. Zhu, and C.-N. Chuah. Graceful Network State Migrations. IEEE/ACM Transactions on Networking, 19(4):1097–1110, 2011.

Digital Library

[33]

M. Reitblatt, N. Foster, J. Rexford, C. Schlesinger, and D. Walker. Abstractions for Network Update. In SIGCOMM, 2012.

Digital Library

[34]

O. Sokolsky and S. Smolka. Incremental Model Checking in the Modal Mu-Calculus. In CAV, pages 351–363, 1994.

Digital Library

[35]

A. Solar-Lezama, C. G. Jones, and R. Bodik. Sketching Concurrent Data Structures. In PLDI, pages 136–148, 2008.

Digital Library

[36]

L. Vanbever, S. Vissicchio, C. Pelsser, P. Francois, and O. Bonaventure. Seamless Network-wide IGP Migrations. In SIGCOMM, 2011.

Digital Library

[37]

M. Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In LICS, 1986.

[38]

M. Vechev, E. Yahav, and G. Yorsh. Abstraction-guided Synthesis of Synchronization. In POPL, pages 327–338, 2010.

Digital Library

[39]

P. Wolper, M. Y. Vardi, and A. P. Sistla. Reasoning about Infinite Computation Paths (Extended Abstract). In FOCS, 1983.

Digital Library

[40]

W. Zhou, D. Jin, J. Croft, M. Caesar, and B. Godfrey. Enforcing Generalized Consistency Properties in Software-Defined Networks. In NSDI, 2015.

Digital Library

Cited By

Györgyi CLarsen KSchmid SSrba J(2024)SyPer: Synthesis of Perfectly Resilient Local Fast Re-Routing Rules for Highly Dependable NetworksIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621323(2398-2407)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621323
Räcke HSchmid SVintan R(2024)Fast Algorithms for Loop-Free Network Updates using Linear Programming and Local SearchIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621077(1930-1939)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621077
Yusuf MBin Abu Bakar KIsyaku BMukhlif F(2023)Distributed Controller Placement in Software-Defined Networks with Consistency and Interoperability ProblemsJournal of Electrical and Computer Engineering10.1155/2023/64669962023Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1155/2023/6466996
Show More Cited By

Recommendations

Efficient synthesis of network updates
PLDI '15

Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN ...
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Handling loops in bounded model checking of C programs via k-induction

The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2015

630 pages

ISBN:9781450334686

DOI:10.1145/2737924

General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

ACM SIGPLAN Notices Volume 50, Issue 6
PLDI '15
June 2015
630 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2813885
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part 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 components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 June 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PLDI '15

Sponsor:

SIGPLAN

PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 13 - 17, 2015

OR, Portland, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

94
Total Citations
View Citations
567
Total Downloads

Downloads (Last 12 months)25
Downloads (Last 6 weeks)9

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Györgyi CLarsen KSchmid SSrba J(2024)SyPer: Synthesis of Perfectly Resilient Local Fast Re-Routing Rules for Highly Dependable NetworksIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621323(2398-2407)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621323
Räcke HSchmid SVintan R(2024)Fast Algorithms for Loop-Free Network Updates using Linear Programming and Local SearchIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621077(1930-1939)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621077
Yusuf MBin Abu Bakar KIsyaku BMukhlif F(2023)Distributed Controller Placement in Software-Defined Networks with Consistency and Interoperability ProblemsJournal of Electrical and Computer Engineering10.1155/2023/64669962023Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1155/2023/6466996
Wang YLi ZJiang CQiu XRao S(2023)Comparative Synthesis: Learning Near-Optimal Network Designs by QueryProceedings of the ACM on Programming Languages10.1145/35711977:POPL(91-120)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571197
Larsen KMariegaard ASchmid SSrba J(2023)AllSynthScience of Computer Programming10.1016/j.scico.2023.102992230:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.scico.2023.102992
Schmid SSchrenk BTorralba A(2022)NetStack: A Game Approach to Synthesizing Consistent Network Updates2022 IFIP Networking Conference (IFIP Networking)10.23919/IFIPNetworking55013.2022.9829770(1-9)Online publication date: 13-Jun-2022
https://doi.org/10.23919/IFIPNetworking55013.2022.9829770
Henzinger MPaz APourdamghani ASchmid S(2022)The augmentation-speed tradeoff for consistent network updatesProceedings of the Symposium on SDN Research10.1145/3563647.3563655(67-80)Online publication date: 19-Oct-2022
https://dl.acm.org/doi/10.1145/3563647.3563655
Lembke JRavi SRoman PEugster P(2022)Secure and Reliable Network UpdatesACM Transactions on Privacy and Security10.1145/355654226:1(1-41)Online publication date: 9-Nov-2022
https://dl.acm.org/doi/10.1145/3556542
Dolati MKhonsari AGhaderi M(2022)Minimizing Update Makespan in SDNs Without TCAM OverheadIEEE Transactions on Network and Service Management10.1109/TNSM.2022.314697119:2(1598-1613)Online publication date: Jun-2022
https://doi.org/10.1109/TNSM.2022.3146971
Bringhenti DValenza F(2022)Optimizing distributed firewall reconfiguration transientsComputer Networks: The International Journal of Computer and Telecommunications Networking10.1016/j.comnet.2022.109183215:COnline publication date: 9-Oct-2022
https://dl.acm.org/doi/10.1016/j.comnet.2022.109183
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents