Fast Control Plane Analysis Using an Abstract Representation
背景
- state-of-art verifiers 【Batfish】 are either too slow or impractical to use for proactive control plane behavior verification under arbitrary link failures
- 理论：proactive analysis tasks often require computing properties of paths, not the paths themselves
- 实际：many enterprise and data center networks use only a handful of routing protocols which interact in very specific ways
目的
(1) verifying security and availability invariants hold across arbitrary failures
(2) equivalence testing.
方法
ARC: abstract representation for control planes
- accurately model the common protocols (OSPF, RIP, and eBGP) and mechanisms (static routes, ECMP, access control lists, and route redistribution)
- is composed of a series of weighted digraphs that are routing protocol- independent.
- the true forwarding path between network locations under any failure scenario is provably included in the ARC’s digraphs, verifying key security and availability invariants boils down to computing simple graph characteristics of the ARC
Example 1
(a)的意图：由于ACL在D出接口的应用，子网S永远不能到达T
(b)的意图：子网S通过U到达T
(a)到(b)的更改，埋下了潜在隐患：当没有link failure时，数据包的路径是: F→Z→Y →B→D→A，在D这里由于ACL的存在，数据包是不可达的；但是发生link failure时，比如链路BC和BD同时断掉，则次优路径BA会发生作用，导致(a)中意图失效；
Example 2
网络的ARC是一种数据结构，它包含一个加权有向图的集合，每个“流量类”都有一个，即一个源-目标子网对。
Pathset-equivalent graphs
包含在任意链路故障下，真实网络中数据包从src到dst转发所有可能的路径
Path-equivalent graphs
对ARC中的有向图各条边调整权值，使得在链路故障的对应的边被去除时，从src到dst所选择的cost最小的路径与真实网络一致
in a real ARC the weights are a function of the relative rank of specifific routing protocols, AS paths, and network links.
ARC验证机制
I1: Always blocked
要在任意实现任意故障的情况下，通过从src节点开始遍历ETG来检查路径的存在。如果dst节点仍然未访问，则该属性保留。否则，假设ETG是Path-equivalent的，我们提供了最短的路径作为一个反例。
I2: Always reachable with < k failures
如果src到dst至少存在k条边不相交的路径，则在k failure的情况下始终能可达。在任意无环有向图中找到边缘不相交路径的数目是NP完全问题，但在单位权图中，问题简化为计算最大流/最小割。
I3: Always isolated
只有当两个流量类的ETG没有任何共同的边时，流量隔离不变变量才被保证保持不变。
I4: Always traverse a waypoint
ETG中删除所有路径点节点，并检查是否存在从数据节点到数据节点的路径。如果存在这样的路径，那么流量可能会选择一些不穿越路径点的路径；我们将此路径作为反例返回。
I5：Equivalence Testing
通过检查两个控制平面的ARC是否具有相同的顶点、边和边权重来测试两个控制平面的等效性