Diagnosing and Repairing Distributed Routing Configurations Using Selective Symbolic Simulation

This paper presents S^2Sim, a novel system that automatically diagnoses and repairs distributed routing configuration errors by selectively simulating symbolic configuration variants to identify intent-compliant fixes, demonstrating high efficiency across networks ranging from 10 to 1,000 nodes.

The Gist

Imagine you are the captain of a massive fleet of ships (the network). Your goal is to get cargo from Port A to Port B safely, avoiding storms and taking specific scenic routes. You have a massive, complex instruction manual (the routing configuration) that tells every ship exactly where to go.

Sometimes, a typo in the manual causes a ship to crash into a reef or take a wrong turn.

The Problem: "It's Broken, But Why?"

Currently, when the fleet gets lost, there are tools that can say, "Hey, the fleet is lost!" (This is Verification). But they are terrible at saying, "Oh, the error is on page 42, line 3, where the captain forgot to turn left."

Fixing the manual usually requires a human expert to read thousands of pages, guess what went wrong, and try to fix it. It's slow, frustrating, and prone to human error.

The Solution: S2Sim (The "Magic Spellchecker")

The paper introduces S2Sim, a new system that doesn't just find the error; it diagnoses the exact typo and repairs the manual automatically.

Here is how it works, using a simple analogy:

1. The "What If" Game (The Contract)

Instead of staring at the broken manual and trying to guess what's wrong, S2Sim plays a game of "What If?"

• The Goal: It asks, "What would the perfect, error-free manual look like that is almost identical to the one we have?"
• The Contract: It creates a set of "Golden Rules" (called Contracts). These are simple promises like: "Ship C must always talk to Ship B," or "Ship F must never take the route through the storm."
• The Insight: If the current manual breaks these Golden Rules, that's where the error is!

2. The "Ghost Ship" Simulation (Symbolic Simulation)

Now, S2Sim runs a simulation. But instead of just running the broken manual, it runs a "Ghost Ship" version.

• Imagine you are watching a movie of the fleet moving.
• When the real ships (the broken manual) try to do something wrong (like Ship C refusing to talk to Ship B), the Ghost Ship steps in and says, "No, no! Remember the Golden Rule? You must talk to Ship B."
• The Ghost Ship forces the fleet to follow the Golden Rules.
• The Magic: Every time the Ghost Ship has to "force" a change, it puts a red flag on the specific line in the manual that caused the problem.
  • Example: "Ah, the Ghost Ship had to override the manual here. The error is in the 'Export Policy' on Ship C."

3. The "Patch" (Repair)

Once S2Sim has found all the red flags, it doesn't just tell you the problem. It writes the fix.

• It uses a smart template system. Instead of rewriting the whole manual, it inserts a tiny, precise patch.
• Analogy: If the error was "Ship F prefers the stormy route," the patch doesn't delete the whole rulebook. It just adds a tiny note: "Ignore the stormy route for this specific cargo."
• It ensures that fixing one problem doesn't accidentally break another part of the fleet.

Why is this a Big Deal?

1. It Handles the "Big Mess" (Complexity)
Real networks are messy. They have:

• ACLs: Like bouncers at a club checking IDs.
• Route Aggregation: Grouping many small streets into one big highway.
• Multi-path: Taking two roads at once to avoid traffic.
• Failures: What if a bridge (link) collapses?

Old tools get confused by this complexity. S2Sim is like a master mechanic who understands that if a bridge collapses, the "Golden Rules" change, and it instantly recalculates the best detour without panicking.

2. It's Fast
The researchers tested S2Sim on networks with up to 1,000 nodes (a huge fleet).

• Old Tools: Could take hours or get stuck forever.
• S2Sim: Fixed real-world errors in 20 seconds and even massive synthetic networks in 15 minutes.

3. It Works with "Real" Mistakes
They tested it on actual configuration files from major cloud providers and telecom companies. It found and fixed the exact same types of mistakes that human engineers struggle with, like "I forgot to tell the router to talk to its neighbor" or "I set the wrong priority for this route."

The Bottom Line

Think of S2Sim as a self-driving car for network engineers.

• Old way: You drive the car, it hits a wall, you get out, read the manual, guess why, and try to fix it.
• S2Sim way: The car senses it's about to hit a wall, instantly calculates the perfect path to avoid it, and rewrites its own GPS instructions so it never makes that mistake again.

It turns a days-long, headache-inducing debugging session into a quick, automated fix, ensuring the internet stays connected and safe.

Technical Summary

Here is a detailed technical summary of the paper "Diagnosing and Repairing Distributed Routing Configurations Using Selective Symbolic Simulation" (S2Sim).

1. Problem Statement

While significant progress has been made in automatically verifying whether distributed routing configurations comply with specific network intents (e.g., reachability, loop-freeness, waypointing), the subsequent steps of diagnosing the root cause of errors and repairing them remain largely manual, time-consuming, and error-prone.

Existing Control Plane Verification (CPV) tools face several limitations:

• Verification-only tools (e.g., Batfish, Minesweeper): Can detect that a configuration is erroneous and provide counter-examples but cannot pinpoint the specific configuration lines causing the error or suggest a fix.
• Repair tools (e.g., CEL, CPR, ACR):
  • CEL: Uses SMT solvers but fails on AS-path related configurations due to path encoding explosion.
  • CPR: Uses constraint programming on abstract graphs but cannot handle local preference configurations.
  • ACR: Relies on trial-and-error and test coverage, often missing latent errors or requiring excessive iterations.
