Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

CB-VER: A Stable Foundation for Modular Control Plane Verification

Dexin Zhang, Timothy Alberdingk Thijm, David Walker, Aarti Gupta

Abstract

Network operators are often interested in verifying \emph{eventually-stable properties} of network control planes: properties of control plane states that hold eventually, and hold forever thereafter, provided the operating environment remains unchanged. Examples include eventually-stable reachability, access control, or path length properties. In this work, we introduce \textsc{CB-Ver}, a new framework for verifying such properties, based on the key idea of a \emph{converges-before graph} (CB-graph for short). When a user provides interfaces for each network component, \textsc{CB-Ver} checks the necessary component-by-component requirements in parallel using an SMT solver. In addition, the tool automatically synthesizes a CB-graph and checks whether it connects all nodes in a network -- if it does, the interfaces are valid and users can check whether additional eventually-stable properties are implied. Moreover, the CB-graph can then be used to determine fault tolerance properties of the network. We formalize our verification algorithm in the Lean theorem proving environment and prove its soundness. We evaluate the performance of \textsc{CB-Ver} on a range of benchmarks that demonstrate its ability to verify expressive properties in reasonable time. Finally, we demonstrate it is possible to automatically generate suitable interfaces by turning the problem around: Given a CB-graph, we use an off-the-shelf Constrained Horn Clause (CHC) solver to synthesize interfaces for every network component that together ensure the given correctness property.

CB-VER: A Stable Foundation for Modular Control Plane Verification

Abstract

Network operators are often interested in verifying \emph{eventually-stable properties} of network control planes: properties of control plane states that hold eventually, and hold forever thereafter, provided the operating environment remains unchanged. Examples include eventually-stable reachability, access control, or path length properties. In this work, we introduce \textsc{CB-Ver}, a new framework for verifying such properties, based on the key idea of a \emph{converges-before graph} (CB-graph for short). When a user provides interfaces for each network component, \textsc{CB-Ver} checks the necessary component-by-component requirements in parallel using an SMT solver. In addition, the tool automatically synthesizes a CB-graph and checks whether it connects all nodes in a network -- if it does, the interfaces are valid and users can check whether additional eventually-stable properties are implied. Moreover, the CB-graph can then be used to determine fault tolerance properties of the network. We formalize our verification algorithm in the Lean theorem proving environment and prove its soundness. We evaluate the performance of \textsc{CB-Ver} on a range of benchmarks that demonstrate its ability to verify expressive properties in reasonable time. Finally, we demonstrate it is possible to automatically generate suitable interfaces by turning the problem around: Given a CB-graph, we use an off-the-shelf Constrained Horn Clause (CHC) solver to synthesize interfaces for every network component that together ensure the given correctness property.

Paper Structure

This paper contains 27 sections, 13 theorems, 30 equations, 10 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. CB-Ver: Overview and Key Ideas
  3. Background: The control plane model
  4. Background: Modeling routing protocols in SMT theories
  5. Motivating Example
  6. Abstract Convergence and CB-graphs
  7. Network Model and Semantics
  8. Abstract Convergence: Semantic Definitions and Theorems
  9. From Theory to Modular Tool: CB-Ver
  10. CB-Ver Algorithm
  11. CB-graphs and Fault Tolerance
  12. Interactive Error Debugging
  13. Automated Synthesis of Abstract Interfaces
  14. Implementation and Evaluation
  15. Benchmarks and Setup
  16. ...and 12 more sections

Key Result

Theorem 1

If a CB-graph for $Q$ is connected, then all nodes $v$ in the network abstractly converge to $Q(v)$. $\blacktriangleleft$$\blacktriangleleft$

Figures (10)

  • Figure 1: Example network with devices A, B, C, D. A originates the route. Local preference is set to 300 on the B-E edge and to 100 elsewhere.
  • Figure 2: Synthesized CB-graphs for interfaces $I_1,Q_1$ and $I_2,Q_2$.
  • Figure 3: Summary: Verification Condition (VC) Formulas.
  • Figure 4: CB-graph of a cross-world network from the Batfish tutorial batfish-tutorials-failure. Houston (bordered in red) is a CB-root and directed arrows are CB-edges.
  • Figure 5: CHC system for the network interface synthesis problem, given the CB-graph. $\mathbb B=\{\mathrm{True},\mathrm{False}\}$ is the Boolean domain, variables $s_u,s_v,s_v'$ in CHC rules are universally quantified implicitly.
  • ...and 5 more figures

Theorems & Definitions (29)

  • Theorem 1: Connected CB-graph Theorem
  • Theorem 2: Correctness Theorem
  • Theorem 3: Fault tolerance theorem
  • Definition 1
  • Definition 2: Network instance
  • Definition 3: Asynchronous schedule
  • Definition 4: Network semantics
  • Definition 5
  • Theorem 4
  • Definition 6: Fairness
  • ...and 19 more