Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/3132747.3132753acmconferencesArticle/Chapter ViewAbstractPublication PagessospConference Proceedingsconference-collections
research-article
Public Access

Automatically Repairing Network Control Planes Using an Abstract Representation

Published: 14 October 2017 Publication History

Abstract

The forwarding behavior of computer networks is governed by the configuration of distributed routing protocols and access filters---collectively known as the network control plane. Unfortunately, control plane configurations are often buggy, causing networks to violate important policies: e.g., specific traffic classes (defined in terms of source and destination endpoints) should always be able to reach their destination, or always traverse a waypoint. Manually repairing these configurations is daunting because of their inter-twined nature across routers, traffic classes, and policies.
Inspired by recent work in automatic program repair, we introduce CPR, a system that automatically computes correct, minimal repairs for network control planes. CPR casts configuration repair as a MaxSMT problem whose constraints are based on a digraph-based representation of a control plane's semantics. Crucially, this representation must capture the dependencies between traffic classes arising from the cross-traffic-class nature of control plane constructs. The MaxSMT formulation must account for these dependencies whilst also accounting for all policies and preferring repairs that minimize the size (e.g., number of lines) of the configuration changes. Using configurations from 96 data center networks, we show that CPR produces repairs in less than a minute for 98% of the networks, and these repairs requiring changing the same or fewer lines of configuration than hand-written repairs in 79% of cases.

Supplementary Material

MP4 File (auto_repair.mp4)

References

