Diagnosing and Repairing Distributed Routing Configurations Using Selective Symbolic Simulation

Although substantial progress has been made in automatically verifying whether distributed routing configurations comply with certain intents, diagnosing and repairing configuration errors remains manual and time-consuming. To fill this gap, we propose S 2 Sim, a novel system for automatic routing configuration diagnosis and repair. Our key insight is that by deriving a set of contracts that guarantees an intent-compliant variant of the erroneous configuration, we can systematically check for all contract violations in the configuration via symbolic simulation to pinpoint and repair the errors. S 2 Sim also introduces a series of extensions to support complex configurations (e.g., ACL, route aggregation and multi-path routing), networks (e.g., underlay and overlay networks), and intents (e.g., k-link failure tolerance). We fully implement S 2 Sim and evaluate its performance using real configurations from two major providers and synthesized configurations composed from their real errors and real-world topologies with different scales O(10) to O(1000). Results show that S 2 Sim accurately and efficiently diagnoses and repairs real configuration errors (i.e., up to 20 seconds in real networks of O(100) nodes and up to 15 minutes in synthesized networks of O(1000) nodes). F's configuration snippet 1 ip as-path al1 permit C 2 ! 3 route-map setLP permit 10 4 match as-path al1 5 set local-preference 200 6 ! 7 route-map setLP permit 20 8 set local-preference 80 9 ! 10 bgp F 11 neighbor A route-map setLP in 12 neighbor E route-map setLP in 13 ! Intents: (1) All routers can reach p (2) A must waypoint C (3) F must avoid B Forwarding path D C E B A F p C's configuration snippet 1 ip prefix-list pl1 seq 5 permit p 2 ! 3 route-map filter deny 10 4 match ip address prefix-list pl1 5 ! 6 route-map filter permit 20 7 ! 8 bgp C 9 neighbor B route-map filter out 10 !