基于B方法的流量控制系统的实现

【摘要】 通过对形式化B方法的研究,结合网络流量控制系统模型,讨论了该模型在形式化B方法下的具体应用,给出了该系统的抽象机模型和精化过程。

【关键词】 B方法;流量控制;特征码

随着网络应用的日益增多和新的网络技术的不断出现,网络流量的控制和管理面临着新的挑战。尤其是P2P技术的出现,给网络路由器造成了极大的负担,导致很多正常的网络业务无法正常运转。由此,市场上出现了流量控制系统,在一定程度缓解了流量对带宽造成的压力。但是目前的流量控制系统对协议识别率普遍较低,存在很多误识别现象,给管理员的管理工作带来很多不便。为了使协议识别更加精确,策略的配置更加合理,将采用形式化B方法对系统进行建模、精化,在FreeBSD下实现该系统。

一、形式化B方法与流量控制系统

1.形式化B方法概述。B方法是一种对软件系统进行描述、设计和编码的方法。这种方法涵盖了软件开发的各个方面,通过一系列的精化步骤进行设计,产生了层次性体系结构及代码。建立在Zermelo - Frankel 集合论的基础上,能够严格地进行形式化规格说明的正确性证明。采用抽象机符号(Abstract Machine Notation,AMN)对软件的规格说明进行类型检测、动态验证、数学证明等确保设计过程的正确,具有精确性、无二义性、一致性、能进行推理等特点。AMN 中结构化的机制增强了信息隐藏和数据封装,严密的部件接口控制确保了大型开发中各个部件的独立开发。

2.流量控制系统概述。流量控制系统一般部署在内网网关和路由器之间,对进出口的流量进行控制。网络流量控制模型一般包括流量分类器、队列管理器、流量整形器和流量监测器等几个部分。数据包首先经过流量分类器,根据数据包的特征对该流量进行特征码识别,接着对识别后的数据包进行分类汇总,再按照事先配置好的策略、优先级将数据包发送至队列管理器,如果该数据包是被禁用协议,则直接将该包丢弃。

在整个流量控制系统中,流量分类器起着最关键的作用,它是后续模块的基础;队列管理器收到不同的数据包后,通过不同的队列调度算法,分配相应的通道带宽,并对关键业务分配保证带宽,保障其网络业务正常进行;流量整形是调整数据传输的平均速率,是数据按照传输模式规定的速率进行传输,尽量避免突发性通信量导致的拥塞问题,主要采用的算法有令牌桶算法;流量检测器能够对数据包的识别、数据包的传输进行监测分析,实时生成图表和报表,供管理员参考。

二、开发过程

1.非形式的规范。一个数据包(Packet)包含源IP地址SourceIP、目的IP地址DestinationIP、源端口SourcePort、目的端口DestionationPort、协议Protocol、数据Data几部分组成。其中协议分为TCP和UDP。当数据包进入分类器(Filter)后,分类器分别检测数据包的几个组成部分,接着设置(set)数据包的状态(state)、数据通道(pipe),根据检测结果将其发送(send)至队列管理器或直接丢弃(drop)。队列管理器(Queue)首先创建(create)不同的通道带宽(Pipe),接着读取数据包的数据通道的值,将其发送至相应的通道。流量整形器(Flow)最后将数据发送至数据出口。流量检测器(Monitor)用于生成图表(graphic)(如图所示):

2.规约开发。根据非形式规范分别对各个抽象机进行规约描述。下面建立分类器Filter抽象机。Filter抽象机封装了数据包的各种信息,集合PROTOCOL用来保存数据包可能的各种协议,集合STATE用来保存数据包的两种状态,集合PIPE用来保存数据包所要进入的带宽队列(由策略预先制定)。Filter抽象机执行2个操作,drop操作将符合丢弃策略(BlockIP、BlockPort、BlockData)的数据包直接丢弃掉,send操作将其他的数据包转发至队列管理器,并设置该数据包所要进入的带宽pipe,将数据包带宽策略设置为100KB。

