軟件源代碼安全分析研究.pdf

1、信息系統(tǒng)安全性格局的大變化,將軟件安全性推到關(guān)乎全局的關(guān)鍵位置,安全分析是用于增強(qiáng)系統(tǒng)安全性的有效手段之一。由于設(shè)計(jì)階段所形成的安全規(guī)范與編程規(guī)范通常較清晰地反映在源代碼中,因此通過(guò)軟件源代碼安全分析方法自動(dòng)檢測(cè)系統(tǒng)中存在的安全漏洞具有重要意義。
　　 本文在對(duì)軟件安全漏洞分類及相關(guān)軟件安全分析技術(shù)研究的基礎(chǔ)上,提出并實(shí)現(xiàn)了用于軟件安全分析的編譯器基礎(chǔ)架構(gòu)；采用自上而下的分析方法實(shí)現(xiàn)了程序語(yǔ)義分析,引入了類型系統(tǒng)形式化方法及基于

2、自動(dòng)機(jī)的定制安全分析手段,實(shí)現(xiàn)了典型安全漏洞的自動(dòng)檢測(cè)。論文研究的具體內(nèi)容包括:
　　 (1)用于軟件安全分析的編譯器基礎(chǔ)架構(gòu)本文將傳統(tǒng)用于編譯器開發(fā)的編譯器基礎(chǔ)架構(gòu)引入軟件安全分析,提出了針對(duì)安全分析的基礎(chǔ)架構(gòu)模型。采用開放編譯器工具ANTLR構(gòu)造了C/C++與Java語(yǔ)言語(yǔ)法分析前端,為程序設(shè)計(jì)語(yǔ)言源代碼構(gòu)建完整的中間表示,引入了專用的程序基本語(yǔ)義信息收集層次,為安全分析提供了較為準(zhǔn)確的程序語(yǔ)義信息,形成了一種支持全分析階段

3、安全檢查及多種分析手段的軟件源代碼安全分析方法。
　　 (2)基于二叉決策圖的指針別名分析本文提出并實(shí)現(xiàn)了一種基于二叉決策圖的流敏感、上下文敏感及路徑敏感的指針別名分析方法,實(shí)現(xiàn)了更為準(zhǔn)確的指針別名信息抽??；基于自上而下的分析方法,提出了包括記憶式跨過(guò)程分析、路徑數(shù)爆炸優(yōu)化、結(jié)點(diǎn)重復(fù)分析優(yōu)化以及不可達(dá)路徑檢測(cè)在內(nèi)的組合優(yōu)化方法,有效解決了敏感分析中的效率問(wèn)題。
　　 (3)語(yǔ)義類型系統(tǒng)的形式化方法本文提出了一種面向安全分

4、析的輕量級(jí)語(yǔ)義類型系統(tǒng),以狀態(tài)集合為依據(jù)給出了語(yǔ)義類型的定義,提出了包含類型推導(dǎo)規(guī)則與安全規(guī)范斷言集合在內(nèi)的語(yǔ)義類型系統(tǒng)模型,并以指針相關(guān)安全分析為例詳細(xì)闡述了語(yǔ)義類型系統(tǒng)的構(gòu)造方法。該類型系統(tǒng)為軟件代碼安全分析提供了統(tǒng)一的形式化模型,可直接應(yīng)用于程序狀態(tài)相關(guān)的軟件安全漏洞檢測(cè)。
　　 (4)基于自動(dòng)機(jī)的定制化安全分析在語(yǔ)義類型系統(tǒng)模型及典型安全漏洞源代碼模式分析的基礎(chǔ)上,本文提出了一種基于自動(dòng)機(jī)模型的定制化安全分析方法,在傳統(tǒng)

5、自動(dòng)機(jī)模型的基礎(chǔ)上,引入了語(yǔ)義約束及分支條件等新的狀態(tài)轉(zhuǎn)移約束,滿足了復(fù)雜安全規(guī)則描述的需要；討論了安全分析過(guò)程中詳細(xì)的模式匹配及狀態(tài)轉(zhuǎn)移處理規(guī)則；并給出了一種基于靜態(tài)報(bào)告安全漏洞的動(dòng)態(tài)植入監(jiān)測(cè)方法。
　　 (5)基于逆向迭代搜索的隱通道檢測(cè)針對(duì)軟件源代碼中的隱通道安全漏洞,本文提出了一種專用的基于信息流圖逆向迭代搜索的隱通道自動(dòng)檢測(cè)方法,采用完整語(yǔ)法與語(yǔ)義分析手段完成原始信息流提取,定義了庫(kù)函數(shù)信息流規(guī)則以及信息流推導(dǎo)規(guī)則,提

6、高了信息流收集的準(zhǔn)確性與完整性；采用基于信息流圖的帶約束逆向深度優(yōu)先搜索算法實(shí)現(xiàn)了潛在隱通道檢測(cè),并通過(guò)語(yǔ)法及語(yǔ)義規(guī)則實(shí)現(xiàn)了偽隱通道的篩選。
　　 論文提出的上述方法嵌入針對(duì)安全分析的編譯器基礎(chǔ)架構(gòu),構(gòu)成了一種準(zhǔn)確性與效率兼顧的軟件源代碼安全分析方法。依托論文工作相關(guān)的科研項(xiàng)目,作者對(duì)論文工作相關(guān)方法與技術(shù)進(jìn)行了實(shí)現(xiàn)及驗(yàn)證,設(shè)計(jì)實(shí)現(xiàn)了相應(yīng)的軟件源代碼安全分析工具,完成了典型安全漏洞的自動(dòng)檢測(cè),通過(guò)了具有測(cè)試資質(zhì)的第三方軟件測(cè)試并