Research Of Software Security Analysis Based On Model Checking

At the present time, the quality and the security of software impact more and more on the security of computer system and network, and the problem of software security has become more and more serious. Research on software security is gradually rewarded much attention throughout the world, but there isn't a mature and practical approach yet. Model checking is a kind of formal verifying technology. This technology is widely used in verifying field of sequential circuit design and communication protocol design. However, model checking in software verifying and security analysis is still under research. Model checking can efficiently and fully automated analysis the security of the software, so it has good prospect for developmen in softeware security field. This paper analyzes the reason why the problem of software security become more and more serious, and the relation between security and vulnerability of software. The development trend that software becomes interconnective, scalable and complex, makes great influence on this software security problem. And with the increasing software vulnerabilities, the software security problems will also increase. This paper introduces the basic concept and the development state of model checking. According to the process of model checking, the techniques used in the three main steps, system modeling, property modeling and model checking algorithm, are introduced. Considering the characteristic of software model checking, the technology and methods to solve the state space explosion problem are introduced too. This paper analyzes the formal methord in MOPS, and presents some assumptions to improve MOPS' deficiencies. A general method to design security properties is given in this paper. Using this proposed method, this paper goes through three steps, proposing security properties, determining FSA states and determining FSA state transition rules, to design and model two security properties. Finally, this paper analyzes the security of the target program, and successfully finds out the security risk in the program.