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

Abstract

Network operators are often interested in verifying 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. In this work, we introduce CB-VER, a new modular framework for verifying such properties, based on the key idea of a converges-before graph (CB-graph for short). Given user-provided specifications for each network component, CB-VER checks the necessary requirements in parallel using an SMT solver and automatically generates a CB-graph. Verification succeeds if all requirements are met and the generated CB-graph connects all nodes in a network. We formalize our verification algorithm in the Lean theorem prover and prove its soundness. Moreover, the generated CB-graph can be used to determine fault tolerance properties of the network. We also consider the inverted problem: Given a connected CB-graph, we can automatically synthesize suitable component specifications by formulating the problem as a Constrained Horn Clause (CHC) problem that ensures the given correctness property. We evaluate the performance of CB-VER and the synthesis tool (along with comparison to other tools) to demonstrate that they can successfully verify expressive properties on a range of benchmarks. Index Terms—Networks, control plane verification, modular verification, invariants, invariant synthesis.