Research On Reliability Verification System Of Cloud Network Data Plane

The cloud computing has experienced birth,development and accelerated explosion in recent ten years.And the cloud computing platform represented by Alibaba Cloud,Huawei Cloud and Tencent Cloud has already become new public infrastructure to be penetrated into various aspects of economic development and social life,changing people’s daily life imperceptibly.Moreover,the network that connects cloud and cloud,cloud and users plays a vital and irreplaceable role in cloud computing.To guarantee network stability and reliability has become a top priority to maintain smooth running of cloud service.However,the recently disclosed series of fault reports pointed out that network failure is one of the chief culprits of cloud service interruption.Various cloud providers have taken active measures to make all efforts in preventing the stability risks to cloud service caused by network failure.Large cloud providers usually operate private WAN all over the world.Therefore,how to guarantee security and reliability of private network when accelerating the expansion of business scale has become a necessary topic for various cloud providers.As an important link to improve large scale network stability,network verification is bound to make crucial contributions to improvement of stability of cloud service.Different from traditional means,such as network monitoring and network testing,network verification conducts accurate modeling on network via formal methods,whose rigorous logical reasoning guarantees correctness of network behaviors to form a favorable complementary relation with traditional means(those three are irreplaceable).This thesis started from practical problems confronted by some domestic cloud providers during operation of private WAN to study the network verification system and explore its self validating.The specific research contents could be divided into the following three parts:1)Verification and synthesis of data plane configuration ACL is a typical representation of data plane configuration.In the view of cloud providers,the WAN ACL play an important role in guaranteeing network’s connectivity,security and reliability.However,the increasing complexity also bring new challenges to operators.The WAN ACL is frequently changed and error-prone.And the errors will lead to service interruption or bring some hidden troubles to further pose a serious threat on stability of cloud service.In order to solve this problem,we designed and implemented a set of automatic update system for WAN ACL.Operators only need to provide the update intent,and the system will generate a reliable update plan automatically and efficiently.This system has been launched in the industrial circle and applied in routine ACL update management for over two years,which not only improves operators’ working efficiency,but detects ACL update risks for many times.All in all,this system has provided powerful guarantee for stability of WAN.2)Joint verification of programmable data plane configuration and program In order to allow end users to enjoy high-speed network service at low cost,cloud providers operate a large number of edge network nodes and use programmable switches to further decrease operation cost.However,the deployment of programmable switches also bring additional stability risks for edge networks.Different from tradition data plane,the packet processing logic in programmable data plane can be programmed by domain specific language.With the gradually improved degree of network function integration,the reliability of switches is confronted with more serious challenges.In order to guarantee that data plane behavior meets expectation logically,we designed and implemented a set of formal verification system for programmable networks,which verifies the configuration and program in a joint manner.This system can verify programmable networks within several minutes and locate bugs accurately in regards with most of tasks.It has been launched in the industrial circle for half a year,which can detect many hidden bugs for programmable switches so as to provide powerful guarantee for stability of edge networks.3)Self validation of data plane verification system The bugs of the data plane verifi-cation system will result in false positives and false negatives in the implementation process,of which false negatives are often extremely concealed.If the verification system fails to detect the violation against expectation,operators and developers are not able to find the problem,which may bring hidden troubles to the reliability of the network.Thus,we designed and implemented the self validating mechanism for the network verification system,which has been applied in the routine validation of the ACL update system and the programmable network verification system.The experiment showed that this mechanism can not only detect false positives of verification systems,but discover much subtler false negatives.In conclusion,this mechanism can improve reliability of verification systems effectively.