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

TL;DR

CB-Ver is a new framework for verifying eventually-stable properties of network control planes using CB-graphs, SMT solvers, and theorem proving, enabling modular and fault-tolerant analysis.

Contribution

Introduces CB-Ver, a novel modular verification framework for network control planes based on CB-graphs, with formal soundness proof and automated interface synthesis.

Findings

CB-Ver efficiently verifies expressive network properties.

The framework can automatically synthesize interfaces ensuring correctness.

Performance benchmarks show practical applicability for real networks.

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.