Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Diagnosing and Repairing Distributed Routing Configurations Using Selective Symbolic Simulation

Rulan Yang, Hanyang Shao, Gao Han, Ziyi Wang, Xing Fang, Lizhao You, Qiao Xiang, Linghe Kong, Ruiting Zhou, Jiwu Shu

TL;DR

This work proposes S^2Sim, a novel system for automatic routing configuration diagnosis and repair that can find an intent-compliant variant by selectively simulating variants of the given configuration in a symbolic way, whose differences between the given configuration reveal the errors in the given configuration and suggest the patches.

Abstract

Although substantial progress has been made in automatically verifying whether distributed routing configurations conform to certain requirements, diagnosing and repairing configuration errors remains manual and time-consuming. To fill this gap, we propose S^2Sim, a novel system for automatic routing configuration diagnosis and repair. Our key insight is that by selectively simulating variants of the given configuration in a symbolic way, we can find an intent-compliant variant, whose differences between the given configuration reveal the errors in the given configuration and suggest the patches. Building on this insight, we also design techniques to support complex scenarios (e.g., multiple protocol networks) and requirements (e.g., k-link failure tolerance). We implement a prototype of S^2Sim and evaluate its performance using networks of size O(10) ~ O(1000) with synthetic real-world configurations. Results show that S^2Sim diagnoses and repairs errors for 1) all WAN configurations within 10 s and 2) all DCN configurations within 20 minutes.

Diagnosing and Repairing Distributed Routing Configurations Using Selective Symbolic Simulation

TL;DR

This work proposes S^2Sim, a novel system for automatic routing configuration diagnosis and repair that can find an intent-compliant variant by selectively simulating variants of the given configuration in a symbolic way, whose differences between the given configuration reveal the errors in the given configuration and suggest the patches.

Abstract

Although substantial progress has been made in automatically verifying whether distributed routing configurations conform to certain requirements, diagnosing and repairing configuration errors remains manual and time-consuming. To fill this gap, we propose S^2Sim, a novel system for automatic routing configuration diagnosis and repair. Our key insight is that by selectively simulating variants of the given configuration in a symbolic way, we can find an intent-compliant variant, whose differences between the given configuration reveal the errors in the given configuration and suggest the patches. Building on this insight, we also design techniques to support complex scenarios (e.g., multiple protocol networks) and requirements (e.g., k-link failure tolerance). We implement a prototype of S^2Sim and evaluate its performance using networks of size O(10) ~ O(1000) with synthetic real-world configurations. Results show that S^2Sim diagnoses and repairs errors for 1) all WAN configurations within 10 s and 2) all DCN configurations within 20 minutes.
Paper Structure (33 sections, 1 theorem, 11 figures, 2 tables)

This paper contains 33 sections, 1 theorem, 11 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Motivation
  3. Limitation of Existing Tools
  4. Technical Challenges
  5. Overview
  6. Why Do We Use Selective Symbolic Simulation
  7. Architecture of $S^2Sim$
  8. Basic Design
  9. Configuration Searching Space
  10. Configuration Variants Exploration
  11. Selective symbolic simulation
  12. Configuration Error Diagnosis and Repair
  13. Supporting Multiple Protocols
  14. Key Problems
  15. Our Solution
  16. ...and 18 more sections

Key Result

Proposition 1

Given a fault-tolerant requirement $req=(src, dst, n, P, k), k>0$. If we let the packet from $src$ to $dst$ with prefix $n$ be forwarded through the $(k+1)$ edge-disjoint paths $p_1, ..., p_{k+1}$, there must exist at least one path to forward the packet under an arbitrary k-link failure.

Figures (11)

  • Figure 1: An example network that illustrates the limitation of existing tools.
  • Figure 2: The architecture of $S^2Sim$.
  • Figure 3: The selective symbolic simulation of the example network.
  • Figure 4: An example network with multiple routing protocols for error diagnosis and repair.
  • Figure 5: An example network to diagnose and repair errors for $k$-link failure tolerance ($k$=1).
  • ...and 6 more figures

Theorems & Definitions (2)

  • Proposition 1
  • proof