基于FSM模型檢驗(yàn)的安全測試技術(shù)研究.pdf

1、隨著計(jì)算機(jī)技術(shù)的不斷發(fā)展，計(jì)算機(jī)軟硬件系統(tǒng)已經(jīng)深入滲透到實(shí)際生活中的各個(gè)領(lǐng)域，若這些系統(tǒng)一旦出錯(cuò)，將給人類帶來不可承受的損失，所以，安全問題已經(jīng)逐漸成為人們的重點(diǎn)關(guān)注對象，但隨著功能逐漸強(qiáng)大、設(shè)計(jì)日益復(fù)雜的發(fā)展，如何降低這些目標(biāo)系統(tǒng)的測試成本也逐漸成為人們有待解決的難題，目前為止，人們已經(jīng)研究出了很多種安全測試方法，比如形式化安全測試、基于模型的安全測試方法、基于故障注入的安全測試、威脅模型和攻擊樹理論、基于風(fēng)險(xiǎn)的安全測試、模糊測試(F

2、uzzTesting)、基于屬性的安全測試和基于白盒的安全測試方法等，在各種安全測試方法中，形式化的模型檢測算法被證明是一種有效的可靠性和正確性的安全測試方法，不僅能夠有效降低目標(biāo)系統(tǒng)安全測試成本，而且能有效定位系統(tǒng)安全威脅，而有限狀態(tài)機(jī)模型可以很好的為各種軟硬件系統(tǒng)建立狀態(tài)遷移系統(tǒng)，被廣泛應(yīng)用到實(shí)際應(yīng)用中，具有深厚的理論基礎(chǔ)，本文利用有限狀態(tài)機(jī)理論，首先通過研究目標(biāo)系統(tǒng)建立狀態(tài)機(jī)模型，隨后在此基礎(chǔ)上用形式化公式表示其安全屬性模型，然后

3、通過判斷系統(tǒng)模型是否符合安全屬性來驗(yàn)證分析目標(biāo)系統(tǒng)的安全性。主要的研究工作包括:
　　 首先，通過對有限狀態(tài)機(jī)理論的研究，來為目標(biāo)系統(tǒng)建立狀態(tài)遷移系統(tǒng)模型，介紹了幾種如何解決狀態(tài)爆炸的算法原理，并提出一種基于模型分解的解決狀態(tài)爆炸問題的方法，為狀態(tài)爆炸問題的研究提供一種理論參考;
　　 然后，研究故障樹模型分析法理論和其時(shí)序邏輯形式化方法，在故障樹模型的基礎(chǔ)上加入時(shí)序邏輯門，方便利用故障樹理論來生成時(shí)序邏輯公式，此方法有

4、助于形式化的描述模型的安全屬性;
　　 最后，通過研究各種安全測試方法和測試工具的特點(diǎn)，選擇合適的工具來進(jìn)行形式化的安全測試，通過AB協(xié)議的仿真實(shí)驗(yàn)過程來證明本文提出的安全測試方法的有效性。
　　 本文的創(chuàng)新點(diǎn)在于給出了一種解決狀態(tài)機(jī)模型狀態(tài)爆炸問題的理論基礎(chǔ)與算法過程，并利用故障樹的時(shí)序邏輯化來建立安全屬性規(guī)范，用CTL公式來描述安全屬性規(guī)范，通過將有限狀態(tài)機(jī)模型和故障樹模型的結(jié)合，給出了一種有效的安全測試方法，并用實(shí)