近十年来,云计算经历了其诞生、发展与加速爆发。在我国,以阿里云、华为云、腾讯云为代表的云计算平台已然成为新型公共基础设施,渗入经济发展与社会生活的方方面面,在潜移默化中改变着每个人的日常生活。作为连接云与云、云与用户的桥梁,网络在云计算中发挥着至关重要且无可替代的作用,保障网络的稳定可靠,是维持云服务平稳运行的重中之重。然而,近期公开的一系列故障报告指出,网络故障是导致云服务中断的罪魁祸首之一,各大云服务提供商纷纷采取积极措施,尽一切努力遏制网络故障为云服务带来的稳定性风险。大型云服务提供商通常运营着遍布全球的私有广域网,因此,如何在业务规模加速扩张的同时保障其私有网络的安全可靠,日益成为各大云服务提供商不得不面对的重要课题。作为提升大型网络稳定性的重要一环,网络验证可为云服务稳定性的提升做出至关重要的贡献。与网络监控及网络测试等传统手段不同,网络验证利用形式化方法对网络进行精确建模,基于严谨的逻辑推理确保网络行为的严格正确性,与传统手段形成了良好的互补关系,三者间相互不可替代。本文将从国内某头部云服务提供商在其私有广域网运营期间遇到的实际问题出发,对云网络数据平面的可靠性验证系统展开研究,并对验证系统的自我校验机制进行探索。具体研究内容可以分为如下三部分:1)数据平面配置的验证与自动生成ACL规则是数据平面配置的典型代表。对云服务提供商而言,广域网ACL在保障网络的连通性、安全性、可靠性等方面起到了重要的作用;然而,其日益增长的复杂度也为运营人员带来了全新的挑战。广域网ACL变更频繁且容易出错,一旦出错将直接导致服务中断或为网络埋下隐患,从而对云服务的稳定性产生严重威胁。为了解决该问题,本文设计并实现了一套面向广域网ACL的自动化变更系统,运营人员只需要提供变更意图,系统即可自动且高效的生成可靠的变更方案。该系统已在工业界落地,并日常用于ACL变更管理。落地两年以来,其在提升运营人员工作效率的同时,多次检测出ACL变更风险,为广域网稳定性提供了有力的保障。2)数据平面配置与程序的联合验证为了让终端用户能够以低廉的成本享受高速网络服务,云服务提供商运营着大量的边缘网络节点,并利用可编程交换机进一步降低运营成本;然而,可编程交换机的部署也为边缘网络带来了额外的稳定性风险。与传统数据平面不同,可编程数据平面的数据包处理逻辑可以通过专用语言进行编程。随着网络功能集成程度的逐渐提升,交换机可靠性面临着愈加重大的挑战,为了保证其数据平面行为在逻辑上是符合预期的,本文设计并实现了一套面向可编程网络的形式化验证系统,从而对数据平面的配置与程序进行联合验证。对于绝大多数验证任务而言,其可在数分钟内给出验证结果,并能对程序缺陷给出准确定位。该系统已在工业界落地半年,为可编程交换机检测出多个隐蔽的程序缺陷,从而为边缘网络的稳定性提供了有力的保障。3)数据平面验证系统的自我校验在数据平面验证系统的实现中,其自身存在的错误会使验证系统发生误报与漏报。其中,验证系统的漏报往极为隐蔽:当验证预期被违背而验证系统没有发现时,运营人员与开发人员也同样无从发现。这就为网络稳定性埋下了隐患。为此,本文设计并实现了面向网络验证系统的自我校验机制,并将其用于ACL变更系统与可编程网络验证系统的日常校验之中。实验表明,该机制不仅可以发现验证系统的误报,也可以发现更为隐蔽的漏报,从而有效提升了验证系统自身的可靠性。