Research On Intrusion Detection Method And Application Based On Linear Model Checking

With the change of network technology,the network structure becomes more complex,and the network faces more and more risks.Intrusion Detection,as an important means to protect network security,has become an essential security measure.Model Checking(MC)is an automatic verification technique that is used in communication protocols,control systems,and intrusion detection in recent years.Intrusion detection based on model checking has the advantages of strong scalability,low false positive rate and accurate identification of known attacks.However,with the development and evolution of attack means and the increasing complexity of application space in recent years,the problem of alarm leakage rate increases.At the same time,with the increase of network traffic and the increasing complexity of network structure,the problem of state space explosion of model checking itself becomes more serious,which leads to the problem of slow response and difficult to ensure real-time performance.Aiming at these problems,this paper explores the shortcomings of existing Model Checking,and combines Linear Model Checking(LMC)to establish a model.The specific research contents are as follows:(1)For existing intrusion detection based on model checking,the complexity of behavior atomization sequence and high complexity of model space lead to high alarm leakage rate and long detection response time.In this paper,an intrusion detection method based on linear model checking is proposed,which reduces the spatial complexity of the model and prolongs the linear sequence length of detection.Meanwhile,based on the description capability of linear model checking,two high-frequency attacks,Scanning Attack and Denial of Service Attack,are described.Experiments show that linear model checking effectively reduces the alarm leakage rate and response time of high-frequency attacks.(2)For detecting persistent attacks,there are problems such as high alarm leakage rate,long response time and large state space.This paper proposes a method of Divide and Conquer Approach(DCA)combined with linear model checking.The detection model was constructed by the sequential logic formula,and the detection model was divided into several sub-models by the decomposition strategy.The verification results of the whole model were obtained by combining the inspection results of different sub-models.This method is used to establish a detection model for two kinds of persistent attacks,namely,claim attack and remote user attack.Experiments show that,compared with the current model checking methods,this method reduces the alarm failure rate and response time of persistent attacks,reduces the state space,and alleviates the problem of state space explosion.