基于MapReduce的OpenFlow网络属性验证技术

刘 艺 雷 程 张红旗 杨英杰

(解放军信息工程大学 郑州 450001) (河南省信息安全重点实验室(解放军信息工程大学) 郑州 450001)(liuyi9582@126.com)



基于MapReduce的OpenFlow网络属性验证技术

刘 艺 雷 程 张红旗 杨英杰

(解放军信息工程大学 郑州 450001) (河南省信息安全重点实验室(解放军信息工程大学) 郑州 450001)(liuyi9582@126.com)

针对OpenFlow网络中由程序自动改变数据平面状态方式引起的流表配置错误问题，提出1种基于MapReduce的OpenFlow网络属性验证技术.首先，利用OpenFlow网络控制转发分离的特点，设计支持实时与非实时2种验证方式的技术架构.其次，提出基于MapReduce模型的非实时验证算法，在Map阶段划分规则等价类，在Reduce阶段构建基于交换机端口谓词的网络转发图并分析可达性，以实现对网络属性的并行验证.与此同时，利用原子谓词消除谓词集合冗余项和规则匹配域转换的方法，提高可达性分析效率.此外，在非实时验证算法的基础上，结合网络更新事件提出实时验证算法，实现网络状态改变时的增量式网络属性验证.最后，理论分析和仿真实验验证了该技术的运行效率和存储开销，并分析了其对TCP连接建立时间的影响.

流表配置；网络可达性分析；网络属性验证；MapReduce模型；OpenFlow网络

软件定义网络[1](software-defined networking， SDN)是美国斯坦福大学CleanSlate项目组提出的1种逻辑控制和数据转发分离的网络架构，基于OpenFlow[2]实现SDN已成为主流趋势[3].在OpenFlow网络中，研究人员通过在中央控制器上开发应用程序，驱动其生成、维护和下发流表，并由OpenFlow交换机简单地按照流表匹配执行，从而灵活控制管理网络.然而，这种自动化的软件管控网络方式存在安全问题.单个程序的高复杂性和多个程序间的竞争关系导致流表配置易出错，网络数据平面状态属性与预期不符，如存在转发回路、出现路由黑洞、访问控制规则失效等，造成交换机无法正确转发数据包，这不仅降低了网络性能，而且违反安全策略危害网络安全[4].

针对这一问题，一种解决方法是从控制平面角度，在应用程序部署前结合网络拓扑验证程序的正确性，如NICE[5]采用模型检查和符号执行2种技术测试控制器程序是否出现缺陷，但由于程序代码通常是不可访问的[6]，该方法实用性不高，此外由于它可扩展性较差，不适用于大型程序.另一种解决方法是从数据平面角度，基于数据平面信息进行网络属性验证[7]，即通过分析全网流表规则验证网络的全局状态是否满足期望的网络属性.一般地，OpenFlow网络属性验证是指验证与功能正确性相关的网络属性[4]，如转发回路、路由黑洞、可达性和数据包目的地控制等.已有的网络属性验证技术如FlowChecker[8]，Anteater[9]，Hassel[10]等普遍耗时长，每次验证至少需要几秒，对于现代数据中心网络等数据平面状态改变频率能达到每秒上千次[11]的网络，不能在网络运行时实时验证流表配置是否出错.

因此，针对现有技术存在验证耗时长、难以满足实时性需求的问题，本文提出了基于MapReduce的OpenFlow网络属性验证技术(MapReduce-based network property verification technique for OpenFlow network， MRVeri)，支持实时和非实时2种验证工作模式.通过引入MapReduce模型实现并行验证和网络状态改变时增量验证，分别加快非实时与实时验证速度；通过将规则谓词聚合为交换机端口谓词和采用原子谓词将规则匹配域的多维集合运算转换为整数集合运算进一步提高验证效率；此外，通过基于原子谓词的谓词表示方式消除冗余项降低存储开销.

1 相关工作

OpenFlow网络采用集中式控制方式，中央控制器能提供统一的、确定的网络数据平面信息[4]，为基于数据平面信息的网络属性验证提供了良好的基础.目前，OpenFlow网络属性验证研究主要集中在3个方面：

1) 基于有限状态自动机的验证.此类研究将数据包看作有限状态自动机，当前状态由数据包头和所处设备定义，下一个状态由包头和当前设备的规则决定，验证网络属性等同于检测终态集合是否存在不期望的状态.FlowChecker将用2元决策图(binary decision diagram， BDD)描述的规则和用计算树逻辑(computation tree logic， CTL)编写的网络属性输入到SMV中进行验证.FLOVER[12]将规则和网络属性翻译为Yices断言，利用Yices SMT进行验证.Hassel将数据包定义为几何空间中的点，规则对数据包的动作定义为该几何空间中的转换函数，设计了多种算法验证不同的网络属性.

