We present a new approach for debugging two router configurations that are intended to be behaviorally equivalent. Existing router verification techniques cannot identify all differences or localize those differences to relevant configuration lines. Our approach addresses these limitations through a modular analysis, which separately analyzes pairs of corresponding configuration components. It handles all router components that affect routing and forwarding, including configuration for BGP, OSPF, static routes, route maps and ACLs. Further, for many configuration components our modular approach enables simple structural equivalence checks to be used without additional loss of precision versus modular semantic checks, aiding both efficiency and error localization. We implemented this approach in the tool Campion and applied it to debugging pairs of backup routers from different manufacturers and validating replacement of critical routers. Campion analyzed 30 proposed router replacements in a production cloud network and proactively detected four configuration bugs, including a route reflector bug that could have caused a severe outage. Campion also found multiple differences between backup routers from different vendors in a university network. These were undetected for three years, and depended on subtle semantic differences that the operators said they were “highly unlikely” to detect by “just eyeballing the configs.”

BibTeX Citation

    author = {Tang, Alan and
              Kakarla, Siva Kesava Reddy and
              Beckett, Ryan and
              Zhai, Ennan and
              Brown, Matt and
              Millstein, Todd and
              Tamir, Yuval and
              Varghese, George},
    title = {Campion: Debugging Router Configuration Differences},
    year = {2021},
    isbn = {9781450383837},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    url = {https://doi.org/10.1145/3452296.3472925},
    doi = {10.1145/3452296.3472925},
    booktitle = {Proceedings of the 2021 ACM SIGCOMM 2021 Conference},
    pages = {748–761},
    numpages = {14},
    keywords = {error localization, network verification, modular reasoning, equivalence checking},
    location = {Virtual Event, USA},
    series = {SIGCOMM '21}