基于形式化方法的軟件代碼安全性驗(yàn)證技術(shù).pdf

1、隨著計(jì)算機(jī)軟件技術(shù)的快速發(fā)展，特別是在航空航天、交通運(yùn)輸、生物醫(yī)療等安全苛求系統(tǒng)中的應(yīng)用越來越廣泛，軟件系統(tǒng)的安全性、可靠性變得越來越重要，任何一個(gè)錯(cuò)誤都可能帶來災(zāi)難性的后果。因此，如何保障軟件系統(tǒng)的安全可靠性越來越受到人們的關(guān)注。
　　從軟件系統(tǒng)的設(shè)計(jì)到最終的代碼實(shí)現(xiàn)，每一個(gè)環(huán)節(jié)都關(guān)系到軟件的安全性，但系統(tǒng)的高層設(shè)計(jì)的正確性不能保證代碼實(shí)現(xiàn)的安全性，因此只有通過對(duì)源代碼進(jìn)行安全性驗(yàn)證才能保障系統(tǒng)的安全性。模型檢測(cè)是一種基于形式化

2、方法的自動(dòng)化驗(yàn)證技術(shù)，與傳統(tǒng)驗(yàn)證技術(shù)相比，具有無二義性、高效、可靠等特點(diǎn)，在電路設(shè)計(jì)和通信協(xié)議設(shè)計(jì)中得到了廣為應(yīng)用，但其在軟件系統(tǒng)安全性領(lǐng)域是近些年才被引入的，特別是在軟件代碼驗(yàn)證領(lǐng)域的研究還不成熟。
　　本文首先介紹了模型檢測(cè)技術(shù)的理論基礎(chǔ)、檢測(cè)流程、發(fā)展現(xiàn)狀，并指出了模型檢測(cè)中狀態(tài)空間爆炸的問題及現(xiàn)有解決方法。通過對(duì)某安全苛求系統(tǒng)的以存儲(chǔ)為中心的軟件構(gòu)件進(jìn)行分析，選定模型檢測(cè)工具LLBMC作為安全性驗(yàn)證研究工具。LLBMC作為

3、一種具有精確內(nèi)存模型的有界模型檢測(cè)工具，能夠針對(duì)軟件模塊的內(nèi)存錯(cuò)誤和邏輯錯(cuò)誤的形式化驗(yàn)證并對(duì)得到的軟件系統(tǒng)錯(cuò)誤進(jìn)行追蹤定位。對(duì)影響軟件系統(tǒng)模型狀態(tài)空間和模型檢測(cè)時(shí)間的兩個(gè)關(guān)鍵要素——廣度和深度進(jìn)行分析，分別用最大循環(huán)的次數(shù)表示廣度，最大函數(shù)調(diào)用深度表示深度，進(jìn)而發(fā)現(xiàn)廣度是導(dǎo)致狀態(tài)空間爆炸的主要因素。在此基礎(chǔ)上，提出了一種面向模型狀態(tài)空間中狀態(tài)可達(dá)性的判斷方法，設(shè)計(jì)了一種基于廣度優(yōu)先剪枝的狀態(tài)空間縮減方法，并通過實(shí)驗(yàn)驗(yàn)證了該方法可有效應(yīng)對(duì)