2) 基于布尔可满足问题的验证.此类研究将网络属性验证问题转换为逻辑网络的可满足性问题.Anteater将规则转换为布尔表达式，和网络属性联合起来组成SAT实例，输入到SAT解决器中执行分析.

3) 基于图的验证.此类研究以图的形式组织全网规则，借助图搜索算法计算网络可达性，从而验证网络属性.VeriFlow[13]通过划分规则等价类和建立转发图高速缓存实现实时验证，但当规则有多个匹配字段时规则等价类的数目可能相当大，会影响验证速率.NetPlumber[11]通过设计管道图(plumbing graph)及其增量更新算法实现实时验证，并提出规则聚类技术使得当规则更新时多个规则类能独立验证，但在链路状态变化时耗时长.Libra[14]首次引入MapReduce实现并行验证，但它建立在数据包只基于目的IP地址前缀进行转发的基础上，不适用于OpenFlow网络.

经分析可知，从时间开销来看，基于有限状态自动机和基于布尔可满足问题的验证技术普遍速度慢，适合以非实时方式验证网络属性；基于图的验证技术速度有所提高，但仍有提升空间，而且在链路状态改变情况下耗时长.从存储开销来看，已有研究普遍未考虑压缩规则信息，降低存储开销.因此，亟需1种支持实时和非实时2种方式、速度快且存储开销小的OpenFlow网络属性验证技术，以解决规则和链路更新造成网络数据平面状态出错的问题.

2 基于MapReduce的OpenFlow网络属性验证技术

Fig. 1 Technical framework of network property verification technique for OpenFlow network.图1 OpenFlow网络属性验证技术架构

OpenFlow网络的集中控制特性为自动化网络属性验证提供了契机[11].结合OpenFlow网络控制转发分离特点，本文提出了支持实时和非实时验证功能的OpenFlow网络属性验证技术，其技术架构如图1所示，主要包括位于中央控制器和交换机之间的验证代理和验证器2部分.非实时验证指在规则下发到交换机后对网络数据平面快照(即全网规则和链路信息)进行整体验证，是实时验证的基础，一般用于状态改变不频繁的网络，可以减少网络通信资源消耗，主要实现步骤如图1中①②③④所示，验证器在收到网络管理员发送的网络属性验证请求后，通知验证代理获取数据平面快照，随后对返回的快照进行验证，将结果反馈给管理员，管理员可依此调整网络.实时验证指验证过程发生在规则下发到交换机前或网络数据平面发生链路更新等状态改变事件时，为了不影响网络运行通常是基于非实时验证结果进行增量式验证，一般用于状态频繁改变的网络，主要实现步骤如图1中⑤⑥⑦所示，验证代理从控制器与交换机的通信报文中提取有用信息发送给验证器进行验证，并根据收到的验证结果执行既定操作，如拒绝规则更新或发出警报等.

由此可知，OpenFlow网络属性验证技术的核心在于验证器上运行的验证算法.由于网络规模大、规则数目多，为了提高验证速率，在进行非实时验证时，需要分解验证任务实现并行验证；在进行实时验证时，需要只分析受规则或链路更新影响的部分网络实现增量验证，因此验证算法引入MapReduce模型.首先进行规则链路信息预处理，之后，在非实时验证时，Map阶段按照规则匹配域划分规则等价类，Reduce阶段按规则等价类将规则组织成若干子图，独立、并行地进行分析；在实时验证时，Map阶段由规则或链路更新信息确定受影响的规则等价类，Reduce阶段对相应子图进行增量更新及分析.

2.1 规则链路信息预处理

依据OpenFlow标准[15]，规则r(inport,C,pri,a).其中，inport具有全网唯一性，表示规则对从特定端口进入其所在交换机的数据包起作用；C为匹配域，包括源/目的IP、端口等匹配字段；pri是规则优先级；a为动作.a主要包括3种：fwd(port)表示将数据包从端口port转发出去；setm→n(port)表示将数据包头由m改为n后从端口port转发出去；drop表示丢弃数据包，为统一起见，可看作从特殊端口port*转发出去.

2)inport和outport分别为数据包进入和离开交换机的端口号.

3)flag_r是规则状态标识，仅在实时验证时使用，flag_r=1表示增加规则，flag_r=0表示删除规则.

2.2 基于MapReduce的非实时网络属性验证

