Lec 12 网络验证（Network Verification）
阅读资料
- R. Beckett et al., A General Approach to Network Configuration Verification (Minesweeper), SIGCOMM 2017
- (Optional) Blog posts
Topics：Reachability、Verification、Network Correctness。核心问题：网络的行为由各路由器上手写的配置决定，配置 bug 是大规模断网的常见原因；能否在部署前用形式化方法证明「网络一定满足某些性质」（如 A 能到 B、没有环路、即使坏一条链路也不黑洞）？
总览
- 为什么要做网络验证（配置 bug → 断网）
- 数据面验证 vs 控制面验证
- Minesweeper：把控制面 + 数据面编码成一个 SMT 公式
- 能验证哪些性质、如何建模故障
- 取舍与意义
- 论文重点图
一、为什么要验证
路由器的转发行为不是直接写的，而是从一堆配置（BGP/OSPF/静态路由、ACL、路由再分发、route-map…）经控制协议收敛后算出来的。配置之间相互作用极其微妙，人很难手推。
现实痛点
大型网络宕机事故里，相当一部分源于配置错误：一条 route-map 写错、再分发造成环路、某条链路一坏就黑洞。这些在「正常状态」下看不出来，往往在故障叠加时爆发。验证的目标：在所有可能的状态（含故障）下证明性质成立，而不是测几条 ping。
大型网络宕机事故里，相当一部分源于配置错误：一条 route-map 写错、再分发造成环路、某条链路一坏就黑洞。这些在「正常状态」下看不出来，往往在故障叠加时爆发。验证的目标：在所有可能的状态（含故障）下证明性质成立，而不是测几条 ping。
二、两类验证
定义 · 数据面验证 vs 控制面验证
数据面验证（如 Veriflow、HSA）：拿到当前已经算好的转发表，检查这一份快照下的可达性/环路。优点快；缺点只看「此刻」，看不到「配置在别的故障/收敛下会变成什么」。
控制面验证（Minesweeper 属此类）：直接分析配置本身，推理「在所有可能的环境（故障、外部路由通告）下，协议会收敛出怎样的转发表，性质是否始终成立」。
数据面验证（如 Veriflow、HSA）：拿到当前已经算好的转发表，检查这一份快照下的可达性/环路。优点快；缺点只看「此刻」，看不到「配置在别的故障/收敛下会变成什么」。
控制面验证（Minesweeper 属此类）：直接分析配置本身，推理「在所有可能的环境（故障、外部路由通告）下，协议会收敛出怎样的转发表，性质是否始终成立」。
三、Minesweeper 的核心思想
把「网络在所有可能输入下会稳定到什么转发状态」整个编码成一个逻辑公式，交给 SMT 求解器找反例。
定义 · 把稳定状态编码为约束（graph-based SMT encoding）
为每条路由通告、每个路由器的选路结果、每条链路状态等引入符号变量；把各协议的选路与收敛规则（如 BGP 选 local-pref/AS-path 最优、OSPF 选最短路、再分发、ACL 过滤）写成对这些变量的约束。这组约束的每一个解，恰好对应网络的一个合法稳定转发状态（stable state）。
为每条路由通告、每个路由器的选路结果、每条链路状态等引入符号变量；把各协议的选路与收敛规则（如 BGP 选 local-pref/AS-path 最优、OSPF 选最短路、再分发、ACL 过滤）写成对这些变量的约束。这组约束的每一个解，恰好对应网络的一个合法稳定转发状态（stable state）。
验证一条性质（如「A 一定能到 B」）的方法：把性质的否定加进约束，问 SMT「存在一个稳定状态使性质被违反吗？」
- UNSAT（无解） → 不存在反例 → 性质在所有状态下都成立 ✓
- SAT（有解） → 求解器给出的解就是一个具体反例（哪条链路坏了、哪条通告导致 A 到不了 B），可直接拿去调试。
推论 · 为什么这套「一个大公式」很通用
不同协议（BGP/OSPF/静态/再分发）只是不同的约束片段，都能塞进同一个公式；不同性质（可达、无环、无黑洞、无路由泄露、两路由器策略等价、负载均衡一致性）只是不同的「否定查询」。所以一套框架覆盖多协议 × 多性质，这正是标题「A General Approach」的含义——对比之前一个工具只查一种协议/一种性质。
不同协议（BGP/OSPF/静态/再分发）只是不同的约束片段，都能塞进同一个公式；不同性质（可达、无环、无黑洞、无路由泄露、两路由器策略等价、负载均衡一致性）只是不同的「否定查询」。所以一套框架覆盖多协议 × 多性质，这正是标题「A General Approach」的含义——对比之前一个工具只查一种协议/一种性质。
四、能验证哪些性质 & 故障建模
可表达的性质（举例）：
- Reachability / isolation：A 能/不能到 B；
- 无转发环路、无黑洞；
- 路由策略等价：两台路由器（或改配置前后）行为一致；
- 多路径一致 / 无路由泄露 / waypointing（流量必经某中间盒）。
定义 · 用符号故障变量覆盖「所有故障」
给每条链路/节点配一个布尔失效变量，并加约束「失效数 ≤ k」。于是 SMT 会在所有「最多坏 k 个组件」的组合里搜反例——无需逐一枚举故障，一次求解覆盖指数级的故障场景。这是控制面验证相对数据面验证的最大威力。
给每条链路/节点配一个布尔失效变量，并加约束「失效数 ≤ k」。于是 SMT 会在所有「最多坏 k 个组件」的组合里搜反例——无需逐一枚举故障，一次求解覆盖指数级的故障场景。这是控制面验证相对数据面验证的最大威力。
五、取舍与意义
- 代价：把收敛规则编码成 SMT 约束、再由求解器搜索，计算量大；规模化（大网络、复杂策略）是难点，论文用图结构编码 + 各种优化来压缩搜索空间。
- 价值：把「网络对不对」从「上线后 ping 一下、出事再查」变成部署前的数学证明，且能给出可复现的反例；它把形式化方法（SMT）成功带进了网络运维。
六、论文重点图
论文部分只记最重点的内容。
- 总体流程图：配置（多路由器、多协议）→ 编译成符号化的稳定状态约束 + 性质的否定 → SMT 求解器 → UNSAT（性质成立）/ SAT（给出违例的具体故障+路由场景）。
- 编码示意：网络拓扑图上，每条边/每个路由决策点挂着符号变量与约束；一个满足所有约束的赋值 = 一个真实可能的转发状态。
本讲小结
配置 bug 是断网主因，而它在正常态下隐形、故障叠加时爆发。Minesweeper 做控制面验证：把多协议的选路/收敛规则与链路故障编码成一个 SMT 公式，其解对应所有可能的稳定转发状态；把性质取反交给求解器——UNSAT 即证明性质恒成立，SAT 则直接给出反例。一套框架覆盖多协议 × 多性质 × 多故障，是「通用网络配置验证」的代表。