MACHINE

Filter(SourceIp,DestinationIp,SourcePort,DestionationPort,Protocol,Data)

SETS

PROTOCOL={tcp,udp}

STATE=[block,pass]

PIPE=[100KB,500KB,1MB]

CONSTANTS

SourceIp∈ipAddress∧

DestinationIp∈ipAddress∧

SourcePort∈NAT∧

SourcePort

DestionationPort∈NAT∧

DestionationPort

Protocol∈PROTOCOL∧

Data∈String

OPERATIONS

d?邝drop=

PRE

state∈STATE

THEN

IF SourceIp∈BlockIP then

state:=block

ELSE IF DestinationIp∈BlockIP then

state:=block

ELSE IF SourcePort∈BlockPort then

state:=block

ELSE IF DestionationPort∈BlockPort then

state:=block

ELSE IF data∈BlockData then

state:=block

END

END;

s?邝send=

PRE

state∈STATE∧

protocol∈PROTOCOL∧

pipe∈PIPE

THEN

IF SourceIp BlockIP∧Pipe=100KB then

state:=passpipe:=100KB

ELSE IF DestinationIp BlockIP∧Pipe=100KB then

state:=passpipe:=100KB

ELSE IF SourcePort BlockPort∧Pipe=100KB then

state:=passpipe:=100KB

ELSE IF DestionationPort BlockPort∧Pipe=100KB then

state:=passpipe:=100KB

ELSE IF data BlockData∧Pipe=100KB then

state:=passpipe:=100KB

END

END

同样可以依次构造队列管理器抽象机Queue、流量整形器抽象机Flow和流量检测器抽象机Monitor。Queue抽象机根据数据包的pipe信息执行create操作,建立相应的带宽通道,数据包通过后将其转发。Flow抽象机create令牌桶操作,令牌桶满后将多余数据包分组到令牌桶外的缓存区排队。Monitor抽象机用来将数据包和其他3个机器搜集来的信息绘制成表格和图表。

3.精化和系统实现。精化是一种用于将软件系统的“抽象模型”(其规范)变换到另一种更具体一些的数学模型(实现)的技术。主要目的是将抽象机经过多次细化,逐步精化精化成一个可以执行的程序,程序的正确性依赖于每一步精化的正确性,最终完成系统实现。在Filter抽象机中,可以对其进一步精化,数据包的data部分我们可以建立特征库,利用模式匹配算法将data中的特征值与特征库进行对比匹配,达到网络应用识别的目的。这一步实现后,接着可以加入时间的因素,有时无法通过一个简单的数据包识别具体的网络应用,这就需要系统要有自动学习功能,通过一段时间的检测分析,判断出具体的网络应用。需要注意的是,在精化的过程中,每个抽象机都要重新进行构造,验证实现的正确性。具体的精化过程在文中不再进行阐述。

提出了利用B方法实现网络流量监控系统的方法。利用B方法进行系统建模,能够充分发挥形式化方法的优点,提高了数据包类型的识别率和系统的稳定性。通过逐步精化和形式化证明,能够验证系统的正确性,生成可执行的系统程序,保证了系统的健壮性、稳定性和可维护性。由于精化过程是个难点也是重点,是生成程序的前提,在该系统下的精化工作还将进一步进行下去。

参考文献

[1]裘宗燕译.B方法.北京:电子工业出版社,2004

[2]Tartanoglu F,Levy N,Issarny V,et al.Using the B Method for the Formalization of Coordinated Atomic Actions[J].Computing and Informatics,2004 (10):103～109

[3]林闯,单志广,任丰原.计算机网络的服务质量(QoS).北京:清华大学出版社,2004:210～226

[4]陈展荣,徐娟,禹智涛.一种基于漏桶算法的模糊流量控制器的设计.广东工业大学学报.2003(1):18～52