[1]
https://bitbucket.org/uw-madison-networking-research/arc.
[2]
Cisco IOS configuration fundamentals command reference. http//:www.cisco.com/c/en/us/td/docs/ios/fundamentals/command/reference/cf_book.pdf.
[3]
The z3 theorem prover. https://github.com/Z3Prover/z3.
[4]
R. Aharoni and E. Berger. Menger's theorem for infinite graphs. Inventiones mathematicae, 2008.
[5]
M. Al-Fares, A. Loukissas, and A. Vahdat. A scalable, commodity data center network architecture. In SIGCOMM, 2008.
[6]
A. Arcuri. On the automation of fixing software bugs. In International Conference on Software Engineering (ICSE), 2008.
[7]
R. Beckett, A. Gupta, R. Mahajan, and D. Walker. A general approach to network configuration verification. In SIGCOMM, 2017.
[8]
R. Beckett, R. Mahajan, T. Millstein, J. Padhye, and D. Walker. Don't mind the gap: Bridging network-wide objectives and device-level configurations. In SIGCOMM, 2016.
[9]
T. Benson, A. Akella, and D. Maltz. Unraveling the complexity of network management. In Symposium on Networked Systems Design and Implementation (NSDI), 2009.
[10]
D. Burton and P. L. Toint. On an instance of the inverse shortest paths problem. Math. Program., 53:45--61, 1992.
[11]
D. Caldwell, S. Lee, and Y. Mandelbaum. Adaptive parsing of router configuration languages. In IEEE Internet Network Management Workshop (INM), 2008.
[12]
L. D'Antoni, R. Samanta, and R. Singh. Qlose: Program repair with quantiative objectives. In International Conference on Computer Aided Verification (CAV), 2016.
[13]
V. Debroy and W. E. Wong. Using mutation to automatically suggest fixes for faulty programs. In International Conference on Software Testing, Verification and Validation (ICST), 2010.
[14]
F. Demarco, J. Xuan, D. L. Berre, and M. Monperrus. Automatic repair of buggy if conditions and missing preconditions with SMT. In International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA), 2014.
[15]
A. El-Hassany, P. Tsankov, L. Vanbever, and M. Vechev. Network-wide configuration synthesis. Technical Report 1611.02537, arXiv, 2016.
[16]
S. K. Fayaz, T. Sharma, A. Fogel, R. Mahajan, T. D. Millstein, V. Sekar, and G. Varghese. Efficient network reachability analysis using a succinct control plane representation. In Symposium on Operating Systems Design and Implementation (OSDI), 2016.
[17]
N. Feamster and H. Balakrishnan. Detecting BGP configuration faults with static analysis. In Symposium on Networked Systems Design and Implementation (NSDI), 2005.
[18]
A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein. A general approach to network configuration analysis. In Symposium on Networked Systems Design and Implementation (NSDI), 2015.
[19]
E. W. Fulp. Optimization of network firewall policies using directed acyclic graphs. In IEEE Internet Mgmt Conf, 2005.
[20]
A. Gember-Jacobson, R. Viswanathan, A. Akella, and R. Mahajan. Fast control plane analysis using an abstract representation. In SIGCOMM, 2016.
[21]
A. Gember-Jacobson, R. Viswanathan, A. Akella, and R. Mahajan. Fast control plane analysis using an abstract representation. Technical Report TR1838, University of Wisconsin-Madison, 2016.
[22]
A. Gember-Jacobson, W. Wu, X. Li, A. Akella, and R. Mahajan. Management plane analytics. In Internet Measurement Conference (IMC), 2015.
[23]
D. Gopinath, M. Z. Malik, and S. Khurshid. Specification-based program repair using SAT. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2011.
[24]
A. Griesmayer, R. Bloem, and B. Cook. Repair of boolean programs with an application to C. In International Conference on Computer Aided Verification (CAV), 2006.
[25]
H. Hojjat, P. Rümmer, J. McClurg, P. Cerný, and N. Foster. Optimizing horn solvers for network repair. In Formal Methods in Computer-Aided Design (FMCAD), 2016.
[26]
P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real time network policy checking using header space analysis. In Symposium on Networked Systems Design and Implementation (NSDI), 2013.
[27]
P. Kazemian, G. Varghese, and N. McKeown. Header space analysis: Static checking for networks. In Symposium on Networked Systems Design and Implementation (NSDI), 2012.
[28]
A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. B. Godfrey. Veri-Flow: Verifying network-wide invariants in real time. In Symposium on Networked Systems Design and Implementation (NSDI), 2013.
[29]
E. Kneuss, M. Koukoutos, and V. Kuncak. Deductive program repair. In Computer Aided Verification (CAV), 2015.
[30]
R. Könighofer and R. Bloem. Automated error localization and correction for imperative programs. In International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2011.
[31]
F. Le, G. G. Xie, D. Pei, J. Wang, and H. Zhang. Shedding light on the glue logic of the internet routing architecture. In SIGCOMM, 2008.
[32]
C. Le Goues, M. Dewey-Vogt, S. Forrest, and W. Weimer. A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 each. In International Conference on Software Engineering (ICSE), 2012.
[33]
F. Logozzo and T. Ball. Modular and verified automatic program repair. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2012.
[34]
R. Mahajan, D. Wetherall, and T. E. Anderson. Understanding BGP misconfiguration. In SIGCOMM, 2002.
[35]
H. Mai, A. Khurshid, R. Agarwal, M. Caesar, P. B. Godfrey, and S. T. King. Debugging the data plane with Anteater. In SIGCOMM, 2011.
[36]
G. S. Malkin. Rip version 2. STD 56, RFC Editor, November 1998. http//:www.rfc-editor.org/rfc/rfc2453.txt.
[37]
S. Mechtaev, J. Yi, and A. Roychoudhury. Directfix: Looking for simple program repairs. In International Conference on Software Engineering (ICSE), 2015.
[38]
J. Moy. Ospf version 2. STD 54, RFC Editor, April 1998. http//:www.rfc-editor.org/rfc/rfc2328.txt.
[39]
S. Narain, G. Levin, S. Malik, and V. Kaul. Declarative infrastructure configuration synthesis and debugging. Journal of Network and Systems Management, 16(3):235--258, Sept. 2008.
[40]
H. D. T. Nguyen, D. Qi, A. Roychoudhury, and S. Chandra. Semfix: program repair via semantic analysis. In International Conference on Software Engineering (ICSE), 2013.
[41]
Y. Rekhter, T. Li, and S. Hares. A border gateway protocol 4 (bgp-4). RFC 4271, RFC Editor, January 2006. http//:www.rfc-editor.org/rfc/rfc4271.txt.
[42]
R. Samanta, J. V. Deshmukh, and E. A. Emerson. Automatic generation of local repairs for boolean programs. In Formal Methods in Computer-Aided Design (FMCAD), 2008.
[43]
R. Stoenescu, M. Popovici, L. Negreanu, and C. Raiciu. Symnet: Scalable symbolic execution for modern networks. In SIGCOMM, 2016.
[44]
Y.-W. E. Sung, X. Tie, S. H. Wong, and H. Zeng. Robotron: Top-down network management at facebook scale. In SIGCOMM, 2016.
[45]
C. von Essen and B. Jobstmann. Program repair without regret. In International Conference on Computer Aided Verification (CAV), 2013.
[46]
W. Weimer, T. Nguyen, C. Le Goues, and S. Forrest. Automatically finding patches using genetic programming. In International Conference on Software Engineering (ICSE), 2009.
[47]
Y. Wu, A. Chen, A. Haeberlen, W. Zhou, and B. T. Loo. Automated bug removal for software-defined networks. In Symposium on Networked Systems Design and Implementation (NSDI), 2017.
[48]
Y. Yuan, R. Alur, and B. T. Loo. NetEgg: Programming network policies by examples. In Workshop on Hot Topics in Networks (HotNets), 2014.
[49]
P. Zave, R. A. Ferreira, X. K. Zou, M. Morimoto, and J. Rexford. Dynamic service chaining with dysco. In SIGCOMM, 2017.
[50]
H. Zeng, P. Kazemian, G. Varghese, and N. McKeown. A survey on network troubleshooting. Technical Report TR12-HPNG-061012, Stanford University, June 2012.

