Packet Reachability Verification in OpenFlow Networks
Packet Reachability Verification in OpenFlow Networks
复制标题
OpenFlow 网络中的数据包可达性验证
DOI：
10.1145/3384544.3384573
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Sugiyama Keigo
中科院分区：
文献类型：
--
作者：
Yoshiura Noriaki;Sugiyama Keigo
OpenFlow是一种能够集中控制网络设备、实现复杂的数据包转发、灵活改变网络拓扑结构的网络技术。在OpenFlow网络中，网络设备分为OpenFlow交换机和OpenFlow控制器。OpenFlow网络由OpenFlow控制器中的程序配置。NetCore是OpenFlow的编程语言之一，用于函数式编程语言Haskell。Haskell中的程序可以在Coq中验证，Coq是一个正式的证明管理系统。针对NetCore，提出了一种OpenFlow网络的验证方法。在该方法中，必须手动以逻辑形式描述所验证的属性。提出了一种通过自动生成可达性验证逻辑公式来自动验证数据包可达性的方法。本文还通过实验对所提出的方法进行了评价。
OpenFlow is a network technology that enables to control network equipment centrally, to realize complicated forwarding of packets and to change network topologies flexibly. In OpenFlow networks, network equipment is separated into OpenFlow switches and OpenFlow controllers. OpenFlow networks are configured by programs in OpenFlow controllers. NetCore is one of programming languages for OpenFlow and is used in functional programming language Haskell. Programs in Haskell may be verified in Coq which is a formal proof management system. For NetCore, a method which verifies OpenFlow networks was proposed. In the method, the properties that are verified must be described in logic manually. This paper proposes a method of automatic verification of packet reachability by automatically generating logical formulas for reachability verification. This paper also evaluates the proposed method by experiment.