基于MapReduce的非实时网络属性验证流程如图2所示，Map阶段划分规则等价类，Reduce阶段基于构建的网络转发图进行属性验证.

Fig. 2 Workflow of non-real-time network property verification.图2 非实时网络属性验证流程

2.2.1 Map阶段

Map阶段的主要任务是依据代理提供的规则信息划分规则等价类.通常规则分类有2种方案：

1) 基于交换机，每个mapper根据规则所属交换机的标识将其交付给不同reducer，但由于规则存在复杂的依赖关系，reducer在验证过程中需要频繁通信，即使是1条规则发生改变也可能需要多个reducer重新执行验证，而且不同交换机上的规则数目差异大；

2) 基于子网，每个mapper根据规则目的IP地址所属的子网将规则划分入不同等价类，此种方法能构造相对完整的转发路径，reducer之间无需或者少量通信就能完成验证任务.因此，本文方案以后者为依据，提出基于子网trie树的规则等价类划分.

记wspa,dst(r)spa分别表示子网w的地址空间范围和规则r的目的IP地址空间范围，若wspa⊆dst(r)spa，则称规则r匹配子网w；若dst(r)spa⊆wspa，则称子网w匹配规则r.

由此，规则等价类定义如下：

定义1.规则等价类Rw={r1,r2,…,rn}，若网络中存在子网w，对于ri(1≤i≤n)，或者ri匹配w，或者w匹配ri.

将规则r分入不同的规则等价类，即找到子网集合W={w1,w2,…,wm}，对于wj(1≤j≤m)，或者r匹配wj，或者wj匹配r.

为快速找到W，将规则目的IP地址和子网地址转化为二进制数形式，dst(r)={0,1,x}λ(可从Pr中获得)，w={0,1,x}λ，其中λ表示地址长度.假设x<0<1，则按从高位到低位的顺序比较，2个地址具有大小关系.据此，规则r匹配子网w意味着dst(r)≤w，子网w匹配规则r意味着dst(r)≥w.

因为网络中规则数目往往远大于子网数目，所以mapper构建子网trie树，1个子网地址对应1个trie树节点，称为实心节点，空心节点意味着没有对应的子网，但为了构建trie树必须生成.假设mapper数目为N，规则总数为S，每个mapper被分配S/N条规则，每次读入1条规则，提取其目的IP地址，转换为二进制数形式，从子网trie树根结点出发遍历，遍历过程与传统路由器进行数据包转发时采用的二进制trie树查找算法类似，即在每个内部节点，遇到0遍历左子树，遇到1遍历右子树，但本文的目的是找到与规则r满足关系——r匹配w或者w匹配r——的所有子网w，因此往往无需遍历整棵树.遍历过程分2种情况：

1)dst(r)>n，若n为实心节点，则W=W∪{n}(假设最初W=∅)；若n为空心节点，则W=W.

2)dst(r)≤n，因为子网trie树中任一节点小于其子孙节点，所以有dst(r)≤n

直至当前节点无子孙节点或出现上述情况2时，结束搜索.

对于wj∈W，mapper输出wj，规则信息对，其中规则信息为，由子网地址(即wj)标识不同的规则等价类.

子网trie树的构建也可以采用传统网络中的路由表压缩算法，减小存储空间，实现快速更新.

2.2.2 Reduce阶段

Reduce阶段的主要任务是根据收到的同一子网对应的规则信息r,outport,pri和所有链路信息构建网络转发图进行可达性分析，从而验证网络属性.为了降低网络转发图规模、加快可达性分析效率，本文提出基于交换机端口谓词(SP)的网络转发图构建算法和基于原子谓词(AP)的网络可达性分析算法.

1) 基于SP的网络转发图构建算法

为计算SP，首先以(inport,pri)为关键字采用最高位优先法(most significant digit first, MSD)对规则进行排序，其中inport是主位关键字，pri为次位关键字，排序结果如下：

之后，利用RP_to_SP算法将已排序规则转换为SP，其中Set(Pr)函数表示将Pr按照相应规则的“setm→n(port)”动作要求进行改变.RP_to_SP算法如下：

算法1. RP_to_SP算法.

输入: 有序的转发表、端口集合{1,2,…,k};

forj=1 tokdo

end for

f←false；

g←inport1；

i←1；

whilei≤m

ifinporti=gthen

else

end if

f←f∨Pri；

i←i+1；

else

{f←false,g←inporti,i←i}；

end if

end while

Fig. 3 Network topology and its forwarding graph.图3 网络拓扑及其网络转发图