Cited By

View all
  • (2024)A Review of Intelligent Configuration and Its Security for Complex NetworksChinese Journal of Electronics10.23919/cje.2023.00.00133:4(920-947)Online publication date: Jul-2024
  • (2024)Automatic Configuration RepairProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696895(213-220)Online publication date: 18-Nov-2024
  • (2024)Kirigami, the Verifiable Art of Network CuttingIEEE/ACM Transactions on Networking10.1109/TNET.2024.336037132:3(2447-2462)Online publication date: Jun-2024
  • Show More Cited By

Index Terms

  1. Automatically Repairing Network Control Planes Using an Abstract Representation

    Recommendations

    Comments

    Please enable JavaScript to view thecomments powered by Disqus.

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    SOSP '17: Proceedings of the 26th Symposium on Operating Systems Principles
    October 2017
    677 pages
    ISBN:9781450350853
    DOI:10.1145/3132747
    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 ACM 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

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 14 October 2017

    Permissions

    Request permissions for this article.

    Check for updates

    Qualifiers

    • Research-article
    • Research
    • Refereed limited

    Funding Sources

    Conference

    SOSP '17
    Sponsor:

    Acceptance Rates

    Overall Acceptance Rate 174 of 961 submissions, 18%

    Upcoming Conference

    SOSP '25
    ACM SIGOPS 31st Symposium on Operating Systems Principles
    October 13 - 16, 2025
    Seoul , Republic of Korea

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)127
    • Downloads (Last 6 weeks)22
    Reflects downloads up to 24 Nov 2024

    Other Metrics

    Citations

    Cited By

    View all
    • (2024)A Review of Intelligent Configuration and Its Security for Complex NetworksChinese Journal of Electronics10.23919/cje.2023.00.00133:4(920-947)Online publication date: Jul-2024
    • (2024)Automatic Configuration RepairProceedings of the 23rd ACM Workshop on Hot Topics in Networks10.1145/3696348.3696895(213-220)Online publication date: 18-Nov-2024
    • (2024)Kirigami, the Verifiable Art of Network CuttingIEEE/ACM Transactions on Networking10.1109/TNET.2024.336037132:3(2447-2462)Online publication date: Jun-2024
    • (2024)When debugging encounters artificial intelligence: state of the art and open challengesScience China Information Sciences10.1007/s11432-022-3803-967:4Online publication date: 21-Feb-2024
    • (2024)Autonomous Attack Mitigation Through Firewall ReconfigurationInternational Journal of Network Management10.1002/nem.2307Online publication date: 20-Oct-2024
    • (2023)Automation for Network Security Configuration: State of the Art and Research TrendsACM Computing Surveys10.1145/361640156:3(1-37)Online publication date: 5-Oct-2023
    • (2023)Beyond a Centralized Verifier: Scaling Data Plane Checking via Distributed, On-Device VerificationProceedings of the ACM SIGCOMM 2023 Conference10.1145/3603269.3604843(152-166)Online publication date: 10-Sep-2023
    • (2023)Chroma: Learning and Using Network Contexts to Reinforce Performance Improving ConfigurationsProceedings of the 29th Annual International Conference on Mobile Computing and Networking10.1145/3570361.3613256(1-16)Online publication date: 2-Oct-2023
    • (2023)Kano: Efficient Cloud Native Network Policy VerificationIEEE Transactions on Network and Service Management10.1109/TNSM.2022.322967520:3(3747-3764)Online publication date: Sep-2023
    • (2023)Automated Firewall Configuration in Virtual NetworksIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2022.316029320:2(1559-1576)Online publication date: 1-Mar-2023
    • Show More Cited By

    View Options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Login options

    Media

    Figures

    Other

    Tables

    Share

    Share

    Share this Publication link

    Share on social media