本文選題：并發(fā) + 搶占��； 參考：《中國科學技術大學》2016年博士論文

【摘要】：計算機系統(tǒng)被廣泛應用于國防、通訊、金融等關鍵領域,構建高可信的計算機系統(tǒng)已成為世界范圍的重要課題。操作系統(tǒng)內核作為計算機系統(tǒng)中的底層核心軟件,其安全可靠性是構建高可信計算機系統(tǒng)的關鍵。防崩潰代碼(crash proof code),即用形式化驗證技術嚴格保證底層操作系統(tǒng)的正確性,被2011年MIT出版的《技術評論》評選為十大新興技術之一,成為了一個新的研究熱點。而操作系統(tǒng)本身的一些特征使得形式化驗證變得困難,譬如很多操作系統(tǒng)通常由C語言和內嵌匯編實現(xiàn)、代碼規(guī)模較大、支持多任務并發(fā)、中斷和搶占等,在這些特征中由于搶占和中斷導致內核代碼的高度并發(fā)使得操作系統(tǒng)的驗證變得尤其困難。操作系統(tǒng)的正確性通常使用應用程序編程接口(API)的具體實現(xiàn)與其高層抽象之間的精化關系來刻畫,這使得操作系統(tǒng)正確性驗證需要基于程序精化驗證技術,而并發(fā)系統(tǒng)內核的驗證需要同時結合并發(fā)驗證和精化驗證,這使得并發(fā)內核的驗證變得十分困難。一方面,由于搶占和中斷請求導致任務執(zhí)行的不確定性使得并發(fā)內核的驗證需要可組合的并發(fā)精化驗證,而相關理論問題直到最近幾年才被解決,因此之前的操作系統(tǒng)內核驗證項目都通過避免搶占和中斷來簡化操作系統(tǒng)內核驗證,它們驗證的內核代碼是串行的。另一方面,現(xiàn)有的可組合的并發(fā)精化驗證技術和中斷驗證方法都是基于簡化的理論模型,不能直接將其應用于商業(yè)化的搶占式操作系統(tǒng)內核驗證工作中,需要進行調整和擴展。本文探索如何將可組合的并發(fā)精化驗證技術和中斷驗證方法應用于驗證商業(yè)化的搶占式內核,并做出了如下貢獻：·本文設計并實現(xiàn)了第一個實用的搶占式操作系統(tǒng)內核驗證框架。驗證框架以驗證操作系統(tǒng)內核功能正確性為目標,這里操作系統(tǒng)內核的功能正確性被定義為應用程序編程接口(API)的實現(xiàn)及其抽象規(guī)約之間的上下文精化關系。整個驗證框架由三個部分構成：(1)操作系統(tǒng)內核的形式化建模；(2)一個支持多級中斷的并發(fā)精化程序邏輯CSL-R用于驗證內核代碼的正確性；(3)以及一些自動證明策略來提高驗證效率�！け疚氖状瓮瓿闪艘粋�商業(yè)搶占式實時操作系統(tǒng)內核μC/OS-Ⅱ的關鍵功能模塊的正確性驗證,包括任務調度程序,時鐘中斷程序,時鐘管理,以及四種同步通信機制：消息隊列、互斥鎖、消息郵箱和信號量,總計約3450行C代碼,覆蓋了68%左右的常用API。同時在高層模型上證明了互斥鎖滿足無優(yōu)先級反轉的性質(priority-inversion-freedom, PIF)。值得一提的是,本文驗證的是第三方開發(fā)的商用內核,而不是為了驗證自己開發(fā)的內核�！け疚乃枋龅牟僮飨到y(tǒng)內核驗證框架和μC/OS-II的驗證都已在定理證明工具Coq中實現(xiàn),生成了機器可檢查的證明。證明腳本的代碼量總計約225000行,這是第一個商業(yè)化實時操作系統(tǒng)內核的核心功能模塊的機器可檢查證明。
[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.
【學位授予單位】：中國科學技術大學
【學位級別】：博士
【學位授予年份】：2016
【分類號】：TP316

【參考文獻】

相關期刊論文 前3條

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

2 朱允敏;張麗偉;王生原;董淵;張素琴;;面向多核處理器的低級并行程序驗證[J];電子學報;2009年S1期

3 肖增良;何锫;康立山;;并行程序驗證的調度策略[J];計算機工程與應用;2009年11期

，

本文編號：1926081