基于模型檢驗(yàn)的軟件安全靜態(tài)分析研究

軟件安全靜態(tài)分析是檢測軟件安全漏洞的一種手段。本文在總結(jié)現(xiàn)有的軟件安全靜
態(tài)分析方法的基礎(chǔ)上，將在硬件設(shè)計(jì)領(lǐng)域得到成功應(yīng)用的模型檢驗(yàn)方法引入到軟件產(chǎn)品的檢驗(yàn)中，給出了一種基于自動(dòng)機(jī)理論的檢測軟件安全的模型檢驗(yàn)方法，闡述了其原理和工作流程，并用實(shí)例進(jìn)行了驗(yàn)證說明。
隨著計(jì)算機(jī)系統(tǒng)廣泛應(yīng)用，系統(tǒng)安全性越來越得到重視。軟件安全漏洞是現(xiàn)代計(jì)算機(jī)
系統(tǒng)的毒瘤，多數(shù)惡意攻擊都源自軟件產(chǎn)品各種各樣的漏洞。由于安全漏洞具有相當(dāng)?shù)碾[蔽性，如何檢測軟件中可能存在的安全漏洞已成為信息安全關(guān)注的焦點(diǎn)。目前對于軟件漏洞檢測的研究有靜態(tài)分析和動(dòng)態(tài)檢測兩個(gè)分支，其中靜態(tài)分析是主要的研究方向。靜態(tài)分析通過對源代碼的掃描和分析來檢測漏洞，不需要改動(dòng)源代碼；動(dòng)態(tài)檢測則通過在程序執(zhí)行期間對內(nèi)存和堆棧的監(jiān)測來檢測漏洞，需要添加并重新編譯源代碼，增加了系統(tǒng)開銷[1]。
模型檢驗(yàn)是一種重要的自動(dòng)化驗(yàn)證方法，它最早由 Clarke 和Emerson 提出[2]，主要通
過顯式狀態(tài)搜索或隱式不動(dòng)點(diǎn)計(jì)算來驗(yàn)證系統(tǒng)的有窮狀態(tài)和命題性質(zhì)。模型檢驗(yàn)在硬件設(shè)計(jì)領(lǐng)域的應(yīng)用已經(jīng)比較成熟，在軟件安全靜態(tài)分析上的應(yīng)用也有研究人員進(jìn)行了一些有意義的探索，如基于進(jìn)程演算的模型檢驗(yàn)方法[3]、基于程序時(shí)序邏輯的模型檢驗(yàn)方法[4]等等。
軟件安全靜態(tài)分析的難點(diǎn)在于如何定義程序的安全屬性以及如何制定對源代碼的約束
條件。為了能夠更好的描述程序的安全屬性并運(yùn)用某種形式化的方法對其進(jìn)行驗(yàn)證，本文基于自動(dòng)機(jī)的相關(guān)理論，通過將軟件的源代碼和安全屬性分別建模為相應(yīng)的自動(dòng)機(jī)模型，探討了一種檢測軟件安全的模型檢驗(yàn)方法。