Research On Network Configuration Verification Method Based On Formal Method

With the acceleration of the global informatization process and the rapid growth of network services,the scale of the network has shown an exponential expansion,and the structure of the network has become more and more complex and diverse.The difficulty and risk of network configuration settings have also increased.Currently,network configuration errors have become one of the main causes of frequent network failures and service interruptions.Network formal verification is an important means to ensure the correct operation of network.Since it was proposed,many scholars have carried out formal verification work at different levels for different types of networks.However,existing work suffers from the following problems:1.In terms of verification methods,most of the existing verification work adopts the method of two global verifications to deal with the verification of network configuration updates,although the verification efficiency of this method is low and the computational overhead is high.The current incremental verification method has problems such as low scalability and difficulty in configuration input,so it is not used by the industry.2.In terms of the type of verification network,the existing verification work only focuses on routing and switching networks or pure software-defined networks,while ignoring one of the main application scenarios of software-defined networks: hybrid multidomain software-defined networks.The hybrid multi-domain software-defined network is a network that includes routing and switching devices and software-defined network devices.This scenario involves the management of policies in multiple different network domains,which brings challenges to formal verification work.Aiming at the verification problem in the configuration update scenario,this paper conducts research on fast verification of configuration updates,and proposes a fast network configuration update verification method based on forwarding information table comparison.In this paper,a formal method is used to construct the network data flow as the flow model,and the forwarding information table items are combined with the network topology to construct the graph model.The specific forwarding path of the packet in the network is abstractly expressed through these two proposed models.This paper discusses the impact of different configuration segment updates on the forwarding information table of the forwarding device,and determines the scheme that needs to be re-verified according to the different attributes to be verified.Combining the content proposed above,this paper proposes a verification algorithm Fast CUV for the configuration update scenario.It analyzes the difference in the forwarding information table through the network snapshots generated by the configuration information before and after the network configuration update and then finds the violation of the forwarding attribute after the configuration update,finally finishes fast verification of network configuration updates.Aiming at the verification problem of hybrid multi-domain software defined network,this paper studies the forwarding policy verification method of hybrid multi-domain software defined network,and proposes a hybrid multi-domain software defined network forwarding policy verification method based on graph algorithm.In this paper,considering the characteristics of hybrid multi-domain software defined networks,a general formal model HM-SDN is designed to describe hybrid multi-domain software defined networks.This model implements the description of hybrid multi domain software defined networks from aspects such as topology,forwarding paths,policies,etc.In order to facilitate the verification process of the proposed model,this paper constructs a software defined network information graph SDNIG according to HM-SDN,which is a data structure on which a hybrid multi-domain software-defined network based on a graph algorithm is implemented.The design of forwarding policy verification algorithm VeriGraph realizes the verification of various forwarding policies.The experimental results show that the fast network configuration update verification method proposed in this paper can efficiently achieve verification of network configuration updates in large-scale network environments when the number of configuration update rows is few.At the same time,the hybrid multi domain software defined network forwarding policy verification method can complete verification work on different network topologies.