VTOS中断系统的设计、实现以及验证

论文摘要

在很多场合下,人们要求计算机系统具有高度的安全性以及可靠性。一个计算机系统的安全性很大程度上取决于其所搭载的操作系统,而操作系统的安全性很大程度上取决于它的内核。因此保证内核的安全性以及可靠性是急需解决的问题。由于软件中存在的bug是随着代码量的增加而增加的,因此精简内核代码的微内核技术是增强内核安全性的方法之一。使用严格的形式化技术对软件进行验证是目前学术界公认的保证软件安全性以及可靠性的方法。诸如Verisoft、SeL4等等项目都使用了形式化方法对操作系统进行验证,并取得了很大的成果。但是目前绝大多数验证项目都是对上层软件的验证,对中断系统进行验证的工作很少。因为中断系统本身处于一个系统的最底层,且中断发生的不确定性导致系统执行流的不确定性使得中断的验证很复杂。但是保证中断系统的正确性是十分有必要的,因为中断系统的正确性保证了中断发生时进程上下文保存和恢复的正确性,这是多任务系统正确性的最基本前提之一。本文在对Minix3内核进行分析以及研究目前的一些操作系统验证项目后,首先设计并实现了一个基于微内核架构的操作系统、VTOS的中断系统以及调度系统,然后在辅助定理证明器Isabelle/HOL中对VTOS的中断系统和调度系统进行建模,通过对中断处理过程中所有可能执行的函数设置前置和后置条件以及相应的定理,证明了VTOS中断系统的完整性以及中断处理过程之中进程的上下文并没有被篡改,从而说明了VTOS中断系统的正确性。

论文目录

• 摘要
• Abstract
• 第一章 引言
• 1.1 研究背景
• 1.2 微内核
• 1.3 Isabelle/HOL介绍
• 1.4 本文研究内容以及主要工作
• 1.5 论文组织结构
• 第二章 相关工作介绍
• 2.1 微内核操作系统的发展
• 2.1.1 Mach
• 2.1.2 L4
• 2.1.3 Minix
• 2.2 操作系统验证项目的介绍
• 2.2.1 UCLA secure unix
• 2.2.2 KIT
• 2.2.3 VFiasco
• 2.2.4 verisoft
• 2.2.5 L4.verified
• 第三章 VTOS中断及调度系统的设计与实现
• 3.1 系统架构
• 3.2 中断系统的实现
• 3.2.1 中断相关知识
• 3.2.2 VTOS的中断机制
• 3.3 调度系统的实现
• 3.3.1 VTOS的调度策略
• 3.3.2 enqueue（）入队列
• 3.3.3 dequeue（）出队列
• 第四章 中断及调度系统的验证
• 4.1 验证目标
• 4.2 霍尔逻辑
• 4.3 自动机理论
• VTOS'>4.3.1 M_VTOS
• Isabelle/HOL'>4.3.2 M_Isabelle/HOL
• VTOS与M_Isabelle/HOL的一致性'>4.3.3 M_VTOS与M_Isabelle/HOL的一致性
• 4.4 验证思想
• 4.5 Isabelle/HOL中的模型
• 4.5.1 中断描述符表
• 4.5.2 寄存器现场
• 4.5.3 进程结构体
• 4.5.4 中断函数链
• 4.5.5 系统的状态
• 4.6 定理的描述以及证明
• 4.6.1 IDT表的正确设置
• 4.6.2 上下文的保存
• 4.6.3 中断处理相关函数的验证
• 4.6.4 上下文的恢复
• 第五章 总结与展望
• 5.1 本文总结
• 5.2 本文的不足与展望
• 参考文献
• 致谢
• 攻读硕士学位期间参与的科研课题