Campion: debugging router configuration differences
Campion: debugging router configuration differences
复制标题
DOI：
10.1145/3452296.3472925
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
Alan Tang;S. Kakarla;Ryan Beckett;Ennan Zhai;Matt Brown;T. Millstein;Y. Tamir;G. Varghese
中科院分区：
文献类型：
--
作者：
Alan Tang;S. Kakarla;Ryan Beckett;Ennan Zhai;Matt Brown;T. Millstein;Y. Tamir;G. Varghese
我们提出了一种新方法，用于调试两种旨在在行为上等效的路由器配置。现有的路由器验证技术无法识别所有差异或将这些差异定位到相关配置线路。我们的方法通过_ modular_分析解决了这些局限性，该分析分别分析了相应的配置组件对。它处理影响路由和转发的所有路由器组件，包括BGP，OSPF，静态路由，路由图和ACL的配置。此外，对于许多配置组件，我们的模块化方法可以使用简单的_结构等价_检查，而无需额外丢失精度与模块化语义检查，从而有助于效率和错误定位。我们在工具坎普（Campion）中实现了这种方法，并将其应用于从不同制造商的备用路由器对备用组件进行调试，并验证了关键路由器的更换。 Campion在生产云网络中分析了30个建议的路由器替换，并主动检测到了四个配置错误，其中包括可能导致严重中断的路线反射器错误。 Campion还发现大学网络中不同供应商的备份路由器之间存在多种差异。这些尚未发现三年，并取决于操作员所说的微妙的语义差异，而这些差异“极不可能”通过“仅仅打动配置”来检测。
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."