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.

翻译：网络运营商通常关注验证网络控制平面的\emph{最终稳定性质}：即在运行环境不变的前提下，控制平面状态最终成立且此后永远保持的性质。这类性质包括最终稳定的可达性、访问控制或路径长度等。本文提出\textsc{CB-Ver}框架，基于\emph{收敛前图}（简称CB图）的核心思想验证此类性质。当用户为每个网络组件提供接口时，\textsc{CB-Ver}利用SMT求解器并行检查各组件间的必要需求。此外，该工具自动合成CB图并验证其是否连接网络中所有节点——若连接成功，则接口有效，用户可进一步检验是否蕴含其他最终稳定性质。同时，CB图还可用于确定网络的容错特性。我们在Lean定理证明环境中形式化验证算法并证明其正确性。通过一系列基准测试评估\textsc{CB-Ver}性能，验证其能在合理时间内完成表达性强的性质验证。最后，我们展示反向实现的可能性：给定CB图，使用现成的约束子句求解器为每个网络组件合成接口，共同确保给定正确性的性质。