The Automated Verification Method Of Parametric Protocols Based On Decision Tree

In broad sense,the protocol refers to the network protocol.The function of the protocol is to describe the communication rules of each module.In this paper,protocol narrowly refers to the protocol program described by Guarded Command Language.Parametric protocol is a parameterized protocol,which is the extension form of the protocol.Parametric protocols are widely used,such as mutually exclusive protocols,cache consistency protocols,network security communication protocols and so on.Parametric protocol verification is the process of verifying the logical correctness of parametric protocol.Its purpose is to ensure that the parametric protocol meets the design requirements.The traditional formal verification method of protocol is to verify whether the protocol requirements are valid in each state by enumerating all reachable states of the protocol.However,this method does not work well for the parametric protocol verification.The reasons are divided into two points.First,the parametric protocol has numerous instances,and each instance is equivalent to a protocol.It is very difficult to verify all instances directly.Secondly,the state space of the parametric protocol instances increases exponentially with the increase of parameters,resulting in the state explosion problem,which makes it difficult to verify the large parameter parametric protocol instances.In order to solve the problem that protocol validation methods are difficult to apply to parametric protocol verification,experts of parametric protocol verification put forward their own solutions,such as abstract method,cut-off method,inductive proof method and so on.Among them,inductive proof method is one of the most feasible solutions.However,using inductive proof to verify the parametric protocol requires finding auxiliary invariants.The traditional method of finding auxiliary invariants is manual derivation.This method can only be applied to small-scale parametric protocol.For large-scale parametric protocol,the manual derivation method is not only difficult to implement but also error-prone,which makes it difficult to generalize the inductive proof method.In order to solve the problem of finding auxiliary invariants in inductive proof method,this paper proposes an invariant judgment method based on decision tree,and combines with the existing inductive proof technology of parametric protocol,proposes an automatic verification method of parametric protocol based on decision tree.The automated verification method of parametric protocols based on decision tree is the first method to apply decision tree method to parametric protocol verification.This method can efficiently find auxiliary invariants and complete the inductive proof of the parametric protocol.The automated verification method of parametric protocols based on decision tree includes the following main innovations:(1)A method of using symmetrically reduced reachable state sets with reference protocol instances as training data of decision tree is proposed.Using this training data not only enables decision tree to accurately judge candidate invariants,but also reduces the memory and time required to generate decision tree and to judge candidate invariants.(2)A decision tree algorithm for instance of parametric protocols is proposed.This algorithm is based on ID3 algorithm.By modifying the generating conditions and methods of the leaf nodes,the decision tree contains more information about the instance of the parametric protocols,to ensure that the decision tree can accurately and correctly judge the candidate invariants.(3)A method of judging candidate invariants by decision tree path is proposed.The principle of this method is to use the relationship between the decision tree path and candidate invariants,and use the category of reachable state to judge whether candidate invariants are invariants of parametric protocols.The automated verification method of parametric protocols based on decision tree aims at cache consistency protocol.Experiments show that the automated verification method of parametric protocols based on decision tree can be applied to many typical parametric protocols including Flash protocol.Compared with the ParaVerifier method,it has obvious advantages in time consumption and memory consumption when validating large-scale parametric protocols.