以图3(a)(b)中的网络拓扑及其网络转发图为例，图3中节点以端口号标识，以SP为节点值，若端口i是j的内部(外部)上游端口，则有1条从节点i到j的以虚线(实线)标识的有向边，p*是为“drop”动作规则设置的特殊端口.比如，p6和p7之间无虚线连接，表示从p6进入交换机的数据包不会从p7转发出去.

与文献[14]中以单个交换机为节点、以物理链路为边的转发图相比，基于SP的网络转发图表达了更加细粒度的规则信息，更加符合OpenFlow规则特点.并且与文献[11]中以规则为节点、以规则关系为边的转发图相比，它将规则信息聚合到端口，降低了图的规模，减少了存储开销的同时也压缩了之后需要进行的图搜索空间，在时间和存储开销方面都更优.

2) 基于AP的网络可达性分析算法

已有的网络属性验证技术的核心算法是计算网络可达性.本文基于网络转发图建立端口可达树，并将网络属性等价转换为端口可达性，通过遍历端口可达树进行验证，同时得到具体的违反信息.然而在计算可达性的过程中，由于规则匹配域的每一维上有许多允许的区间和任意的覆盖，在最坏情况下，多维集合交并运算的计算复杂度为O(2n)(n是包头位数).因此，为了提高可达性分析速度，本文引入原子谓词[16].AP是从给定谓词集合Ψ中提取的若干谓词，记AP集合为B(Ψ)={b1,b2,…,bm}，它满足5个条件：

① ∀i∈{1,2,…,m},bi≠false；

③ 若i≠j，则bi∧bj=false；

⑤m是所有满足条件①～④的谓词集合的元素数目最小值.

若以整数{1,2,…,m}标识每个AP，可得谓词p对应的整数集合S(p)⊆{1,2,…,m}，由此谓词在多维空间上的合取(析取)转化为更加快速的整数集合交(并)运算，而且AP集合远小于Ψ[16]，消除了冗余项，减少了谓词存储开销.

算法2. ReTree_path_Build算法.

输入: 图G、端口s;

输出: 端口s可达树的一条路径.

if (s是输入端口) then

/*t和temp分别暂时存储节点标识和节点值*/

while(1)

/*寻找数据包能到达的内部下游端口*/

(t,temp)=Inner_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

/*在可达树中增加节点*/

else

ReTree.add(t,temp);

/*寻找数据包能到达的外部下游端口*/

(t,temp)=External_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

elseReTree.add(t,temp);

end if

end if

end while

else

/*S(P)满足∃p,(S(P),p)∈

(t,temp)←(s,∪S(P));

while(1)

(t,temp)=External_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

else

ReTree.add(t,temp);

(t,temp)=Inner_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

elseReTree.add(t,temp);

end if

end if

end while

end if

Inner_relate(G,(t,temp))

{ /*寻找数据包能到达的内部下游端口*/

if (∃v,v=in_next(G,t)) then

temp∩S(P)≠∅) then

S(v)=temp∩S(P);

end if

temp∩S(P)≠∅) then

S(v)=S(v)∪Set(temp∩S(P));

(t,temp)←(v,S(v));

else (t,temp)←∅;

end if

else

路由黑洞报告; /*发现路由黑洞*/

(t,temp)←∅;

end if

return (t,temp).

}

External_relate(G,(t,temp))

{ /*寻找数据包能到达的外部下游端口*/

if (∃v,v=out_next(G,t)) then

if (!visisted(v)) then

(t,temp)←(v,S(v));

else (t,temp)←∅;

end if

else

转发回路报告; /*发现转发回路*/

(t,temp)←∅;

end if

else (t,temp)←∅;

end if

return (t,temp).

}

以图3所示网络为例，表1和表2分别是用AP集合表达的网络转发图中各节点输入和输出谓词.

Table 1 Input Predicates of Nodes

Table 2 Output Predicates of Nodes

图4是端口p1的可达树，它涵盖了经过和未经过“setm→n(port)”操作的数据包转发路径信息，假设验证策略“p1和p11所连主机不能通信”，由可达树可知，存在数据包b3∨b4经过端口序列p1→p2→p4→p5→p7→p8→p10→p11后变为b6∨b8到达p11，故网络不满足该策略.

Fig. 4 Reachability Tree of p1.图4 端口p1可达树

