本文選題：并發(fā) + 搶占�。� 參考：《中國(guó)科學(xué)技術(shù)大學(xué)》2016年博士論文

【摘要】：計(jì)算機(jī)系統(tǒng)被廣泛應(yīng)用于國(guó)防、通訊、金融等關(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)通常由C語(yǔ)言和內(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)系來(lái)刻畫(huà),這使得操作系統(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í)行的不確定性使得并發(fā)內(nèi)核的驗(yàn)證需要可組合的并發(fā)精化驗(yàn)證,而相關(guān)理論問(wèn)題直到最近幾年才被解決,因此之前的操作系統(tǒng)內(nèi)核驗(yàn)證項(xiàng)目都通過(guò)避免搶占和中斷來(lái)簡(jiǎn)化操作系統(tǒng)內(nèi)核驗(yàn)證,它們驗(yàn)證的內(nèi)核代碼是串行的。另一方面,現(xiàn)有的可組合的并發(fā)精化驗(yàn)證技術(shù)和中斷驗(yàn)證方法都是基于簡(jiǎ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)：·本文設(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)證明策略來(lái)提高驗(yàn)證效率。·本文首次完成了一個(gè)商業(yè)搶占式實(shí)時(shí)操作系統(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í)在高層模型上證明了互斥鎖滿足無(wú)優(yōu)先級(jí)反轉(zhuǎn)的性質(zhì)(priority-inversion-freedom, PIF)。值得一提的是,本文驗(yàn)證的是第三方開(kāi)發(fā)的商用內(nèi)核,而不是為了驗(yàn)證自己開(kāi)發(fā)的內(nèi)核�！け疚乃枋龅牟僮飨到y(tǒng)內(nèi)核驗(yàn)證框架和μC/OS-II的驗(yàn)證都已在定理證明工具Coq中實(shí)現(xiàn),生成了機(jī)器可檢查的證明。證明腳本的代碼量總計(jì)約225000行,這是第一個(gè)商業(yè)化實(shí)時(shí)操作系統(tǒng)內(nèi)核的核心功能模塊的機(jī)器可檢查證明。
[Abstract]:Computer system is widely used in the key fields such as national defense, communication and finance. The construction of a highly trusted computer system has become an important issue in the world. As the core software of the computer system, the core of the operating system is the key to the construction of a highly trusted computing system. The crash proof code, Formalized verification technology is used to strictly guarantee the correctness of the underlying operating system. It has become one of the ten new emerging technologies by "technical review" published by MIT in 2011, and it has become a new research hotspot. And some features of the operating system make formalized verification difficult, for example, many operating systems usually consist of C language and embedded assembler. A large scale of code supports multitask concurrency, interruption, and preemption. In these features, the high concurrency of the kernel code caused by preemption and interruption makes the verification of the operating system especially difficult. The correctness of the operating system is usually refined by the implementation of the application programming interface (API) and its high-level abstraction. This makes the verification of the correctness of the operating system based on the procedure refinement verification technology, and the verification of the concurrent kernel needs to be combined with concurrent validation and refinement validation, which makes the verification of the concurrent kernel difficult. On the one hand, the uncertainty of the task execution due to the preemption and interruption requests makes the concurrency internal. Nuclear verification requires a combination of concurrent refinement validation, and related theoretical issues have not been solved until recent years, so the previous operating system kernel validation projects simplify the operating system kernel validation by avoiding preemption and interruption, and the kernel code that they verify is serial. On the other hand, existing concurrent refined tests are available. Both the authentication technology and the interrupt verification method are based on the simplified theoretical model, which can not be applied directly to the kernel verification of the commercial preemptive operating system, and need to be adjusted and extended. This paper explores how to apply the combined concurrency verification and interruption verification method to the verification of the preemptive kernel of the commercialized system. The following contributions are made:. This paper designs and implements the first practical preemptive operating system kernel validation framework. The validation framework aims to verify the correctness of the operating system kernel function, and the function correctness of the operating system kernel is defined as the implementation of the application programming interface (API) and its abstract protocol. The whole validation framework consists of three parts: (1) formalized modeling of the operating system kernel; (2) a concurrent refinement logic CSL-R supporting multilevel interrupts to verify the correctness of the kernel code; (3) and some automatic proof strategies to improve the efficiency of verification. The correctness of the key functional modules of the real time operating system kernel mu C/OS- II, including task scheduler, clock interrupt program, clock management, and four synchronous communication mechanisms: message queuing, mutex, message mailbox and semaphore, total about 3450 lines of C code, covering about 68% of the common API. and proving on the high level model The mutex satisfies the property of non priority inversion (priority-inversion-freedom, PIF). It is worth mentioning that this article is verified by the commercial kernel developed by the third party, not in order to verify its own kernel. The operating system kernel verification framework and the verification of the C/OS-II are all in the theorem proving tool Coq Now, a proof of machine checking is generated. It proves that the code amount of the script total about 225000 lines, which is the machine checking proof of the core functional modules of the first commercial real-time operating system kernel.
【學(xué)位授予單位】：中國(guó)科學(xué)技術(shù)大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP316

【參考文獻(xiàn)】

相關(guān)期刊論文 前3條

1 王勇朝;李兆鵬;馮新宇;;一個(gè)C語(yǔ)言子集上的程序邏輯[J];小型微型計(jì)算機(jī)系統(tǒng);2014年06期

2 朱允敏;張麗偉;王生原;董淵;張素琴;;面向多核處理器的低級(jí)并行程序驗(yàn)證[J];電子學(xué)報(bào);2009年S1期

3 肖增良;何锫;康立山;;并行程序驗(yàn)證的調(diào)度策略[J];計(jì)算機(jī)工程與應(yīng)用;2009年11期

，

本文編號(hào)：1926081