操作系统内核中线程管理与中断管理的验证研究

项目名称： 操作系统内核中线程管理与中断管理的验证研究

项目编号： No.61202052

项目类型： 青年科学基金项目

立项/批准年度： 2013

项目学科： 计算机科学学科

项目作者： 郭宇

作者单位： 中国科学技术大学

项目金额： 23万元

中文摘要： 操作系统内核的线程管理与中断管理是内核的主要组成部分。它们位于内核的最底层，为上层的内核代码提供多线程机制，其安全性对于整个计算机系统至关重要。这部分代码由于并发性与内在复杂性，为形式化验证内核带来了一些验证难题。而国内外的一些操作系统内核验证工作也对这部分代码研究不足，他们或验证串行执行的线程管理代码，或过度简化这部分功能，因此无法适用于主流内核中的线程管理与中断管理代码，如FreeRTOS与Linux等。本项目拟针对当前研究的不足，深入分析实际的操作系统内核中的并发特性，探索研究支持多核的内核线程管理与中断管理部分的语义描述与验证的一般性方法与理论，并应用这些理论方法来验证一个实际的但规模相对较小的嵌入式操作系统内核FreeRTOS的线程管理与中断管理部分。本项目研究的操作系统内核中的并发代码的验证方法、相关理论与技术对高可信计算机系统的构建有着一定的理论价值与科学意义。

中文关键词： 程序验证；操作系统内核；线程管理；中断管理；

英文摘要： Thread management and interrupt management are the essential parts of operating system kernels. Providing the multithreading mechanism at the lowest level of kernels, they are obviously critical to the safety of computer systems. Since the concurrency and the intricate design, these parts of code are extremely hard to verify formally. Although a large amount of research work has been done for verifying OS kernels, the thread management and interrupt management are usually serialized, or over-simplified to verify. As a result, previous work is unable to applied to verify reaslistic thread management and interrupt management of some of modern OS kernels, like Linux, FreeRTOS and so on. In this proposal, we propose a research project for verifying the thread management and interrupt management of some realistic OS kernels with multi-core support, where the kernel code runs concurrently with sophisticated control flows. We plan to work on the theoretical aspect of verifying the thread management and interrupt management with multi-core support, methodolgy of describing the formal semantics of OS kernels, program logics for reasoning about the safety of kernel code. We also plan to verify the thread management and interrupt management of a realitic embedded OS kernel- - FreeRTOS. We hope that the theoretical result o

英文关键词： Program verification；Operating system kernel；Thread management；Interrupt management；