Research On Model Checking Technology Of Software Vulnerability

As the importance of information security has become increasingly prominent, effective solution to the security problems that exist in information system software have become increasingly urgent demand. Explore, analysis, protection and use of software vulnerabilities is being more and more attention. As a kind of formal method, model checking can be correct, efficient and completely in identifying specific types of software Vulnerabilities. Based on the analysis of the existing technology of software model checking, this paper describes a framework of the vulnerability detection model for c source code and realizes a model checking software called be MCS.The basic idea of the model framework is to model program to a pushdown automaton (PDA), to represents security attributes to a finite-state automaton (FSA). Safety attribute refers to wrong operation sequence that violates safe programming rules. Then it uses model checking techniques to identify whether any state of FSA is reachable in the PDA. That means to verify whether the wrong operation sequence of FSA exists in all possible operation sequences of PDA. The main advantage of this approach lies in its ability to fully verifying the existence of certain types of vulnerabilities. And it is an efficient and scalable.MCS is a model checking software with C/S architecture. It is an integrated management system that provides functions of vulnerability checking and vulnerability query. The system includes core module and application module. Application Module builds the C/S platform and database. Core module does the actual work of model checking and runs on the server. First, Client uploads files of security attribute and source code to server. Then, Server will complete to check the files and store results into database. Server can also provide query, statistics and other functions for client. Keywords: Model Checking , Vulnerability Dig, Static Analysis, Software Verification...