安全苛求性軟件安全性的形式化分析.pdf

1、隨著信息技術(shù)的飛速發(fā)展，軟件規(guī)模不斷膨脹，系統(tǒng)也越來越復(fù)雜;同時，越來越多的基礎(chǔ)領(lǐng)域都高度依賴于計算機(jī)，如航空航天、電子商務(wù)、遠(yuǎn)程醫(yī)療等。軟件故障可以帶來非常嚴(yán)重的后果，尤其是對于安全苛求系統(tǒng)而言，即使只是一個很小的軟件錯誤都有可能導(dǎo)致整個系統(tǒng)的崩潰，從而導(dǎo)致災(zāi)難性的后果。因此，如何保證軟件的安全性已成為現(xiàn)代軟件技術(shù)發(fā)展和應(yīng)用的一個關(guān)鍵問題。
　　對于軟件系統(tǒng)安全性的保證要貫穿整個生命周期，高層設(shè)計的正確，并不能保證實現(xiàn)代碼的正確

2、，因此對于代碼也必須要進(jìn)行檢測。隨著軟件系統(tǒng)的規(guī)模和復(fù)雜程度的增加，傳統(tǒng)的檢測方法都不能滿足需求，模型檢測作為自動化的形式化方法，能夠高效、準(zhǔn)確的找到系統(tǒng)中的錯誤。
　　本文在對某安全苛求軟件的管理及存儲相關(guān)模塊進(jìn)行分析的基礎(chǔ)上，利用模型檢測工具LLBMC對其安全性進(jìn)行驗證，分析其在軟件設(shè)計和實現(xiàn)上存在的不足。LLBMC是具有精確內(nèi)存模型的限界模型檢測工具，本文實現(xiàn)了目標(biāo)程序源碼C語言到LLVM IR的轉(zhuǎn)換，并利用SMT求解器對得

3、到的問題進(jìn)行驗證，提出了軟件模塊安全性規(guī)范，通過判斷系統(tǒng)是否滿足規(guī)范以分析其安全性。模型檢測應(yīng)用于軟件系統(tǒng)的最主要問題就是狀態(tài)空間爆炸問題，本文通過多次實驗對最大循環(huán)次數(shù)、最大函數(shù)調(diào)用深度等參數(shù)對狀態(tài)空間和模型檢測消耗時間的影響進(jìn)行了分析，并針對狀態(tài)空間爆炸問題提出了幾種狀態(tài)約簡方法，包括減小最大調(diào)用深度、減小變量空間、廣度優(yōu)先修剪法等。實驗表明，通過幾種狀態(tài)約簡方法的組合，可使得驗證狀態(tài)空間控制在可檢測范圍內(nèi)。
　　本文實現(xiàn)了針