The Security Verification Technology For Software Code Based On The Formal Methods

With the rapid development of computer software technology, especially the application in aerospace, transportation, medical and other safety critical fields is used widely, the safety, the reliability of the software system is becoming more and more important, and any mistake may lead to disastrous consequences. Therefore, how to guarantee the safety and reliability of the software system has been paid more and more attention.From design to final implementation of a software system, each link relates to the security of the software, the correctness of the high-level design of the system cannot guarantee the security of code implementation, so only through security authentication of the source code in order to protect the safety of the system. Model checking technology is a kind of automatic verification technology based on formal method, compared with the conventional verification techniques, has the advantages of ambiguity-free, efficient and reliable, in the design of the circuit design and the communication protocol is widely applied. Model checking is only in recent years has been applied to the validation of software systems, compared with the conventional verification technology, has the characteristics of high efficient and reliable. But it was introduced only in the software security field in recent years, especially in the field of software code validation research is not yet mature.This paper first introduces the basis theoretical of model checking technology, the detection process, the development status, and points out that the state space explosion problem in model checking and some solutions. Through the analysis of the storage-centric software component a safety critical system, using model checking tools LLBMC to safety validation. LLBMC as an accurate memory model with bounded model checking tool to formal verifications of memory errors and logic errors of the software module, and the errors have been found can be tracked. Analyzing the two key factors affecting the system state space model and the time of model checking from the breadth and depth, respectively, with the largest number of circular said the maximum breadth, depth of function calls that the depth. We find the breadth is the main factor leading to state space explosion. On this basis, we propose a model-oriented method to determine the State of accessibility in state space, design a State space reduction method based on breadth-first prune and experimentally verify this method can effectively respond to state space explosion problem detection.Finally, in the paper we use a safety critical system software component to verify the state accessibility judgment method, breadth-first pruning method and balance problems. The result indicates that these methods can detect several security vulnerabilities in software code, improve the software systems, especially the reliability of safety-critical systems to provide a solid guarantee.