【作者】 陈楠；

【导师】 王震宇；

【作者基本信息】 解放军信息工程大学 ， 计算机应用技术， 2010， 硕士

【摘要】 软件安全检测是保证计算机系统安全、避免遭受恶意攻击的重要技术手段。鉴于静态检测技术自动化程度高、分析速度快等优点,研究静态漏洞检测技术具有重要意义。针对缓冲区溢出漏洞,本文在深入分析其形成机理的基础之上,综合约束分析、模型检测两种技术对程序缓冲区进行跟踪分析,通过在缓冲区操作程序点插入缓冲区属性初始化、属性传递和属性断言等信息,构建了缓冲区属性约束系统,从而采用模型检测技术通过求解约束系统完成程序缓冲区漏洞的检测。针对约束分析的精确性问题,本文提出了基于GCC抽象语法树的过程内别名分析算法,该算法通过指针变量分析生成指针变量的别名信息集合,并完成集合元素属性与互为别名的缓冲区属性信息的变换映射,从而有效地提高了分析精确性。在关键技术研究的基础上,本文设计并实现了基于约束系统模型求解的缓冲区溢出漏洞自动检测原型系统:CodeAnalysis。测试结果表明:该系统能够检测出典型的已知缓冲区溢出漏洞,并且针对未知的缓冲区漏洞,该系统亦能有效地检测并定位。更多还原

【Abstract】 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.更多还原