Security Testing Techniques Based On FSM Model Checking

With the continuous development of computer technology, computer hardware and software systems has deeply penetrated into all areas of our life,once the system goes wrong,it will bring us unbearable loss. Therefore, security issues have gradually become people’s first focus, however, with the development of increasingly function and increasingly complex design, how to reduce the target test cost of the target system also gradually become a problem to be solved. So far, people have developed many kinds of security testing methods, such as formal safety Testing, security Testing method based on the model, safety tests based on fault injection, threats and attack tree model theory, a risk-based security Testing, Fuzz Testing (Fuzz Testing), based on the attribute of the safety and security based on white-box Testing method and so on, among all kinds of safety test methods, the formal model was proved to be an effective detection algorithm of reliability and validity of the safety test method, not only can effectively reduce the target system security Testing cost, and effective positioning system security threat, and the finite state machine model can be very good to establish a state transition system for all kinds of hardware and software system, has been widely applied into practice, which has a profound theoretical basis. This paper, by using the finite state machine theory and studying establishing state machine model for the target system, and then use formal formula to express security attribute model of target system, through the judgment of whether system model is in line with the security attribute analysis to verify the target system of security. The main research work includes:First of all, through the study of the finite state machine theory, state transition system model is established for the target system, several algorithms principles of how to solve the state explosion are introduced, and put forward a kind of method based on the model decomposition to solve the problem of state explosion, providing a theoretical reference to the state explosion problem research;Then do some research on the fault tree model theory and its temporal logic formal analysis method, on the basis of the fault tree model, add temporal logic gate, which is convenient to use the theory of fault tree to generate temporal logic formulas, this method helps to formalize security attributes of the description model;Finally, by studying the characteristics of various security testing methods and testing tools, select appropriate tools to conduct the formal safety tests, through AB protocol simulation process to prove the safety testing the effectiveness of the method proposed in this paper.Innovation point of this paper is to provide several theoretical basis of algorithms solving the problem of state machine model’s state explosion, and by using the fault tree of temporal logic to establish requirements for the security properties specification which is described by CTL formula, through the combination of finite state machine model and fault tree model, presents an effective security testing method, and experimental results show this method is highly efficient.