C程序靜態(tài)分析與錯(cuò)誤檢測.pdf

1、隨著計(jì)算機(jī)技術(shù)的快速發(fā)展和普及，軟件系統(tǒng)已經(jīng)成為這個(gè)社會(huì)不可缺少的一部分。與此同時(shí)，軟件質(zhì)量的問題也日益突出，特別的，對于用C語言編寫的軟件，其中一部分是應(yīng)用于安全攸關(guān)的領(lǐng)域如銀行、航天、航空等，一個(gè)軟件錯(cuò)誤就可能引起災(zāi)難性的后果。
　　靜態(tài)程序分析是提高軟件質(zhì)量的一種有效手段，然而靜態(tài)分析工具在對實(shí)際程序分析時(shí)會(huì)產(chǎn)生一定的誤報(bào)和漏報(bào)，前者導(dǎo)致耗費(fèi)大量的精力在錯(cuò)誤報(bào)告的手工確認(rèn)上，后者則導(dǎo)致無法發(fā)現(xiàn)潛在的程序錯(cuò)誤，這兩個(gè)問題是限制

2、靜態(tài)分析工具在實(shí)際中廣泛使用的主要原因。而誤報(bào)和漏報(bào)的產(chǎn)生的根源在于靜態(tài)分析的精確性和可伸縮性。
　　本文圍繞靜態(tài)分析工具的精確性和可伸縮性開展了如下研究工作:
　　C程序內(nèi)存泄漏檢測:內(nèi)存泄漏是C程序中常見的編程錯(cuò)誤，特別對于需要長時(shí)間運(yùn)行的服務(wù)端軟件，內(nèi)存泄漏會(huì)導(dǎo)致服務(wù)端軟件運(yùn)行性能下降，甚至崩潰。學(xué)術(shù)界已提出多種基于靜態(tài)分析的檢測方法，但是這些方法對程序做了一定程度的抽象，導(dǎo)致精度丟失，從而增加了分析的誤報(bào)率和漏報(bào)率。

3、針對該問題，本文提出了一個(gè)內(nèi)存狀態(tài)轉(zhuǎn)移模型用于檢測程序的內(nèi)存泄漏，該模型相比其他方法能夠更為全面地捕捉動(dòng)態(tài)內(nèi)存在程序分析過程中的狀態(tài)變化。為了支持跨過程分析，本文還提出了一種更精確的函數(shù)摘要的表示方法，相比于內(nèi)聯(lián)的方法既保持了一定的分析精度又提高了分析的速度。該方法已實(shí)現(xiàn)在一個(gè)原型工具M(jìn)elton中。通過實(shí)驗(yàn)，Melton在多個(gè)使用廣泛的開源軟件（如OpenSSH）中找到了數(shù)十個(gè)之前未被發(fā)現(xiàn)的內(nèi)存泄漏，并得到開發(fā)者的確認(rèn)和修復(fù)。

4、　　支持多錯(cuò)誤檢測的靜態(tài)分析框架:本文提出了一個(gè)支持多種程序錯(cuò)誤檢測的靜態(tài)分析框架，并實(shí)現(xiàn)了一個(gè)靜態(tài)分析工具Canalyze。Canalyze在對實(shí)際程序分析的過程中找到了上百個(gè)之前尚未被發(fā)現(xiàn)的程序錯(cuò)誤，并得到開發(fā)者的確認(rèn)。另外，為了提高靜態(tài)分析工具Canalyze的可伸縮性，提出了一種精確的基于函數(shù)摘要的分析方法，并實(shí)現(xiàn)在工具Canalyze中，與基于函數(shù)內(nèi)聯(lián)的方法比較提高了2到3倍的分析速度。
　　面向符號(hào)執(zhí)行的約束求解優(yōu)化:

5、符號(hào)執(zhí)行一般采用SMT(Satisfiability Modulo Theories)求解器進(jìn)行約束求解，然而SMT求解器的求解時(shí)間代價(jià)過高。針對該問題，本文提出了一個(gè)輕量級(jí)的基于賦值重用和后驗(yàn)證的約束求解框架。賦值重用是在符號(hào)分析的過程中重用歷史求解過的約束集的可滿足賦值，來加快當(dāng)前的求解過程;后驗(yàn)證方法則是采用一個(gè)輕量級(jí)的求解器求解程序中的約束，然后再采用SMT求解器對可疑的路徑進(jìn)行后驗(yàn)證。這些優(yōu)化策略在保持求解精度的情況下，提升了