此外，为了加快验证速度，可在树节点中存储从根节点到该节点的路径上的端口序列，并为每棵可达树维护1张Hash表(HT)，它由一系列关键字，值对组成，其中“关键字”是端口号v，“值”是树中标识为v的节点集合，则由HT(v)可得v在可达树中对应的节点，节点值为从端口s到v的数据包集合，存储的端口序列为具体路径信息.比如在验证路径点(waypoint)策略时，如从端口s到d的数据包必须经过某个路径点，如端口m，可由HT(d)得到d对应的节点，通过检查该节点中存储的端口序列是否存在m进行验证.采用相似的方法可以验证更加复杂的路径点策略，如所有来自端口s的数据包应该经过某个路径点集合，或者所有从端口s到d的数据包应该按序经过指定的路径点序列.

2.3 基于MapReduce的实时网络属性验证

基于MapReduce的实时网络属性验证建立在非实时验证的基础上，通过增量更新网络转发图和端口可达树实现实时网络属性验证，主要分6种情况:

1) 增加规则rnew.如图5所示，mapper将规则的目的IP地址与子网trie树进行匹配，输出w，规则信息对，发送至不同reducer上.reducer需要：①根据rnew的规则信息更新相应SP；②更新AP集合；③使用更新后的SP和AP集合更新网络转发图和端口可达树.为提高处理速度，步骤②③可并行进行.

Fig. 5 Real-time verification workflow for adding rules.图5 规则增加时实时网络属性验证流程

在步骤①中，由于rnew的RP可能与已有规则的RP存在交集，为了加快更新速度，规则列表中增设字段Ri表示实际能被规则ri处理的数据包集合，如式(1)所示：

Ri=Pri∧(∨inportj=inporti,Prj∩Pri≠∅,prij>prii

(1)

则对于端口x，SP中各元素如式(2)～(4)所示：

(2)

(3)

(4)

在步骤②中，SP的改变可能导致AP集合变化.假设原有AP集合为B({p1,p2,…pn})，当增加谓词pnew时，按照式(5)计算新的AP集合.

Β({p1,p2,…,pn}∪{pnew})={bk=ak1∧ck2|

ak1∈B({p1,p2,…pn}),

(5)

当删除谓词pold时，原有AP集合可能不满足2.2.2节中条件⑤，需要最小化.基本思路是以prt(bi)={pj|i∈S(pj),1≤j≤n}衡量AP的表达能力，对于2个不同的b,b′∈B({p1,p2,…，pn})，若prt(b)=prt(b′)，则将它们融合，采用文献[16]中最小化AP集合算法可得B({p1,p2,…,pn}-pold).

在步骤③中，若端口x的SP在步骤①中被改变，则需要更新含有x的可达树.利用每棵可达树的Hash表计算x所在节点(即HT(x))，对该节点及其子孙节点的节点值进行更新.单个节点的更新如图6所示：

Fig. 6 Updating a single node.图6 单个节点更新示意图

(6)

由此可得到带有临时谓词集合的临时可达树.在完成AP集合更新后，需要将临时可达树“转正”，分2种情况：①若AP集合未发生改变，则只需将Φ中的谓词转换为相应的整数集合；②若AP集合发生改变，则基于新的AP集合重新遍历可达树，计算相应的节点值.

2) 删除规则r.与情况1类似，首先由mapper将r发送至相应的reducer上，reducer根据r更新SP、AP集合和可达树.

3) 增加子网.mapper向子网trie树中插入新的子网，并计算其规则等价类，reducer为新增等价类构建网络转发图.

4) 删除子网.mapper将子网从子网trie树中删除，并通知相应的reducer删除与该子网有关的信息.

5) 启用新链路.网络的链路状态对SP和AP集合没有影响，假设新链路连接2个端口p1和p2，由HT(p1)(HT(p2))在可达树中定位它们对应的节点，并以p1(p2)为起点对增加新链路后的网络转发图进行DFS搜索，扩展可达树，同时修改Hash表.

6) 中断旧链路.与情况5类似，由HT(p1)(HT(p2))在可达树中定位节点，删除这些节点及其子孙节点，并修改Hash表.

2.4 时间复杂度分析

