形狀分析符號執(zhí)行引擎中的狀態(tài)合并.pdf

1、C語言以其對底層機器操控的靈活性，在操作系統(tǒng)、嵌入式軟件、底層驅(qū)動等要求高效的軟件設計領域得到廣泛應用。然而出于靈活性和效率的考慮，C語言賦予程序員對計算機完全掌控的能力同時，犧牲了一定的安全性:非法指針解引用、內(nèi)存泄漏、緩沖區(qū)溢出等內(nèi)存安全問題在C語言程序中尤其突出。
　　提高軟件的可靠性一直是軟件開發(fā)過程中所追求的目標之一。程序動態(tài)測試、程序靜態(tài)分析和程序驗證是目前確保軟件安全質(zhì)量的主要方法。程序驗證作為保證程序正確性的最嚴格

2、的手段，通過形式化方法對程序的各種性質(zhì)給出嚴格的數(shù)學證明，從而保證了程序的可靠性;然而程序驗證目前還未實現(xiàn)自動化證明，需要大量的人工證明，因此未能在工業(yè)界得到廣泛的應用。程序動態(tài)測試的測試結(jié)果依賴于給定的測試集，面對復雜的軟件系統(tǒng)測試集很難做到代碼的高覆蓋率，而且動態(tài)測試的成本和風險較高。程序靜態(tài)分析在程序運行之前對代碼進行分析，可以較早并且低成本地發(fā)現(xiàn)代碼中可能存在的缺陷。
　　符號執(zhí)行技術以其良好的精度控制和代碼覆蓋率，被廣泛

3、用于程序靜態(tài)分析之中。對一個程序進行分析時，符號執(zhí)行引擎以模擬真實的程序執(zhí)行過程的方式，分析程序的數(shù)據(jù)流和控制流信息，并檢查程序執(zhí)行過程中可能出現(xiàn)的所有狀態(tài)，得到程序的分析結(jié)果。高精度和高覆蓋率要求對程序狀態(tài)描述具體而完備，這會導致符號執(zhí)行過程中常見的狀態(tài)爆炸問題，使得符號執(zhí)行技術的可伸縮性（Scalability）較差。筆者所在項目組基于符號執(zhí)行技術實現(xiàn)了一個帶形狀分析功能的C程序分析工具，該工具同樣存在路徑爆炸、可伸縮性較差的問題，

4、本文的主要工作是設計和實現(xiàn)狀態(tài)合并功能及其優(yōu)化，主要貢獻有:
　　針對帶形狀分析的符號執(zhí)行引擎，設計并實現(xiàn)了狀態(tài)合并的算法，這其中主要的難點在于如何確保狀態(tài)合并的引入不會造成程序分析結(jié)果精度的下降，尤其是在引入形狀分析之后，在特定的狀態(tài)抽象規(guī)則之上，如何判定狀態(tài)是否可以合并，以及合并規(guī)則對分析精度的保證。
　　根據(jù)狀態(tài)合并在符號執(zhí)行引擎中的實際效果，考慮約束求解器的求解能力以及求解時間開銷，引入了約束求解器求解代價驅(qū)動的優(yōu)化