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

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

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