由于实时网络属性验证是对非实时验证中的SP，AP集合和端口可达树进行增量式更新，在最坏情况下退化为非实时验证，故本文只分析非实时网络属性验证的时间复杂度.Map阶段的时间开销分为构建子网trie树和遍历子网trie树2部分.因为向trie树插入IP地址前缀相当于对trie树进行查找，其时间是小于或等于IP地址长度的常量，所以构建子网trie树的时间复杂度为O(w)，其中w是子网数目.同时，若m个mapper共同对r条规则进行等价类划分，需要O(rm)时间遍历trie树，故总的时间复杂度为O(w+rm).Reduce阶段的时间开销分为基于SP构建网络转发图和基于AP分析网络可达性2部分.以1个reducer为例计算时间复杂度.假设网络中有e条链路和n个交换机，平均每个交换机含有k个端口和1张含m条规则的流表.基于SP构建网络转发图阶段，计算SP包括规则排序和执行RP_to_SP算法2项操作，时间复杂度为O(2m+n(k+m))；构建网络转发图主要是寻找内部关联和外部关联关系，时间复杂度为O(nk2+e).基于AP分析网络可达性阶段，计算AP集合的时间复杂度取决于给定谓词集合大小[16]，在最坏情况下每条规则含2个互不重叠的谓词，给定谓词集合大小为2mn，时间复杂度为O(mn)；网络可达性分析的时间开销与待验证的网络属性有关，在此只分析构建1棵可达树，主要操作是遍历转发图的边，在最坏情况下同一交换机上任2个端口之间都存在内部关联关系，时间复杂度为O(nk2+e).故在最坏情况下总的时间复杂度为O(nk2+nk+mn+e).

3 实验结果与分析

3.1 实验条件

本文在Hadoop 2.2.0平台上开发MapReduce程序进行仿真实验，硬件选取情况如表3所示，节点之间以100 Mbps带宽互联，操作系统为Ubuntu 12.04.

Table3 Information of Hadoop Platform Hardware

为与Hassel和NetPlumber等工具进行性能对比，数据集采用Stanford大学主干网[17]数据和Internet2[18]数据，如表4所示：

Table4 Information of Experimental Datasets

3.2 实验结果分析

为验证MRVeri的实时与非实时验证效率，实验分为3部分：1)基于整体实验数据集进行非实时网络属性验证；2)通过随机改变实验数据集中的规则和链路信息模拟动态网络进行实时网络属性验证；3)基于Mininet仿真平台评估MRVeri对TCP连接建立时间的影响.

1) 非实时网络属性验证实验

采用MRVeri和Hassel验证Stanford大学主干网和Internet2中是否存在转发回路，若存在则返回具体的路径.其中，对于Stanford大学主干网，为与文献[10]中的结果进行比较，选取30个端口检测转发回路.实验结果显示，MRVeri和Hassel都在Stanford大学主干网和Internet2中分别发现12条和2条回路路径，时间开销如表5所示:

Table5 Time Overhead of MRVeri and Hassel

由表5可看出，MRVeri的速率比Hassel分别快约37倍和45倍.原因有3点：1)引入了MapReduce，可以实现并行验证；2)构造端口可达树的速度快，为证明这一点，在MRVeri(只采用1个reducer)和Hassel都完成规则预处理后，随机选取端口计算可达树，每个端口可达树的时间开销CDF图如图7所示，可知MRVeri最大耗时不足1ms，明显快于Hassel；3)AP集合可以压缩真实网络中规则的大量冗余，如Stanford大学主干网和Internet2的AP集合大小分别为509和216，远小于其规则数目.

Fig. 7 CDF of constructing time for each port reachability tree.图7 每个端口可达树的时间开销CDF图

2) 实时网络属性验证实验

为评估MRVeri在实时验证方面的性能，分别在规则增加、规则删除、链路启用和链路失效这4种情况下测算更新端口可达树时间.

为模拟规则增加场景，先随机选取实验数据集中90%规则构造端口可达树，之后将剩下的10%规则逐条插入.类似地，在规则删除实验中，先对实验数据集中所有规则计算端口可达树，再随机选取10%规则逐条删除.为模拟链路启用场景，先随机选取实验网络拓扑中10%的链路，标识其为不可用，并构造端口可达树，之后逐条将这些链路的标识修改为可用.链路失效场景则是先对整网计算端口可达树，再随机选取10%的链路，逐条标识其为不可用.图8和图9分别表示在Stanford主干网和Internet2中端口可达树更新时间的分布情况.

Fig. 8 CDF of update time of port reachability trees in Stanford.图8 Stanford主干网端口可达树更新时间CDF图

Fig. 9 CDF of update time of port reachability trees in Internet2.图9 Internet2端口可达树更新时间CDF图

由图8和图9可知，当规则增加时，MRVeri对Stanford主干网和Internet2中绝大部分可达树进行更新的时间分别小于0.37 ms和0.7 ms；当规则删除时，分别小于0.5 ms和1 ms；当链路启用时，分别小于1.01 ms和0.28 ms；当链路失效时，更新时间最快，分别小于0.007 ms和0.002 ms.与文献[11]中NetPlumber在规则增加和链路启用情况下的更新时间对比分别如图10和表6所示.

