軟件可信驗證自動化技術(shù)研究.pdf

1、缺陷和漏洞廣泛存在于各種軟件中，難以避免，由其引發(fā)的故障很容易給生命財產(chǎn)帶來損害，甚至災(zāi)難性后果。應(yīng)對這一問題的有效途徑是設(shè)計有效合理的自動化的測試方法對軟件系統(tǒng)可信度進(jìn)行充分全面的驗證。本論文對軟件可信安全性驗證研究從靜態(tài)驗證和動態(tài)檢測兩個角度分別著手。
　　首先從靜態(tài)檢測角度，針對安全苛刻性編程標(biāo)準(zhǔn)，提出基于規(guī)則匹配的代碼靜態(tài)檢測方法。構(gòu)建易于表述及存儲源碼信息的源碼表示模型，解決C++語言的靈活性和復(fù)雜性導(dǎo)致的難以對代碼直接

2、進(jìn)行規(guī)則匹配的問題;設(shè)計解析樹模型和存儲轉(zhuǎn)換模型，完成從源代碼提取與規(guī)則有關(guān)的信息翻譯為中間表示文件的源碼解析過程;設(shè)計包含編程安全標(biāo)準(zhǔn)中全部有效規(guī)則的規(guī)則庫模型用于對中間表示文件進(jìn)行規(guī)則匹配和缺陷反饋;通過系統(tǒng)實現(xiàn)和實驗驗證方法的有效性。
　　然后從動態(tài)檢測角度，提出一種基于非確定性FSM模型的測試生成和測試驗證方法。針對復(fù)雜軟件系統(tǒng)狀態(tài)行為轉(zhuǎn)換不確定的問題，提出層次化建模方法，對不確定的狀態(tài)轉(zhuǎn)移進(jìn)行聚類和分層建模，將其轉(zhuǎn)化為分

3、層子狀態(tài)機(jī)間確定唯一的狀態(tài)轉(zhuǎn)移，解決軟件設(shè)計規(guī)格不確定行為難以描述和生成測試用例的問題;提出從正則式模型產(chǎn)生測試集的方法，根據(jù)狀態(tài)機(jī)與正則表達(dá)式的等價關(guān)系，構(gòu)建狀態(tài)機(jī)模型對應(yīng)的的正則式模型，給出遷移覆蓋算法從正則式模型生成測試集，解決軟件系統(tǒng)控制流程中循環(huán)部分在用例中難以精確描述的問題;在正則式模型中加入不同觸發(fā)參數(shù)作為用例特征，劃分出不同特征的測試集，提高用例的驗證能力和測試充分性。
　　靜態(tài)手段可以在軟件開發(fā)早期發(fā)現(xiàn)程序中的潛