基于模型檢測的操作系統(tǒng)內(nèi)核性質(zhì)驗證的研究.pdf

1、操作系統(tǒng)是計算機系統(tǒng)中最基本、最重要的軟件,其安全性和可靠性是計算機系統(tǒng)提供可信計算的首要條件,也是其它應用軟件正常運行的基本保障。但是操作系統(tǒng)內(nèi)核結構復雜、規(guī)模龐大,其開發(fā)與調(diào)試都十分困難,一些隱藏的錯誤用一般的軟件測試及驗證技術很難發(fā)現(xiàn)。模型檢測技術具有簡潔明了、自動化程度高等特點,往往能發(fā)現(xiàn)其他測試技術難以發(fā)現(xiàn)的軟件錯誤,傳統(tǒng)的模型檢測摒除了很多軟件實現(xiàn)細節(jié),要檢測實際的代碼,就需要從代碼中直接建立抽象描述。而操作系統(tǒng)內(nèi)核結構復雜

2、,手動對源代碼進行抽象存在建模工作量大、人工參與過多、易出錯以及屬性難以描述和檢測等問題。
　　 本文以Linux內(nèi)核作為實驗對象,提出了一種基于屬性的操作系統(tǒng)內(nèi)核自動驗證方法,利用模型抽取工具Modex從Linux內(nèi)核源代碼自動抽取模型,試圖保證模型與實現(xiàn)代碼一致性的同時減少因人工參與產(chǎn)生的人為錯誤,然后用時間軸屬性來描述源代碼應有的屬性,最后用模型檢測工具Spin對Linux內(nèi)核代碼模型進行檢測。實驗選取了Linux內(nèi)核中接