Research On Formal Modeling Verification Method Of Network Security In Industrial Control Systems

Industrial control system(ICS)is a system applied to industrial infrastructure.Common usage scenarios include supervisory control,data acquisition,and industrial automation.The industrial control system contains a variety of different hardware and software,and the system structure is complex throughout the day.The traditional industrial control system is a closed system based on mechanical and electronic equipment only.With the development of network technology,modern industrial control systems use more and more information technology and communication equipment,which increases the complexity and interconnection between systems.At the same time,network security issues related to industrial control systems have also gradually increased.More and more defense methods are applied to industrial control system networks,which greatly improves the security of the system.Formal descriptions related to industrial control systems have become hot spots.The formal method verifies the feasibility and correctness of the logic through accurate mathematical description and abstract system behavior.This article applies the moving target defense method to industrial control systems.Use PAT to establish a time automaton model for the system,and use a formal verification method to analyze and verify the model to evaluate the correctness and security of the method in system application.This article first studies and analyzes the relevant knowledge of the industrial control system and current security defense methods,and applies the moving target defense method to the industrial control system defense.We use PAT to establish a time automaton model for system behavior,attacker,security decision strategy system recovery mechanism after attack,etc.to describe the defense lines of the security defense system.Finally,we chose to use model detection as a formal verification method to perform formal verification analysis on the security properties of system behavior and security defense methods such as deadlock,correctness,reachability and linear sequential logic.The main results of this article are as follows:(1)Use time automata to establish a model for the security model of the mobile target defense industrial control system,simulate the dynamic defense mechanism of the security defense model,and describe the working process of the security model.Compare the number of executives in the mobile target defense and verify that choosing three executives can better balance the accuracy and the efficiency of the system's security defense.(2)Use time automata to build models for single-choice decision strategies and multi-choice decision strategies for mobile target defense.Combining the characteristics of multiple choice decision and single choice decision strategy,a compound choice decision strategy is proposed,and a time automata model is established.This strategy has the advantages of reducing system resource expenditure and increasing the accuracy of decision selection.(3)Write relevant assertion statements for the system,and verify and analyze the system model related to the deadlock algorithm,reachability algorithm,linear time logic algorithm,etc.And the language contains verification methods to verify the attribute mode of the analysis system to evaluate the effectiveness of the mobile target defense applied to the industrial control system.