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

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

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

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

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

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