Research On Detection Method For Vulnerabilities In Open-source Software Based On Model Checking

Nowadays,with the explosion of open-source software,the number of users that make use of open-source software is growing bigger and bigger,and the application fields that open-source software involves are becoming more and more.Thus,people cannot help to pay much attention on the safety issue of open-source software.In this age that open-source software is known as unsafe with lots of vulnerabilities,the study about vulnerability detection on open-source software has become the hotspot in software detection area.In this paper,we aim at finding an automatic detection method for vulnerabilities in open-source software,which can both expand the detectable vulnerabilities set and improve the detection efficiency.Model checking is an effective formal method for vulnerability detection.Model checking is able to detect vulnerabilities from software's source code,it is not only an automatic detection method,but also a precise one.Thus,model checking theory is very much worth studying for its high practicability.In this thesis,we concluded the most useful methods and software that commonly used in open-source software detection,and analyzed the researches about model checking theory in open-source software.Furthermore,we proposed a vulnerability detection method in open-source software based on model checking theory.The method is based on a newly come-up theory of conditional model checking recent years.Firstly,conditional model checking theory combines two or more model checking algorithms together in serial form,and by this means,the failure times of model checker could be decreased,what's more,the detectable vulnerabilities set could be expanded.Secondly,we analyzed the model checker CPAChecker deeply into its architecture and core algorithms,besides,we provided the formal description and algorithm flow of configurable program analysis.Based on configurable program analysis framework,conditional model checking method could be executed automatically,and by this means,the efficiency of model checking method could be improved.Finally,we made an experiment on open-source Web server,Tomcat.The results of conditional model checking on Tomcat show that,besides the vulnerabilities that other detection methods can detect,our conditional model checking can discover the vulnerabilities that other methods cannot find.