基于形式化方法的軟件代碼安全性驗證技術.pdf

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

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

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