Buffer Overflow Vulnerabilities Detection System Based On Constraint System Model

Software safety detecting is playing an important way to protect Computer System and avoid being attacted, depending on Static Analysis's excellences such as higher automatization, researching the technologies of Static Analysis is very important.Aiming at Buffer Overflow Vulnerability, this paper has researched its base principle, and combined constraint analysis and model checking technology which have been applied in detecting BOVs sepatately, through following analysis to insert information as buffer attributes initialization,attributes transfer and attributes assert,then has constructed buffer Attributes constraint system, and adopted model checking technology to solve constraint system in order to detect BOVs among c programs.For the problem of constraint analysis'accuracy, this paper has brought forward alias analysis algorithm during process based on GCC Abstract Syntax Tree, by pointer variable analysis this algorithm has generated alias information assemble, and has finished the exchange mapping between assemble element attributes and attributes of alias buffer information, so the accuracy is increased effectively.Based on the analysis of pivotal technology above, this paper has designed a prototype system to detect BOVs based on constraint system model checking, the testing result shows that this prototype system can discover typical known vulnerabilities,and for unknown vulnerabilities this system aslo can locate effectively.