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**新框架，其核心思想为**收敛前图**（简称CB-graph）。当用户为每个网络组件提供接口时，CB-Ver借助SMT求解器并行检查各组件间必要条件。此外，该工具自动合成CB-graph并验证其是否连接网络中所有节点——若成功连接，则接口有效，用户可进一步验证其他蕴含的最终稳定性质。同时，CB-graph还可用于判定网络的容错属性。我们在Lean定理证明环境中形式化验证算法并证明其可靠性。通过多组基准测试评估CB-Ver性能，证明其能在合理时间内验证表达力丰富的性质。最后，我们论证可通过问题逆向转换自动生成合适接口：给定CB-graph，使用现成的约束Horn子句（CHC）求解器为每个网络组件合成接口，共同确保给定正确性属性。