在规则增加情况下，MRVeri在Stanford中与NetPlumber相当，在Internet2中略优于NetPlumber;但在链路启用时，远优于NetPlumber，主要因为网络链路状态对SP和AP集合没有影响，只需从受影响的端口出发进行DFS搜索更新可达树，而NetPlumber需要进行更多的操作来更新其所维护的管道图.此外在链路失效时Veriflow平均需要1.15 s验证网络属性，相较MRVeri更慢.

Fig. 10 Update time in rule adding case.图10 规则增加情况下更新时间图

DataSourceNetPlumberMRVeriMeanMedianMeanMedianStanford302021200.10.037Internet2476023200.0240.0052

3) TCP连接建立时间实验

Fig. 11 Time of building TCP connection.图11 TCP连接建立时间图

在Mininet仿真平台上模拟OpenFlow网络，它以Floodlight为控制器，具有50个OVS交换机，每个交换机上连接1个主机.运行TCP客户程序的主机每隔5s随机向某个运行TCP服务器程序的主机发起连接，并在连接建立后立即释放，同时，为使Floodlight尽可能多地下发新规则到OVS交换机上，设置规则超时时间为1 s.由于MRVeri包括验证代理和验证器2部分，故实验分别在不运行MRVeri、仅运行验证代理和完整运行MRVeri的情况下，测试不同数目主机对建立TCP连接的平均时间，结果如图11所示:

当MRVeri执行实时网络属性验证时，TCP连接建立平均时间增加了约41%，其中验证代理使其增加约35.4%(验证算法仅约5.6%)，这是由于验证代理处于控制器与交换机之间，需要缓存大量通信报文、提取和预处理有用的规则链路信息、与底层交换机通信等，可通过将验证代理纳入控制器中减少开销，从而使属性验证过程对终端用户透明.此外，随着主机数目的增多，TCP连接建立平均时间的增加幅度未显著增大.

4 结束语

针对OpenFlow网络流表配置易出错问题，本文从数据平面角度出发，提出了基于MapReduce的网络属性验证技术.它通过提供实时和非实时验证，方便代理或管理员及时调整网络，减少错误配置带来的损失.针对网络规模大、规则数目多的特点，通过引入MapReduce实现并行非实时验证和增量实时验证.此外，由于网络属性验证是以对网络转发图的可达性分析为基础，针对已有可达性分析算法速度慢的问题，通过提出RP_to_SP算法聚合规则谓词，以构建表达信息更细粒度、规模更小的网络转发图；通过采用原子谓词，将可达性计算过程中规则匹配域的多维集合运算转换为整数集合运算，以提高效率、消除冗余项和优化验证存储开销.仿真实验选取了2个实际网络拓扑和数据，并模拟了OpenFlow网络中TCP连接建立场景.结果表明,在非实时工作模式下，MRVeri比Hassel分别快约37倍和45倍，存储开销分别少约33倍和24倍；在实时工作模式下，当网络链路改变时，MRVeri验证速度远优于NetPlumber，Veriflow等现有实时验证技术，并且其实时验证算法对TCP连接建立时间影响小.

[1]McKeown N. Software-defined networking[C] //Proc of the 28th IEEE INFOCOM. New York: IEEE Communications Society, 2009: 30-32

[2]McKeown N, Anderson T, Balakrishnan H, et al. OpenFlow: Enabling innovation in campus networks[J]. ACM SIGCOMM Computer Communication Review, 2008, 38(2): 69-74

[3]Zuo Qingyun, Chen Ming, Zhao Guangsong, et al. Research on OpenFlow-Based SDN technologies[J]. Journal of Software, 2013, 24(5): 1078-1097 (in Chinese)

(左青云, 陈鸣, 赵广松, 等. 基于 Open Flow 的 SDN 技术研究[J]. 软件学报, 2013, 24(5): 1078-1097)

[4]Zhang S, Malik S, McGeer R. Verification of Computer Switching Networks: An Overview[M]. Berlin: Springer, 2012: 1-16

[5]Canini M, Venzano D, Peresini P, et al. A NICE way to test OpenFlow applications[C] //Proc of the 9th USENIX Symp on Networked System Design and Implementation. Berkeley, CA: USENIX Association, 2012: 127-140

[6]Sherwood R, Gibb G, Yap K K, et al. Can the production network be the testbed?[C] //Proc of the 9th USENIX Symp on Operating Systems Design and Implementation. Berkeley, CA: USENIX Association, 2010: 1-6

[7]McGeer R. Verification of switching network properties using satisfiability[C] //Proc of IEEE ICC’12. Piscataway, NJ: IEEE, 2012: 6638-6644

