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

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

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

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