Research On Formal Verification And Application Technology Of Network Security Protocol Based On Reinforcement Learning

Formal verification uses mathematical methods to prove the completeness of the system.The current formal verification has been successfully used to find design flaws in many security protocols,and many design flaws have been discovered.But the existing formal verification methods are mainly manual verification and semi-automated verification.Because of the memory explosion caused by the excessive state space of protocol,the automatic verification of network security protocol is still a challenge.In this paper,the author proposes a general framework that can automate the verification protocol.We use a dynamic strategy method to assist formal verification tools to intelligently search paths on the theorem tree.Compared with existing static strategies,this method is more flexible and does not require human learning costs.After training,the dynamic strategy can automatically optimize the neural network according to the protocol,and it does not need artificial assistance,which improves the probability of successful verification.In order to verify the proposed framework,this paper formalized the verification of several popular network security protocols.In order to solve the token contract to verify the contract quantity and require higher security level of validation,this paper proposes a scrip formal modeling method of token contracts and five on integer overflow vulnerability of token modeling,and use the formal verification,automatic validation framework proposed in this paper a successful and efficient to find the existence of integer overflow vulnerability.The design idea of this strategy is:When performing a random path search in the theorem tree,if the lemma represented by a node in the theorem tree is not on the correct path,we should give it a lower weight.Therefore,we introduce a reinforcement learning algorithm DQN(Deep Q Network)to implement this strategy.The formal modeling method of token contract proposed in this paper needs to model a series of logic codes of the program first,and then use the calculus method to prove whether its security attributes are satisfied or destroyed.The main tasks carried out are:1.In order to enable the neural network in reinforcement learning to learn the formal verification logic,this paper designs a formal data extraction technology.This technology prunes the intermediate theorem automatically generated by the verification tool,extracts corresponding logical statements to simplify the description verification process,and solves the problem that the existing formal verification data is difficult to directly interact with the neural network.And the storage structure of the theorem tree is constructed.By pruning the redundant data and using neural networks to assist the recursive construction of the theorem tree,the problem that the theorem tree is easy to cause state space explosion is solved.In order to arrange the extracted data according to its expressed logical semantics and facilitate interaction with neural networks,this paper constructs a theorem tree storage structure.There are an infinite number of conversation protocols in the theorem tree.By pruning redundant data and using neural network to assist the construction of the theorem tree recursively,the problem of state space explosion easily caused by the storage of the theorem tree is solved.2.In order to solve the problem that supervised learning and unsupervised learning algorithms are difficult to train due to lack of data set,this paper introduces DQN neural network in reinforcement learning to formal verification,and proposes a method of feature vector extraction and algorithm of judgment cycle detection.It improves the universality of neural network and the success rate of path selection.Compared with the supervised learning method,this method does not need to provide data sets for neural network training.3.In order to demonstrate the application scenario of the automatic formalized validation framework proposed in this paper,and to solve the security problems in the token contract,a formalized modeling method for token contract is proposed in this paper.The logic code of the token contract is modeled to analyze whether its security properties are satisfied or broken.Through the automated validation framework in this paper,the existing vulnerabilities are found successfully and efficiently.