[8]Al-Shaer E, Al-Haj S. FlowChecker: Configuration analysis and verification of federated OpenFlow infrastructures[C] //Proc of the 3rd ACM Workshop on Assurable and Usable Security Configuration. New York: ACM, 2010: 37-44

[9]Mai H, Khurshid A, Agarwal R, et al. Debugging the data plane with anteater[J]. ACM SIGCOMM Computer Communication Review, 2011, 41(4): 290-301

[10]Kazemian P, Varghese G, McKeown N. Header space analysis: Static checking for networks[C] //Proc of the 9th USENIX Symp on Networked System Design and Implementation. Berkeley, CA: USENIX Association, 2012: 113-126

[11]Kazemian P, Chan M, Zeng H, et al. Real time network policy checking using header space analysis[C] //Proc of the 10th USENIX Symp on Networked System Design and Implementation. Berkeley, CA: USENIX Association, 2013: 99-111

[12]Son S, Shin S, Yegneswaran V, et al. Model checking invariant security properties in OpenFlow[C] //Proc of IEEE ICC’13. Piscataway, NJ: IEEE, 2013: 1974-1979

[13]Khurshid A, Zhou W, Caesar M, et al. VeriFlow: Verifying network-wide invariants in real time[J]. ACM SIGCOMM Computer Communication Review, 2012, 42(4): 467-472

[14]Zeng H, Zhang S, Ye F, et al. Libra: Divide and conquer to verify forwarding tables in huge networks[C] //Proc of the 11th USENIX Symp on Networked System Design and

Implementation. Berkeley, CA: USENIX Association, 2014, 14: 87-99

[15]Openflow Switch Consortium. Openflow switch specification, version 1.0.0[OL]. [2015-03-09]. https://www.open networking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-spec-v1.0.0.pdf

[16]Yang H, Lam S S. Real-time verification of network properties using atomic predicates[C] //Proc of IEEE ICNP’13. Piscataway, NJ: IEEE, 2013: 1-11

[17]Atlassian. Header Space Library and NetPlumber[CP/OL]. [2015-04-15]. https://bitbucket.org/peymank/hassel-public

[18]Internet2 Community. The Internet2 Observatory Data Collections[CP/OL]. [2015-04-15]. http://www.internet2.edu/research-solutions/research-support/observatory

Liu Yi, born in 1991. PhD candidate. Her main research interests include SDN security and security policy management.

Lei Cheng, born in 1989. PhD candidate. His main research interests include network security and MTD (leicheng12150@gmail.com).

Zhang Hongqi, born in 1962. Professor and PhD supervisor. His main research interests include network security and classification protection (zhq37922@126. com).

Yang Yingjie, born in 1971. PhD and associate professor. His main research interests include security management and situation awareness (yang-yj1002@263. net).

MapReduce-Based Network Property Verification Technique for OpenFlow Network

Liu Yi, Lei Cheng, Zhang Hongqi, and Yang Yingjie

(PLAInformationEngineeringUniversity,Zhengzhou450001) (HenanKeyLaboratoryofInformationSecurity(PLAInformationEngineeringUniversity),Zhengzhou450001)

Aimed at the problem of configuration errors of flow tables resulting from automatic change of data-plane state by software in OpenFlow network, a MapReduce-based network property verification technique is proposed. Firstly, by exploiting the separation of logic control from data forwarding in OpenFlow network, a novel technical framework providing non-real-time and real-time verification is designed. Further, on the basis of the advantage of parallel computing in MapReduce, a non-real-time verification algorithm is presented, which can verify network properties in parallel in two phases. In Map phase, it slices network into equivalence classes. In Reduce phase, it builds network forwarding graph with switch port predicates and conducts network reachability analysis. Meanwhile, with the help of atomic predicates, it can not only eliminate the redundancy of the set of switch port predicates, but also convert highly computation-intensive operations on predicates to those on sets of integers, speeding up computation of network reachability further. Based on it, a real-time verification algorithm is proposed. According to different network update events, it applies different changes to the results of non-real-time verification in order to incrementally verify properties. Finally, theoretical analysis and experimental results show the low time and storage overhead of the proposed technique. Additionally, its effect on the time of building TCP connection is also analyzed.

flow table configuration; network reachability analysis; network property verification; MapReduce model; OpenFlow network

2015-06-14；

2015-09-06

国家“八六三”高技术研究发展计划基金项目(2012AA012704)；郑州市科技领军人才项目(131PLJRC644)

TP393.08

This work was supported by the National High Technology Research and Development Program of China (863 Program) (2012AA012704) and Zhengzhou Science and Technology Talents Project (131PLJRC644).