方星(1997-), 男, 硕士生, 主要研究领域为网络验证, 网络安全, 计算机网络
胡波(1981-), 男, 硕士, 高级工程师, 主要研究领域为网络安全, 网络验证
马超(1991-), 男, 工程师, 主要研究领域为网络风险评估, 网络验证
黄伟庆(1972-), 男, 博士, 正高级工程师, 博士生导师, CCF 高级会员, 主要研究领域为网络安全, 物联网安全, 云计算安全, 信号处理理论与技术, 电磁声光检测与防护
随着计算机网络规模和复杂度的日益增长, 网络管理人员难以保证网络意图得到了正确实现, 错误的网络配置将影响网络的安全性和可用性. 受到形式化方法在硬软件验证领域中成功应用的启发, 研究人员将形式化方法应用到网络中, 形成了一个新的研究领域, 即网络验证(network verification), 旨在使用严格的数学方法证明网络的正确性. 网络验证已经成为当下网络和安全领域的热点研究, 其研究成果也在实际网络中得到了成功应用. 从数据平面验证、控制平面验证和有状态网络验证3个研究方向, 对网络验证领域的已有研究成果进行了系统总结, 对研究热点内容与解决方法进行了分析, 旨在整理网络验证领域的发展脉络, 为本领域研究者提供系统性文献参考和未来工作展望.
With the increasing scale and complexity of computer networks, it is difficult for network administrators to ensure that the network intent has been correctly realized, and the incorrect network configuration will affect the security and availability of the network. Inspired by the successful application of formal methods in the field of hardware verification and software verification, researchers applied formal methods to networks, forming a new research field, namely network verification, which aims to use rigorous mathematical methods to prove the correctness of the network. Network verification has become a hot research topic in the field of network and security, and its research results have been successfully applied in actual networks. From the three research directions of data plane verification, control plane verification, and stateful network verification, this study systematically summarizes the existing research results in the field of network verification, and analyzes the research hotspots and related solutions, aiming to organize the field of network verification and provides systematic references and future work prospects for researchers in the field.
现代网络已经变得非常复杂和庞大, 运行着大量不同厂商与不同类型的网络设备, 并交互有数十种不同的网络协议. 随着诸如虚拟化、云计算、物联网等技术变得越来越普遍, 网络似乎变得更加复杂, 管理起来也变得更加困难, 从而变得非常容易出错. 软件定义网络(software-defined networking, SDN)[
在面对复杂且庞大的网络时, 网络管理人员主要依靠个人经验与理解进行管理, 被称作“复杂性大师”[
受到硬软件验证技术的启发, 2012年左右出现了一个新的研究领域, 即网络验证(network verification), 旨在使用严格的数学方法证明网络的正确性. 硬软件验证技术通过使用形式化方法, 能够在硬软件投入使用之前证明系统的正确性, 以避免意外错误的发生. 例如, AMD公司形式化验证了AMD K5处理器的浮点数除法运算的正确性[
网络验证领域代表研究
网络验证使用严格的数学方法, 能够基于网络的配置或转发状态推断出所有可能的网络行为, 然后将网络行为与意图进行比较, 验证网络意图是否得到了正确实现. 相比于同样基于形式化方法进行建模分析, 但关注于验证单个协议行为正确性(如不会出现死锁、活锁、溢出等错误状态)的协议验证(protocol verification)领域[
目前, 已经有学者发表了网络验证领域的综述性文章[
本文第1节介绍了网络验证领域中必要的背景知识; 第2–4节分别介绍了数据平面验证、控制平面验证、有状态网络验证3个研究方向的研究情况; 第5节介绍了网络验证相关领域的研究情况; 第6节对网络验证领域中的未来研究工作进行了展望; 最后对本文做出总结.
为了更好地阐述网络验证领域中的研究情况, 下面分别介绍网络和验证两部分的背景知识. 网络相关的背景知识主要有数据平面、控制平面、SDN、有状态网络, 有助于理解各个研究方向的划分与研究问题; 验证相关的背景知识主要为形式化方法, 有助于理解网络验证研究的验证方法.
如
传统网络与SDN的网络功能逻辑分层
在传统网络中, 控制平面分散在网络中的各个设备中, 与数据平面高度耦合, 通过分布式的控制过程计算路由信息. 然而, 这种分布式的架构管理起来非常困难, 部署业务时需要逐个配置网络设备, 且需要考虑复杂多样的网络协议和厂商配置语言, 非常容易出错. 为了更好地管理网络与网络业务创新, McKeown等人提出了OpenFlow方案[
在传统网络架构下, 网络管理人员主要通过部署中间件(middlebox)[
形式化方法(formal methods)是一种基于严格数学基础的技术, 用于对计算机硬软件系统规约、开发、验证[
形式化方法是网络验证领域的核心技术[
形式化验证步骤
形式化验证技术目前主要有模型检测[
形式化验证技术总结
验证技术 | 系统建模方法 | 属性建模方法 | 验证过程 | 优点 | 缺点 |
模型检测 | 有限状态机 | 时态逻辑公式 | 遍历状态空间判断公式是否得到满足 | 自动化的快速验证 | 状态爆炸问题 |
符号执行 | 程序 | 程序断言 | 遍历程序路径空间, 求解路径约束判断程序断言是否成立 | 使用少量输入完成高覆盖的测试 | 路径爆炸问题 |
定理证明 | 公式 | 公式 | 证明系统公式( |
无状态爆炸问题, 应用范围广 | 使用复杂且不提供反例 |
SAT/SMT
|
逻辑公式 | 逻辑公式 | 使用求解器求解表达系统( |
应用范围广 | 部分问题求解难度高 |
抽象解释 | 抽象域 | 抽象域 | 将抽象后的系统和属性作为新的验证对象, 进一步使用验证技术完成验证 | 计算效率高 | 损失分析精度 |
数据平面验证是网络验证领域中的第1个热点研究方向, 通过分析数据平面和网络拓扑信息, 验证数据包转发行为与网络意图的一致性. 其中, 数据平面主要是指转发表或流表, 此外还包括访问控制列表(access control lists, ACL)等决定数据包转发的信息. 目前, 数据平面验证主要验证数据包转发相关的网络属性, 如可达性、无转发循环、区域流量隔离. 其中, 可达性用于保证网络设备之间的正常通信, 例如设备A发送的数据包可以正常到达设备B; 无转发循环用于保证网络中不存在数据包转发循环; 区域流量隔离用于保证特定区域的网络设备不能相互通信, 例如办公区与公共区的网络设备不能相互访问. 需要指出的是, 网络属性与网络策略、网络意图一样, 用于表达期望达到的网络行为, 不同之处在于表达形式与表达粒度.
相比控制平面, 数据平面直接体现了数据包的转发行为, 有更好理解的语义. 因此, 数据平面验证相比控制平面验证更加容易实现, 不需要考虑控制平面中复杂的配置语言与协议交互过程. 不过, 由于数据平面验证分析的是数据平面快照信息, 且数据平面经常会发生变化(例如接收到新的外部路由通告、链路状态改变或正处于路由收敛过程), 数据平面验证需要实现实时验证, 通过持续采集与验证数据平面信息, 保证数据平面行为与策略之间的实时一致性.
由于传统网络和SDN的数据平面都是转发规则信息, 两种网络架构下的数据平面验证所解决的问题在本质上是相同的, 都是通过分析转发规则信息验证网络策略. 因此, 同一数据平面验证方法可以在两个网络架构中得到使用. 两个网络架构下的数据平面验证过程的主要区别是数据平面的获取过程与数据格式, 在传统网络中可以通过终端或SNMP协议获取转发表信息, 在SDN中则可以通过控制器获取流表信息. 虽然SDN并没有使得数据平面验证问题变得更简单, 但其可以更方便地获取数据平面信息.
本节根据研究主要解决的问题, 将已有研究分成了离线验证研究、实时验证研究、高扩展性验证研究、高表达性验证研究4个研究内容部分, 并结合时间顺序与验证技术对各个部分的研究进行了详细介绍. 其中, 扩展性是指研究工具处理大型网络验证任务的能力, 与验证速度和算法复杂度相关; 表达性是指工具的建模分析能力, 在数据平面验证中体现为数据平面行为的建模分析能力, 例如能够建模分析网络地址转换(network address translation, NAT)、访问控制列表等特殊的转发功能.
早期的数据平面验证研究, 开创性地使用不同形式化方法, 通过分析数据平面实现了网络属性的验证, 提供了数据平面验证的不同实现方案. 由于早期研究对验证速度要求较低, 主要使用离线验证的方法实现, 即不考虑数据平面的实时变化.
(1) 基于模型检测技术
Al-Shaer等人于2009年提出了ConfigChecker[
(2) 基于SAT求解器技术
Mai等人于2011年提出了Anteater[
(3) 基于符号执行技术
Kazemian等人于2012年提出了HSA[
(4) 离线验证工具总结
上述数据平面验证工具为该方向中早期的开创性研究, 分别使用模型检测、SAT求解技术、符号执行这3种形式化方法, 通过分析数据平面信息完成了可达性等网络属性的验证. ConfigChecker[
由于离线验证工具的验证速度普遍较慢, 难以及时地发现网络错误, 且无法处理数据平面的实时变化以保证验证结果的实时正确性. 为解决该挑战, 学术界陆续开展了实时验证的研究, 旨在开发出高效的验证算法, 能够在每次网络状态更新时实时地完成验证. 受益于集中式控制的网络架构, SDN可以方便地获取数据平面的更新信息, 且可以通过拦截违反验证属性规则的下发, 提前阻止错误的发生. 受到分布式网络架构的限制, 实时验证在传统网络中实现起来相对比较困难.
(1) 基于等价类方法
Khurshid等人于2013年提出了VeriFlow[
在VeriFlow被提出不久之后, Yang等人于同年提出了更加高效的实时验证工具Atomic Predicates Verifier (APV)[
(2) 基于增量计算方法
NetPlumber[
(3) 基于增量计算和等价类方法
受到APV[
虽然APV[
Horn等人于2017年提出了Delta-net[
Horn等人于2019年提出了等价类计算框架#PEC[
(4) 实时验证工具总结
VeriFlow[
尽管实时验证工具已经达到了很高的验证速度, 可以在数据平面变化后的短时间内完成验证. 但是, 这些实时验证工具主要关注于校园网等中小型网络的验证, 在面临着包含数千或数万台网络设备的大型网络时, 会因为超时或内存不足而不能完成验证. 因此, 需要开发出具有高扩展性的数据平面验证工具, 实现大型网络的快速验证. 其中, 高扩展性验证除了需要较高的验证速度, 还需要具有较低的算法复杂度.
(1) 基于分布式计算技术
Zeng等人于2014年提出了Libra[
(2) 基于模态逻辑的互模拟技术
Plotkin等人于2016年提出了一种网络变换方法[
(3) 基于网络结构特征
Jayaraman等人于2019年提出了RCDC[
(4) 高扩展性验证工具总结
上述研究通过高性能计算或简化验证任务, 实现了大型网络下的快速验证. Libra[
除了高扩展性, 数据平面验证工具还需要实现高表达性, 用于建模验证真实网络中复杂多样的网络功能, 例如数据包头部转换、数据包封装与解封装、组播数据包等.
(1) 基于逻辑编程语言Datalog
相较于实现实时验证, Lopes等人[
(2) 基于等价类方法
通过改进实时验证工具APV[
Zhang等人于2020年提出了APKeep[
(3) 基于模型检测技术
Jensen等人指出, 保证链路中断情况下的网络正确性是非常重要的, 但是已有数据平面验证工具往往无法完成链路中断情况的假设分析, 或因算法复杂度过高无法验证多条链路中断的假设情况. 此外, 由于MPLS网络支持可变化大小的数据包头部, 大多已有验证工具不能完成建模分析. 基于上述考虑, Jensen等人于2018年提出了P-Rex[
(4) 高表达性验证总结
NOD[
本节根据研究主要解决的问题, 将数据平面验证研究分成了离线验证、实时验证、高扩展性验证和高表达性验证4个研究内容部分, 并结合时间顺序和验证技术具体介绍了各个部分的研究内容. 离线验证是最早出现的数据平面验证研究, 创新性地使用不同的形式化方法, 通过分析数据平面实现了网络属性验证, 提供了实现数据平面验证的不同思路. 但是, 离线验证研究未考虑数据平面的实时变化, 不能保证验证结果的实时正确性. 实时验证研究使用等价类和增量计算技术, 通过只验证或建模受到数据平面变化影响的部分, 实现了数据平面实时验证. 高扩展性验证研究旨在实现大型网络下的快速验证, 使用了不同技术用于提升验证速度或优化算法复杂度. 高表达性验证研究旨在处理真实网络中复杂的网络功能, 以验证多种类型的网络. 需要指出的是, 部分的数据平面验证研究, 特别是前沿研究, 同时解决了多个研究部分的问题. 对于这些可以被划分到多个研究部分的研究, 本文根据其侧重解决的问题进行划分. 例如, APKeep[
下面对数据平面验证的实现和优化方法进行总结. 实现方面, 数据平面验证与形式化验证一样, 主要分为系统建模、属性建模、属性验证3个流程, 其建模与验证方法取决于使用的验证技术. 例如, 基于模型检测实现时使用状态机建模数据平面等信息, 然后遍历状态空间验证使用逻辑公式表示的网络属性; 基于图算法实现时使用图模型建模数据平面等信息, 然后使用深度优先搜索等图算法验证网络属性. 目前, 数据平面验证工具主要验证可达性以及相关网络属性, 且可达性验证大多基于Xie等人[
数据平面验证中可达性验证的主要实现思路
数据平面验证技术总结
工具 | 基于技术 | 扩展性 | 表达性 | 简要总结 |
ConfigChecker[ |
模型检测 | 低 | 中 | 首个正式提出的数据平面验证工具 |
Anteater[ |
SAT求解 | 低 | 中 | 首个在真实网络中发现错误的数据平面验证工具 |
HSA[ |
符号执行 | 低 | 中 | 使用基于函数的分析方法, 能够找到违反验证属性的全部反例 |
VeriFlow[ |
图算法 | 中 | 低 | 使用等价类方法划分网络, 只对受到数据平面变化影响的等价类建模验证 |
APV[ |
图算法 | 高 | 低 | 划分等价类后, 使用数字集合替代数据包集合进行计算, 有效提升了验证速度 |
NetPlumber[ |
符号执行 | 中 | 中 | 基于HSA[ |
APC[ |
图算法 | 高 | 低 | 基于APV[ |
ddNF[ |
- | - | - | 一种数据结构, 相比基于BDD计算等价类更加高效, 且可以增量计算等价类 |
Delta-net[ |
图算法 | 中 | 低 | 使用数字区间表示数据包集合, 优化了等价类计算过程, 但存在区间爆炸问题 |
#PEC[ |
- | - | - | 一种等价类计算方法, 基于ddNF[ |
Libra[ |
图算法 | 高 | 中 | 基于MapReduce计算框架, 根据子网将验证任务划分为多个独立的验证任务, 通过分布式计算实现了高效验证 |
Plotkin等人[ |
- | - | - | 一种网络变换方法, 基于网络结构对称性与数据平面行为等价性简化网络结构, 并保证变换前后网络中的属性验证结果相同 |
RCDC[ |
SMT求解 | 高 | 低 | 针对特定结构的数据中心网络, 将全局属性的验证任务简化成为局部属性的验证任务 |
NOD[ |
Datalog | 低 | 高 | 使用通用的Datalog语言有效建模了多种复杂的网络属性与网络功能, 但验证速度较慢 |
APT[ |
图算法 | 高 | 高 | 基于APV[ |
APKeep[ |
图算法 | 高 | 高 | 基于APT[ |
P-Rex[ |
模型检测 | 中 | 中 | 实现了多项式时间复杂度的任意链路失效情况的可达性验证, 但只能适用于MPLS网络 |
控制平面验证通过分析控制平面信息、网络拓扑与环境信息, 验证在这些信息结合生成的数据平面下, 所有的数据包转发行为与网络意图一致. 与数据平面验证一样, 控制平面验证可以验证可达性、无转发循环等数据包转发相关的网络属性. 除此之外, 控制平面验证可以通过控制输入的环境信息, 对网络环境作出假设, 从而完成假设网络环境下的网络属性验证, 保证网络属性在未来可能出现的网络情况中依然能够成立. 例如, 保证在任意
相比数据平面验证, 控制平面验证最具有吸引力的地方在于, 可以在网络配置部署之前完成验证, 提前阻止错误的发生. 此外, 控制平面验证通过直接分析配置文件, 可以在发现错误之后更加有效地定位到错误配置. 但是, 控制平面验证需要考虑不同厂商网络设备的实现差别(如不同格式的配置语言)以及复杂的协议交互过程. 此外, 控制平面在某些情况下存在多个收敛数据平面, 且其最终收敛到的数据平面是不确定的, 例如BGP Wedgies[
由于传统网络中和SDN的控制平面格式与表示含义都不相同, 两个网络架构下的控制平面验证所解决的验证问题并不相同. 传统网络中的控制平面验证通过分析分布在各处网络设备中的配置文件验证网络策略; SDN中的控制平面验证则通过分析控制器或应用中的程序验证网络策略, 验证方法与软件程序验证较为相似. 因此, 两种网络架构下的控制平面验证方法的差别较大. 由于传统网络目前仍然占据主要地位, 本文只介绍传统网络中的控制平面验证技术.
本节根据研究主要解决的问题, 将控制平面验证方向中的已有研究分成了开创性研究、高扩展性验证研究、高表达性验证研究3个研究部分, 并结合时间顺序和验证技术对各个部分的验证技术进行了详细介绍. 其中, 扩展性是指研究工具处理大型网络验证任务的能力, 与验证速度和算法复杂度相关; 表达性是指工具的建模分析能力, 在控制平面验证中体现为控制平面行为的建模分析能力, 例如能够建模分析所有网络协议、处理不同厂商的控制平面实现差异、分析所有可能收敛的数据平面状态等.
早期的控制平面验证研究, 创新性地使用不同技术, 通过分析控制平面实现了网络属性的验证, 提供了控制平面验证的不同实现方案.
(1) 基于逻辑编程语言Datalog
Fogel等人于2015年提出了Batfish[
(2) 基于图算法
Gember-Jacobson等人于2016年提出了ARC[
(3) 基于BDD
Fayaz等人于2016年提出了ERA[
(4) 开创性研究总结
上述工具为控制平面验证方向中开创性研究, 通过模拟数据平面或直接分析控制平面实现了网络属性验证. Batfish[
与数据平面验证一样, 控制平面验证面临着验证大型网络的挑战. 为完成包含上千甚至上万台网络设备的大型网络下的验证任务, 陆续出现了高扩展性的控制平面验证研究, 致力于实现高验证速度和低算法复杂度.
(1) 基于控制平面等价性的网络压缩
Beckett等人于2018年提出了Bonsai[
由于Bonsai[
(2) 基于抽象解释
Beckett等人于2018年提出了ShapeShifter[
(3) 基于网络结构特征
Lopes等人于2019年提出了FastPlane[
(4) 基于模型检测
在控制平面验证工具Plankton[
(5) 基于增量计算
Zhang等人于2020年提出了控制平面增量验证工具RealConfig[
Li等人于2020年提出了NUV[
(6) 高扩展性验证研究总结
上述研究基于不同技术实现了较高的扩展性. Bonsai[
控制平面验证除了需要较高的扩展性以处理大型网络的验证任务, 还需要较高的表达性以处理实际的复杂网络情况. 其中, 控制平面验证的表达性与控制平面和环境信息的建模能力相关. 控制平面信息是指由配置文件实现的各种网络协议, 如BGP、OSPF、RIP等. 控制平面建模能力越高, 表示越能准确建模越多的网络协议行为, 越能实现准确且覆盖范围高的验证. 由于不同厂商的网络设备在实现相同的网络协议时, 其配置语言甚至实现形式都各不相同, 需要考虑不同厂商设备的这种实现差异. 此外, 控制平面可能存在多个收敛数据平面, 且在收敛过程中会产生多个数据平面过渡状态, 需要对这些收敛和过渡数据平面情况准确建模. 环境信息是指链路状态、外部路由通告等影响数据平面生成结果的网络信息. 环境信息建模能力越高, 表示越多的网络情况能够得到分析, 例如可以保证任意
(1) 基于模型检测
Prabhu等人于2017年提出了Plankton[
(2) 基于SMT求解器技术
Beckett等人于2017年提出了Minesweeper[
Ye等人于2020年提出了Hoyan[
(3) 基于图算法
Abhashkumar等人于2020年提出了Tiramisu[
(4) 高表达性验证研究总结
上述研究基于不同技术, 实现了不同方面的表达性提升. Plankton[
本节根据研究主要解决的问题, 将控制平面验证研究分成了开创性研究、高扩展性验证和高表达性验证3个研究部分, 并结合时间顺序和验证技术具体介绍了各个部分的已有研究. 开创性研究是最早出现的控制平面验证研究, 提供了控制平面验证的不同实现方案. 高扩展性研究旨在实现大型网络下的快速验证, 使用了不同技术用于提升验证速度或优化算法复杂度. 高表达性验证旨在实现准确且大范围地建模控制平面与环境信息, 以应对实际网络中复杂的网络情况. 与数据平面验证研究的划分方法一致, 本章根据研究侧重解决的问题以及创新点对控制平面验证研究进行划分. 例如, Hoyan[
下面对控制平面验证的实现和优化方法进行总结. 实现方面, 如
控制平面验证主要实现思路
控制平面验证技术总结
工具 | 实现思路 | 基于技术 | 扩展性 | 表达性 | 简要总结 |
Batfish[ |
模拟 | Datalog | 低 | 高 | 完整模拟生成数据平面, 然后使用数据平面验证工具完成验证 |
ARC[ |
图算法 | 图算法 | 高 | 低 | 使用定制化的图算法直接分析控制平面验证网络属性, 实现了很高的验证速度, 但表达性较低 |
ERA[ |
模拟 | BDD | 中 | 中 | 基于路径模拟控制平面协议行为, 然后根据生成信息验证网络属性, 兼顾了扩展性和表达性 |
Bonsai[ |
- | 稳定路径问题路由代数理论 | - | - | 一种网络变换方法, 基于网络结构对称性与控制平面行为等价性简化网络结构, 并保证验证结果在变换前后的网络中相同 |
Origami[ |
- | 稳定路径问题路由代数理论 | - | - | 基于Bonsai进行改进, 结合网络抽象过程与验证过程, 根据验证结果调整网络抽象, 使抽象后的网络能够提供足够的链路用于链路环境分析 |
ShapeShifter[ |
模拟 | 抽象解释 | 高 | 低 | 对控制平面协议行为进行抽象, 牺牲了一定的验证精确度, 实现了接近线性的时间复杂度 |
FastPlane[ |
模拟 | 图算法 | 高 | 低 | 通过优化路由选择、传播等协议行为, 实现了数据平面的快速收敛, 但只适用于具有单调特征的BGP网络 |
Plankton[ |
模拟 | 模型检测 | 高 | 高 | 使用相对SMT求解技术更高效的模型检测技术, 并通过等价类等技术进行优化, 实现了高扩展性 |
RealConfig[ |
模拟 | DDlog | 高 | 高 | 使用DDlog增量生成数据平面以应对控制平面的变化情况, 使用APKeep[ |
NUV[ |
- | 路由代数理论 | - | - | 可以找到受控制平面更新影响的网络策略, 帮助其他工具实现增量验证 |
Plankton[ |
模拟 | 模型检测 | 中 | 高 | 详尽地建模了所有可能的数据平面情况, 能够验证控制平面所有可能生成的数据平面状态 |
Minesweeper[ |
SMT求解 | SMT求解 | 中 | 高 | 可以建模所有可能生成的数据平面情况, 但使用SMT公式建模存在一定的扩展性问题 |
Tiramisu[ |
模拟/
|
图算法 | 高 | 高 | 基于ARC[ |
Hoyan[ |
模拟 | SMT求解 | 高 | 高 | 结合了模拟技术建模速度快和SMT求解技术可有效处理不确定性情况的优点, 且可以准确建模不同厂商的控制平面协议行为 |
上述介绍的数据平面验证与控制平面验证研究已经实现了较高的表达性与扩展性, 但是这些研究都针对验证无状态网络, 没有考虑网络中的中间件, 或直接将中间件当作无状态设备处理, 不能正确完整地验证中间件. 调查显示, 中间件在网络中的数量已经与路由器的数量相当[
目前, 有状态网络验证属于起步阶段, 且主要采用数据平面验证方法实现. 由于已有的有状态网络验证研究数量较少, 本节不对有状态网络验证研究进行划分, 直接根据研究的出现时间进行顺序介绍.
目前的有状态网络验证研究仍处于开创性阶段, 使用不同的技术实现了有状态网络下的网络属性验证.
(1) 基于符号执行
Stoenescu等人于2013年最早开始了有状态网络验证研究, 基于符号执行技术提出了SymNet[
(2) 基于SMT求解技术
Panda等人于2015年提出了中间件建模和有状态网络验证的思路[
(3) 基于抽象解释技术
Velner等人于2016年对有状态网络中的区域流量隔离属性验证进行了复杂度分析, 并提出了一种原型验证工具[
基于Velner等人的复杂度分析与抽象方法[
(4) 基于符号模型检测技术
Yuan等人于2020年提出了NetSMC[
(5) 开创性研究总结
上述研究分别基于符号执行、SMT求解、抽象解释和符号模型检测技术, 实现了有状态网络验证. SymNet[
由于有状态网络验证处于起步阶段, 研究数量较少, 本节未对有状态网络验证研究进行分类, 直接按照研究的出现时间进行顺序介绍. 目前, 有状态网络验证主要解决了实现问题, 提出了有状态网络验证的不同实现方案, 但是其扩展性与表达性仍处于较低水平, 不能完成大型网络下的快速验证, 或大范围且准确地建模各种网络功能. 其中, 已有研究主要基于数据平面验证技术实现, 即通过分析数据包的转发信息验证可达性等网络属性. 与无状态网络中的数据平面验证的区别在于, 有状态网络验证还需要考虑影响数据包转发行为的中间件状态信息. 由于中间件的状态信息与中间件先前接收到的数据包相关, 且数据包的接收数量与接收顺序不受限制, 建模有状态网络非常困难, 区域流量隔离等基本的验证问题在这种情况下也变得不可解. 为实现验证问题的可判定, 不能完整地建模有状态网络, 都需要进行一定的抽象, 如假定中间件状态有限、网络设备以任意顺序处理数据包、网络中只存在一个数据包等. 这种抽象方法带来的问题是, 不能完整地建模所有网络行为, 或不能保证验证结果的准确性.
有状态网络验证技术总结
工具 | 基于技术 | 准确性 | 扩展性 | 表达性 | 简要总结 |
SymNet[ |
符号执行 | 可靠 | 低 | 低 | 通过在数据包头部添加状态信息建模有状态中间件, 提出了建模语言SEFL以加快符号执行过程 |
VMN[ |
SMT求解 | 准确 | 低 | 中 | 提出了一种中间件抽象建模方法, 使用网络压缩技术提高了扩展性 |
Alpernas等人[ |
抽象解释 | 可靠 | 中 | 中 | 通过抽象数据包处理顺序与中间件状态, 实现了较低复杂度的验证 |
NetSMC[ |
模型检测 | 可靠 | 中 | 中 | 将网络抽象为单个数据包转发的模型, 使用定制的符号模型检测算法实现了较高的验证速度 |
(1) SDN控制平面验证
本文只介绍了传统网络中的控制平面验证研究. 对于SDN控制平面验证, 可以分为SDN程序验证和控制器验证两种实现方案[
(2) 网络测试
网络验证可以通过分析数据平面或控制平面以验证网络的正确性, 但其仍存在一定的局限性, 难以发现网络中存在的全部错误, 例如路由器不正确按照转发表转发数据包, 网络链路拥塞等. 网络测试是对网络验证的补充, 能够发现网络设备硬件错误等实现错误. 但是, 网络测试并不能证明网络中不存在错误[
(3) 网络配置综合
由于不同的网络管理人员对网络运行有着不同的理解, 且网络意图和配置实现之间存在巨大的语义鸿沟, 非常容易出现配置错误. 网络配置综合旨在根据网络意图自动生成正确的网络配置. 网络配置综合与软件验证领域中的程序综合(program synthesis)的实现思想比较相似, 都试图使用形式化方法自动生成符合规约的配置或代码. 其中, 程序综合是指使用指定的编程语言自动生成符合程序规约的技术[
(4) 网络仿真
网络仿真技术使用虚拟机技术构建出虚拟环境, 通过运行与真实网络相同的网络设备固件与配置, 生成对应的转发表信息进行验证. 网络仿真通过仿真实际网络运行情况, 能够发现网络验证所不能发现的设备实现错误, 可以被看作是网络验证的增强版本[
(5) 基于意图的网络(IBN)
IBN是一种新兴的网络范式, 可以自动地实现用户意图, 并通过持续监控网络状态信息, 判断用户意图是否得到正确实现[
(1) 定量属性验证
目前, 网络验证关注的网络属性主要为可达性、无转发循环、区域流量隔离等布尔值属性. 尽管其可以对网络安全意图提供保证, 但其无法对网络性能意图提供保证, 如延迟, 丢包率等. 因此, 需要实现对表达性能意图的定量属性的验证. 目前, 已有的定量属性验证研究有SLA-Verifier[
(2) 错误定位与修复
已有的网络验证研究在发现违反网络属性的错误之后, 依然需要根据输出信息手动定位错误配置并完成修复. 因此, 需要自动化的错误定位与修复功能, 以保证在发现网络错误之后能够及时修复. 目前, 已经有相关研究实现了数据平面验证或控制平面验证后的错误定位[
(3) 更方便地使用网络验证工具
网络验证研究已经取得了显著的成果, 可以为大型复杂的网络提供安全性和可用性方面的保证. 然而, 由于网络验证工具大多使用定制化的语言表达网络意图, 且缺少容易操作的图形界面, 使用起来比较困难. 因此, 下一步的目标是提高网络验证工具的易用性, 使其能够得到广泛应用, 像Ping和Traceroute等工具一样流行[
(4) 检测网络验证工具的正确性
与其他软件工具一样, 网络验证工具也可能存在漏洞, 导致输出错误的验证结果. 因此, 在网络验证工具投入运行之前, 有必要进行正确性检测. 最近, Birkner等人提出了Metha[
网络验证是近年来的热点研究领域, 学术界和工业界对该领域做出了大量的研究, 并将部分的工具进行了实际应用以保证网络的安全可靠性. 本文分为数据平面验证、控制平面验证和有状态网络验证3个研究方向, 对网络验证领域中的已有研究做出了综述. 由于目前传统网络架构仍占据主流地位, 本文只对传统网络中的控制平面验证研究进行了介绍. 无状态数据平面验证作为网络验证领域最早的研究工作, 目前已经得到了很好的解决, 可以在大型网络中完成实时验证; 控制平面验证也取得了显著的进展, 可以在运行有多种协议的大型网络中完成快速验证; 有状态网络验证目前研究相对较少, 仍处于起步阶段. 网络验证领域的研究成果及时地满足了目前日益复杂庞大的网络的可用性和安全性需求, 且仍有非常大的发展空间. 本文希望通过提供网络验证领域发展以来的热点研究内容与解决方法, 帮助读者了解网络领域研究的发展脉络, 以思考该领域现有的研究技术并找到创新的研究思路.
http://www.youtube.com/watch?v=c9-K5O_qYgA]]>
https://www.youtube.com/watch?v=Ho239zpKMwQ]]>
https://www.intentionet.com/blog/three-ways-to-break-a-network-and-one-to-save-it/]]>
https://www.zdnet.com/article/azure-global-outage-our-dns-update-mangled-domain-records-says-microsoft/]]>
https://www.futuriom.com/articles/news/centurylink-peers-blame-wobbly-router-for-massive-outage/2020/09]]>
https://opengear.com/white-paper/measuring-the-true-cost-of-network-outages]]>
Russinoff DM. A mechanically checked proof of correctness of the AMD K5 floating point square root microcode. Formal Methods in System Design, 1999, 14(1): 75–125. [doi: 10.1023/A:1008669628911]
Brat G, Drusinsky D, Giannakopoulou D, Goldberg A, Havelund K, Lowry M, Pasareanu C, Venet A, Visser W, Washington R. Experimental evaluation of verification and validation tools on martian rover software. Formal Methods in System Design, 2004, 25(2): 167–198. [doi: 10.1023/B:FORM.0000040027.28662.a4]
Li YH, Wang ZL, Yin X, Shi XG, Wu JP, Ye FD, Yao JY, Zhang H. Assisting reachability verification of network configurations updates with NUV. Computer Networks, 2020, 177: 107326. [doi: 10.1016/j.comnet.2020.107326]
et al. Accuracy, scalability, coverage: A practical configuration verifier on a global WAN. In: Proc. of the Annual Conf. of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication. New York: Association for Computing Machinery, 2020. 599–614.]]>
https://netverify.fun/2-current-state-of-research/]]>
Yang HK, Lam SS. Scalable verification of networks with packet transformers using atomic predicates. IEEE/ACM Transactions on Networking, 2017, 25(5): 2900–2915. [doi: 10.1109/TNET.2017.2720172]
et al. Validating datacenters at scale. In: Proc. of the ACM Special Interest Group on Data Communication. Beijing: Association for Computing Machinery, 2019. 200–213.]]>
Beckett R, Gupta A, Mahajan R, Walker D. Abstract interpretation of distributed network control planes. Proceedings of the ACM on Programming Languages, 2020, 4(POPL): 42. [doi: 10.1145/3371110]
https://www.intentionet.com/]]>
https://forwardnetworks.com/]]>
https://apstra.com/]]>
https://www.networkcomputing.com/networking/intent-based-verification-leading-new-wave-network-automation]]>
https://www.cisco.com/c/en/us/solutions/intent-based-networking.html]]>
https://www.juniper.net/us/en/research-topics/what-is-intent-based-networking.html]]>
https://carrier.huawei.com/en/adn]]>
Qadir J, Hasan O. Applying formal methods to networking: Theory, techniques, and applications. IEEE Communications Surveys & Tutorials, 2015, 17(1): 256–291. [doi: 10.1109/COMST.2014.2345792]
Li YH, Yin X, Wang ZL, Yao JY, Shi XG, Wu JP, Zhang H, Wang Q. A survey on network verification and testing with formal methods: Approaches and challenges. IEEE Communications Surveys & Tutorials, 2019, 21(1): 940–969. [doi: 10.1109/COMST.2018.2868050]
Zhang XL, Wang C, Li Q, Wu JP. Toward comprehensive network verification: Practices, challenges and beyond. IEEE Network, 2020, 34(1): 108–115. [doi: 10.1109/MNET.001.1800330]
Kreutz D, Ramos FMV, Veríssimo PE, Rothenberg CE, Azodolmolky S, Uhlig S. Software-defined networking: A comprehensive survey. Proceedings of the IEEE, 2015, 103(1): 14–76. [doi: 10.1109/JPROC.2014.2371999]
https://www2.eecs.berkeley.edu/Colloquium/Archives/15-16/Fall2015/varghese.shtml]]>
Narain S, Levin G, Malik S, Kaul V. Declarative infrastructure configuration synthesis and debugging. Journal of Network and Systems Management, 2008, 16(3): 235–258. [doi: 10.1007/s10922-008-9108-y]
http://www.jos.org.cn/1000-9825/6088.htm]]>
http://www.jos.org.cn/1000-9825/6088.htm]]>
McKeown N, Anderson T, Balakrishnan H, Parulkar G, Peterson L, Rexford J, Shenker S, Turner J. OpenFlow: Enabling innovation in campus networks. ACM SIGCOMM Computer Communication Review, 2008, 38(2): 69–74. [doi: 10.1145/1355734.1355746]
https://www.youtube.com/watch?app=desktop&v=WabdXYzCAOU]]>
Fonseca PC, Mota ES. A survey on fault management in software-defined networks. IEEE Communications Surveys & Tutorials, 2017, 19(4): 2284–2321. [doi: 10.1109/COMST.2017.2719862]
Yu YB, Li X, Leng X, Song LB, Bu K, Chen Y, Yang JF, Zhang L, Cheng K, Xiao X. Fault management in software-defined networking: A survey. IEEE Communications Surveys & Tutorials, 2019, 21(1): 349–392. [doi: 10.1109/COMST.2018.2868922]
https://rfc-editor.org/rfc/rfc3234.txt]]>
http://www.jos.org.cn/1000-9825/5652.htm]]>
http://www.jos.org.cn/1000-9825/5652.htm]]>
Wing JM. A specifier's introduction to formal methods. Computer, 1990, 23(9): 8–22. [doi: 10.1109/2.58215]
Hall A. Seven myths of formal methods. IEEE Software, 1990, 7(5): 11–19. [doi: 10.1109/52.57887]
Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 1986, 8(2): 244–263. [doi: 10.1145/5397.5399]
King JC. Symbolic execution and program testing. Communications of the ACM, 1976, 19(7): 385–394. [doi: 10.1145/360248.360252]
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic model checking: 1020 States and beyond. Information and Computation, 1992, 98(2): 142–170. [doi: 10.1016/0890-5401(92)90017-A]
Clarke E, Biere A, Raimi R, Zhu YS. Bounded model checking using satisfiability solving. Formal Methods in System Design, 2001, 19(1): 7–34. [doi: 10.1023/A:1011276507260]
De Moura L, Bjørner N. Satisfiability modulo theories: Introduction and applications. Communications of the ACM, 2011, 54(9): 69–77. [doi: 10.1145/1995376.1995394]
https://www.microsoft.com/en-us/research/publication/network-verification-in-the-light-of-program-verification/]]>
https://rfc-editor.org/rfc/rfc4264.txt]]>
Parr TJ, Quong RW. ANTLR: A predicated-
https://github.com/batfish/batfish]]>
Griffin TG, Shepherd FB, Wilfong G. The stable paths problem and interdomain routing. IEEE/ACM Transactions on Networking, 2002, 10(2): 232–243. [doi: 10.1109/90.993304]
https://github.com/vmware/differential-datalog]]>
Li YH, Wang ZL, Yao JY, Yin X, Shi XG, Wu JP, Zhang H. MSAID: Automated detection of interference in multiple SDN applications. Computer Networks, 2019, 153: 49–62. [doi: 10.1016/j.comnet.2019.01.042]
et al. Troubleshooting blackbox SDN control software with minimal causal sequences. In: Proc. of the 2014 ACM Conf. on SIGCOMM. Chicago: Association for Computing Machinery, 2014. 395–406.]]>
Singh A, Aujla GS, Bali RS. Intent-based network for data dissemination in software-defined vehicular edge computing. IEEE Transactions on Intelligent Transportation Systems, 2021, 22(8): 5310–5318. [doi: 10.1109/TITS.2020.3002349]
https://netverify.fun/network-verification-2-0/]]>