小型操作系统内核的轻量级形式化设计和验证方法研究

项目名称： 小型操作系统内核的轻量级形式化设计和验证方法研究

项目编号： No.61402057

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

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 钱振江

作者单位： 常熟理工学院

项目金额： 24万元

中文摘要： 操作系统功能体系需求、设计和实现的一致性，以及功能体系与实现的正确性和安全性是安全操作系统重要的两个问题，由于操作系统框架和形式化逻辑系统的复杂性，对其设计和实现的形式化验证变得非常困难。此前我们对操作系统的安全结构和功能体系进行了研究，开发了一个小型微内核操作系统原型VTOS。本课题旨在针对操作系统设计实现和验证方面提出一种易于建模、描述能力强、推理方便的形式化方法。本申请课题计划针对Intel处理器建立操作系统内核硬件模型，描述系统内核代码的语义；设计内核状态自动机模型，分析内核的功能与安全特性，准确定义系统内核的状态空间，建立内核论域以及与逻辑系统中模型的映射关系，定义内核功能正确性和系统完整性的逻辑断言；借助Isabelle/HOL定理证明器验证VTOS微内核的实现是否满足预期功能正确性和完整性的逻辑断言；研究形式化验证过程中的反馈机制，通过对系统设计的反馈来保证系统的正确性。

中文关键词： 操作系统；形式化设计；形式化验证；内核完整性；内核正确性

英文摘要： The consistency among functonality requirements, design and implementation of the operating system, and the correctness and security of the system functionality and implementation, are the two important issues for the security operating system. Due to the

英文关键词： Operating system；formal design；formal verification；kernel integrity；kernel correctness