• Latent Errors: Many tools fail to identify errors that have not yet caused a failure but will do so once other configurations are updated.

The core challenge is to accurately and efficiently locate the specific configuration snippets responsible for intent violations and generate a minimal, conflict-free repair patch.

2. Methodology: S2Sim

The authors propose S2Sim, a system that shifts the paradigm from "analyzing what went wrong" to "finding a compliant variant and comparing differences." The core insight is that if an intent-compliant variant of the erroneous configuration can be found, the differences between the two reveal the errors and the necessary repairs.

S2Sim operates through three key design pillars (D1-D3):

D1: Deriving Intent-Compliant Contracts & Selective Symbolic Simulation

Instead of searching for a concrete configuration, S2Sim derives a set of contracts (Boolean predicates) that guarantee an intent-compliant data plane.

1. Contract Derivation:
   • S2Sim computes an intent-compliant data plane that is as close as possible to the original erroneous data plane (minimizing changes).
   • It uses DFA multiplication to find valid paths for unsatisfied intents while reusing existing valid paths.
   • From this compliant data plane, it derives intent-compliant contracts (e.g., isPeered, isImported, isExported, isPreferred) which represent the necessary conditions for the network to function correctly.
2. Selective Symbolic Simulation:
   • S2Sim simulates the original erroneous configuration symbolically.
   • At each step, it checks if the router's behavior violates the derived contracts.
   • If a violation is detected, the simulation forces the behavior to obey the contract and switches to a symbolic variant of the configuration.
   • This process continues until the simulation converges to the intent-compliant data plane.
   • Result: All violated contracts are recorded, mapping directly to specific configuration snippets (e.g., a specific route-map rule).

D2: Assume-Guarantee for Multi-Protocol Networks

To handle complex networks with layered protocols (e.g., OSPF as underlay and BGP as overlay):

• S2Sim uses an assume-guarantee approach.
• It first assumes the underlay (e.g., OSPF) is functioning correctly and diagnoses/repairs the overlay (e.g., BGP).
• The repaired overlay's requirements then become the intents for the underlay, which is subsequently diagnosed and repaired.
• This modular approach handles dependencies between different routing protocols (path-vector and link-state).

D3: Fault-Tolerant Repair (k-Link Failure)

To ensure configurations remain compliant even under $k$ link failures:

• S2Sim computes $k+1$ edge-disjoint paths for each intent (based on the Pigeonhole Principle).
• It derives fault-tolerant contracts ensuring that at least one valid path exists regardless of which $k$ links fail.
• The selective symbolic simulation is extended to check for contract violations under these fault-tolerant constraints.

Repair Mechanism: Contract-Specific Templates

Once errors are localized, S2Sim generates repair patches using constraint programming:

• Instead of solving a massive global constraint problem (which leads to unsatisfiable solutions due to conflicts), S2Sim uses contract-specific templates.
• For each violated contract, it inserts a new, fine-grained rule (e.g., matching a specific prefix or AS-path) before the existing rule.
• The action of this new rule is modeled as a symbolic variable and solved independently. This ensures that repairs for different prefixes do not conflict on the same configuration snippet.

3. Key Contributions

1. Novel Paradigm: Introduces a "variant-comparison" approach using selective symbolic simulation to diagnose and repair routing configurations, avoiding the NP-complete enumeration of counter-examples.
2. Contract-Based Abstraction: Defines a comprehensive set of routing contracts (peering, import, export, preference) that map directly to configuration snippets, enabling precise error localization.
3. Scalability & Complexity Handling:
   • Supports complex configurations including ACLs, route aggregation, multi-path routing (ECMP), and AS-path filtering.
   • Handles multi-protocol networks (OSPF/BGP) via assume-guarantee decomposition.
   • Supports fault tolerance ($k$-link failure) by computing edge-disjoint paths.
4. Template-Based Repair: Solves the issue of conflicting repairs by using fine-grained templates, ensuring satisfiable solutions for complex policy interactions.

4. Evaluation Results

The authors implemented S2Sim as a plugin for Batfish and evaluated it using:

• Real-world data: Configurations from two major providers (Data Center WAN and IP Radio Access Networks).
• Synthesized data: Networks ranging from $O(10)$ to $O(1000)$ nodes, with injected real-world error types.

Key Findings:

• Accuracy: S2Sim successfully diagnosed and repaired 100% of the injected error types (including AS-path filters, local preferences, and multi-protocol issues) that existing tools (CEL, CPR) failed to handle.
• Efficiency:
  • Real Networks ($O(100)$ nodes): Diagnosis and repair completed in ~20 seconds.
  • Synthesized Large Networks ($O(1000)$ nodes): Completed in ~15 minutes.
  • Speedup: S2Sim achieved >10x speedup compared to state-of-the-art tools (CEL and CPR) in both reachability and fault-tolerant scenarios.
• Scalability:
  • Runtime is linear with respect to the number of intents.
  • Runtime is quadratic with respect to network scale (dominated by the second simulation step).
  • Error type and error count have negligible impact on runtime.

5. Significance

S2Sim represents a significant advancement in Network Configuration Management (NetConf). It bridges the gap between verification (detecting errors) and automation (fixing errors). By moving away from brute-force enumeration and leveraging symbolic simulation guided by intent-compliant contracts, S2Sim offers a practical, scalable, and accurate solution for maintaining the reliability of large-scale, complex distributed networks. It addresses the "last mile" problem in network verification, enabling operators to automatically recover from configuration drifts and errors without manual intervention.