随着网络技术的高速发展,分布式网络控制平面变得越来越复杂。为了满足不同业务流量的路由转发需求,控制平面运行着多种路由协议,路由协议的配置参数众多,十分灵活。不同厂商的设备配置语言不同,错误的配置可能造成网络中断等安全事故的发生,这使得配置和维护网络是一个具有挑战性且容易出错的过程。因此,为了保证网络的安全性和可用性,控制平面之上网络配置的验证面临着严峻的挑战。而现有的用于验证网络配置的工具存在验证速度太慢、系统资源消耗过大等问题。为了解决上述问题,本文的研究目标是:在校园网络等真实网络配置场景下,搭建一种轻量级的网络验证模型,并实现相应的网络安全性策略和可用性策略的验证方法,实现对网络的快速验证,同时减少验证过程中系统资源的消耗。本文的研究内容和贡献主要包括以下三个部分:首先,设计基于控制平面抽象表示的轻量级多层网络验证模型。控制平面抽象表示的验证模型是一组单层的有向图,该模型资源消耗较少,但缺少对一些关键路由协议属性的建模,应用场景有限。因此,为了减少验证过程中的资源消耗,本文在控制平面抽象表示的基础上,将其单层图模型扩展为多层图模型,解耦图模型的功能,多层网络验证模型可以对单层图模型中缺少的部分关键路由协议属性进行建模。从实验结果来看,本文网络验证模型相较于其他常用验证模型而言,随着网络设备数量的增加,模型构建时间缩短1-20倍不等,CPU占用时间缩小一半左右,物理内存占用减少10%-30%。其次,研究并提出了基于改进广度优先遍历的网络安全性策略验证方法。考虑到验证安全性策略过程中,需要检验网络中特定协议标签的配置是否按照一定顺序进行。因此,为了加快验证速度,本文根据相关图遍历算法,提出了基于改进广度优先遍历的网络安全性策略验证方法。从实验结果来看,随着网络设备数量的增加,相比较Minesweeper的验证方法而言本文方法验证速度提升至20倍,比Tiramisu的验证方法验证速度加快2倍,CPU峰值占比减少约16%。最后,研究基于整数线性规划的网络可用性策略验证方法。为了加快验证速度,本文在整数线性规划的基础上,对不同的可用性策略验证方法设置相关约束条件,减少与目标策略不相关的网络属性的建模。从实验结果来看,在小型网络规模下,该方法相较于其他可用性策略验证方法,减少了虚拟机内存回收次数,相比较Minesweeper的方法,随着网络规模的增大,验证速度逐步提升至18倍。