抢占式操作系统内核验证框架的设计和实现

发布时间：2018-05-23 19:41

本文选题：并发 + 抢占　；参考：《中国科学技术大学》2016年博士论文

【摘要】：计算机系统被广泛应用于国防、通讯、金融等关键领域,构建高可信的计算机系统已成为世界范围的重要课题。操作系统内核作为计算机系统中的底层核心软件,其安全可靠性是构建高可信计算机系统的关键。防崩溃代码(crash proof code),即用形式化验证技术严格保证底层操作系统的正确性,被2011年MIT出版的《技术评论》评选为十大新兴技术之一,成为了一个新的研究热点。而操作系统本身的一些特征使得形式化验证变得困难,譬如很多操作系统通常由C语言和内嵌汇编实现、代码规模较大、支持多任务并发、中断和抢占等,在这些特征中由于抢占和中断导致内核代码的高度并发使得操作系统的验证变得尤其困难。操作系统的正确性通常使用应用程序编程接口(API)的具体实现与其高层抽象之间的精化关系来刻画,这使得操作系统正确性验证需要基于程序精化验证技术,而并发系统内核的验证需要同时结合并发验证和精化验证,这使得并发内核的验证变得十分困难。一方面,由于抢占和中断请求导致任务执行的不确定性使得并发内核的验证需要可组合的并发精化验证,而相关理论问题直到最近几年才被解决,因此之前的操作系统内核验证项目都通过避免抢占和中断来简化操作系统内核验证,它们验证的内核代码是串行的。另一方面,现有的可组合的并发精化验证技术和中断验证方法都是基于简化的理论模型,不能直接将其应用于商业化的抢占式操作系统内核验证工作中,需要进行调整和扩展。本文探索如何将可组合的并发精化验证技术和中断验证方法应用于验证商业化的抢占式内核,并做出了如下贡献：·本文设计并实现了第一个实用的抢占式操作系统内核验证框架。验证框架以验证操作系统内核功能正确性为目标,这里操作系统内核的功能正确性被定义为应用程序编程接口(API)的实现及其抽象规约之间的上下文精化关系。整个验证框架由三个部分构成：(1)操作系统内核的形式化建模；(2)一个支持多级中断的并发精化程序逻辑CSL-R用于验证内核代码的正确性；(3)以及一些自动证明策略来提高验证效率。·本文首次完成了一个商业抢占式实时操作系统内核μC/OS-Ⅱ的关键功能模块的正确性验证,包括任务调度程序,时钟中断程序,时钟管理,以及四种同步通信机制：消息队列、互斥锁、消息邮箱和信号量,总计约3450行C代码,覆盖了68%左右的常用API。同时在高层模型上证明了互斥锁满足无优先级反转的性质(priority-inversion-freedom, PIF)。值得一提的是,本文验证的是第三方开发的商用内核,而不是为了验证自己开发的内核。·本文所描述的操作系统内核验证框架和μC/OS-II的验证都已在定理证明工具Coq中实现,生成了机器可检查的证明。证明脚本的代码量总计约225000行,这是第一个商业化实时操作系统内核的核心功能模块的机器可检查证明。
[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

【参考文献】