搶占式操作系統(tǒng)內(nèi)核驗(yàn)證框架的設(shè)計(jì)和實(shí)現(xiàn).pdf

1、計(jì)算機(jī)系統(tǒng)被廣泛應(yīng)用于國防、通訊、金融等關(guān)鍵領(lǐng)域，構(gòu)建高可信的計(jì)算機(jī)系統(tǒng)已成為世界范圍的重要課題。操作系統(tǒng)內(nèi)核作為計(jì)算機(jī)系統(tǒng)中的底層核心軟件，其安全可靠性是構(gòu)建高可信計(jì)算機(jī)系統(tǒng)的關(guān)鍵。
　　防崩潰代碼(crash proof code)，即用形式化驗(yàn)證技術(shù)嚴(yán)格保證底層操作系統(tǒng)的正確性，被2011年MIT出版的《技術(shù)評(píng)論》評(píng)選為十大新興技術(shù)之一，成為了一個(gè)新的研究熱點(diǎn)。而操作系統(tǒng)本身的一些特征使得形式化驗(yàn)證變得困難，譬如很多操作系統(tǒng)

2、通常由C語言和內(nèi)嵌匯編實(shí)現(xiàn)、代碼規(guī)模較大、支持多任務(wù)并發(fā)、中斷和搶占等，在這些特征中由于搶占和中斷導(dǎo)致內(nèi)核代碼的高度并發(fā)使得操作系統(tǒng)的驗(yàn)證變得尤其困難。
　　操作系統(tǒng)的正確性通常使用應(yīng)用程序編程接口(API)的具體實(shí)現(xiàn)與其高層抽象之間的精化關(guān)系來刻畫，這使得操作系統(tǒng)正確性驗(yàn)證需要基于程序精化驗(yàn)證技術(shù)，而并發(fā)系統(tǒng)內(nèi)核的驗(yàn)證需要同時(shí)結(jié)合并發(fā)驗(yàn)證和精化驗(yàn)證，這使得并發(fā)內(nèi)核的驗(yàn)證變得十分困難。一方面，由于搶占和中斷請(qǐng)求導(dǎo)致任務(wù)執(zhí)行的不確定

3、性使得并發(fā)內(nèi)核的驗(yàn)證需要可組合的并發(fā)精化驗(yàn)證，而相關(guān)理論問題直到最近幾年才被解決，因此之前的操作系統(tǒng)內(nèi)核驗(yàn)證項(xiàng)目都通過避免搶占和中斷來簡化操作系統(tǒng)內(nèi)核驗(yàn)證，它們驗(yàn)證的內(nèi)核代碼是串行的。另一方面，現(xiàn)有的可組合的并發(fā)精化驗(yàn)證技術(shù)和中斷驗(yàn)證方法都是基于簡化的理論模型，不能直接將其應(yīng)用于商業(yè)化的搶占式操作系統(tǒng)內(nèi)核驗(yàn)證工作中，需要進(jìn)行調(diào)整和擴(kuò)展。本文探索如何將可組合的并發(fā)精化驗(yàn)證技術(shù)和中斷驗(yàn)證方法應(yīng)用于驗(yàn)證商業(yè)化的搶占式內(nèi)核，并做出了如下貢獻(xiàn):<

4、br>　　本文設(shè)計(jì)并實(shí)現(xiàn)了第一個(gè)實(shí)用的搶占式操作系統(tǒng)內(nèi)核驗(yàn)證框架。驗(yàn)證框架以驗(yàn)證操作系統(tǒng)內(nèi)核功能正確性為目標(biāo)，這里操作系統(tǒng)內(nèi)核的功能正確性被定義為應(yīng)用程序編程接口(API)的實(shí)現(xiàn)及其抽象規(guī)約之間的上下文精化關(guān)系。整個(gè)驗(yàn)證框架由三個(gè)部分構(gòu)成:(1)操作系統(tǒng)內(nèi)核的形式化建模;(2)一個(gè)支持多級(jí)中斷的并發(fā)精化程序邏輯CSL-R用于驗(yàn)證內(nèi)核代碼的正確性;(3)以及一些自動(dòng)證明策略來提高驗(yàn)證效率。
　　本文首次完成了一個(gè)商業(yè)搶占式實(shí)時(shí)操作系

5、統(tǒng)內(nèi)核μC/OS-Ⅱ的關(guān)鍵功能模塊的正確性驗(yàn)證，包括任務(wù)調(diào)度程序，時(shí)鐘中斷程序，時(shí)鐘管理，以及四種同步通信機(jī)制:消息隊(duì)列、互斥鎖、消息郵箱和信號(hào)量，總計(jì)約3450行C代碼，覆蓋了68％左右的常用API。同時(shí)在高層模型上證明了互斥鎖滿足無優(yōu)先級(jí)反轉(zhuǎn)的性質(zhì)(priority-inversion-freedom，PIF)。值得一提的是，本文驗(yàn)證的是第三方開發(fā)的商用內(nèi)核，而不是為了驗(yàn)證自己開發(fā)的內(nèi)核。
　　本文所描述的操作系統(tǒng)內(nèi)核驗(yàn)證框架