基于符號執(zhí)行的代碼靜態(tài)檢測方法研究與實現(xiàn).pdf

1、隨著軟件技術(shù)的普及發(fā)展，軟件系統(tǒng)被應(yīng)用到我們生活的各個方面，在帶來極大便利的同時我們也承受著由軟件漏洞所帶來的巨大風(fēng)險。如何有效的保證軟件質(zhì)量是一個極為迫切的需求。在保證軟件質(zhì)量的方法中有兩大類，前期可以通過靜態(tài)分析源代碼盡早發(fā)現(xiàn)潛在漏洞；后期可以動態(tài)運(yùn)行二進(jìn)制代碼分析實際運(yùn)行結(jié)果。程序的漏洞越早發(fā)現(xiàn)其修改成本越小，所以程序靜態(tài)分析是一種重要的軟件質(zhì)量保證方法。在眾多的靜態(tài)分析方法中，符號執(zhí)行以其高度的精確性獲得了極大關(guān)注。
　　

2、符號執(zhí)行是一種路徑敏感上下文相關(guān)的分析方法，在計算資源足夠充分的情況下它可以對程序進(jìn)行非常精確地分析，從而發(fā)現(xiàn)一些細(xì)微的漏洞。然而符號執(zhí)行理論本身也面臨著幾大難題，其中包括路徑爆炸、約束求解和內(nèi)存模型。
　　論文首先對近三十年來符號執(zhí)行技術(shù)的發(fā)展進(jìn)行了概述，討論了符號執(zhí)行的基本原理和近年提出的一些改進(jìn)方法。這些改進(jìn)包括：在測試數(shù)據(jù)生成方面提出了動態(tài)符號執(zhí)行，它是一種結(jié)合具體值和符號值的方法；在路徑爆炸抑制方面提出一些啟發(fā)式搜索策略

3、；在約束求解方面主要提出了無關(guān)約束消除和增量式求解。本文緊接著分析討論了一種非常強(qiáng)大的中間語言LLVM IR，對其語法構(gòu)成、數(shù)據(jù)類型及指令集做了分析，并對其數(shù)據(jù)類型和指令集進(jìn)行了形式化描述。本文隨后對符號執(zhí)行中內(nèi)存模型展開了討論，對比了當(dāng)下符號執(zhí)行理論中各種主流內(nèi)存模型（名字值模型、數(shù)組模型和基于區(qū)域的三元組模型）的優(yōu)缺點，并提出一種樹狀結(jié)構(gòu)的內(nèi)存模型TMM（Tree-memory model）。這種內(nèi)存模型的核心思想是以樹狀結(jié)構(gòu)來表示