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