Mining Method Based On Model Checking Of Software Vulnerabilities

In the cyber-society, information security has become extremely important while more and more security threats occur. Vulnerabilities in information systems are the source of network information security problems. The security flaws are the hidden cancer of modern information systems, for most malice attacks occur because of different kinds of vulnerabilities in software products. One important aspect of the analysis testing the security of the information system is to explore the possible vulnerabilities in the software; therefore, how to detect the vulnerabilities has been especially focused in nowadays information community. Model checking technology is an automated checking technology which is comprehensively used in temporal circuit designing and communication protocol designing and has been a success. It has been just a few years since model checking was brought into software testing and vulnerability detecting. At present, this technology is still under research and has applied in the development of WINXP operating system. Compared with the traditional technologies, model checking technology, as a kind of formal method, can detect and explore specific kind of vulnerabilities in the software correctly, efficiently and completely. It is a hopeful method to improve the quality, especially the security, of the software.This paper firstly discusses the definition of vulnerability and presents one information security vulnerability definition which belongs to our research sphere. Also explored in this paper is the main theme of model checking, its evolution, and the latest research hotspots about this technology. Then, the effort of applying model checking in different phases of software development process is discussed. During the illustration of applying model checking technology into software vulnerability detecting, a vulnerability detecting system model for source code is addressed, and a particular approach of application modeling in source code model checking is proposed. Then the effort of two temporal security property designing and modeling is accomplished, verified with experiments. The tool is applied in real applications, and finally have vulnerabilities successively detected and verified. An analysis and comparison of the popular vulnerability detecting tools which are based on model checking technology is...