| 摘要 | 第1-6页 |
| Abstract | 第6-9页 |
| 目录 | 第9-12页 |
| 插图 | 第12-13页 |
| 第一章 引言 | 第13-18页 |
| ·选题背景与意义 | 第13-15页 |
| ·本文的主要工作 | 第15-16页 |
| ·攻读博士期间完成的主要工作 | 第16-17页 |
| ·参加的主要科研项目 | 第16页 |
| ·论文的撰写和发表 | 第16-17页 |
| ·本文的组织和安排 | 第17-18页 |
| 第二章 OS形式化设计与验证的研究基础和相关工作 | 第18-37页 |
| ·软件形式化验证的评价体系 | 第19页 |
| ·采用形式化方法的意义 | 第19-21页 |
| ·形式化方法需要考虑的几个问题 | 第21-22页 |
| ·形式化工具的正确性 | 第21-22页 |
| ·从非形式化到形式化的转化 | 第22页 |
| ·OS形式化设计和验证框架 | 第22-23页 |
| ·OS形式化设计和验证研究现状 | 第23-35页 |
| ·UCLA Secure Data Unix | 第24-26页 |
| ·Provably Secure Operating System(PSOS) | 第26-27页 |
| ·Kernel for Isolated Tasks(KIT) | 第27-28页 |
| ·DTOS | 第28页 |
| ·VFiasco | 第28-29页 |
| ·EROS/Coyotos | 第29-30页 |
| ·Flint | 第30-31页 |
| ·Verisoft | 第31-32页 |
| ·L4.verified/seL4 | 第32-35页 |
| ·已有工作的不足、存在的问题和本文的思路 | 第35-37页 |
| 第三章 预备知识 | 第37-39页 |
| 第四章 OS对象语义模型(OSOSM)研究 | 第39-55页 |
| ·OS对象语义模型(OSOSM)的意义 | 第39-40页 |
| ·OSOSM框架 | 第40-43页 |
| ·OS对象 | 第40-41页 |
| ·OS对象语义模型(OSOSM) | 第41-43页 |
| ·OSOSM论域和形式化模型 | 第43-46页 |
| ·OSOSM语义分析和安全性验证 | 第46-54页 |
| ·VMM基本功效层的语义 | 第46-50页 |
| ·VMM实现层和优化层的语义 | 第50-53页 |
| ·系统安全性验证 | 第53-54页 |
| ·本章小结 | 第54-55页 |
| 第五章 OS形式化设计与安全需求的一致性验证 | 第55-83页 |
| ·本章研究背景 | 第55-56页 |
| ·VTOS微内核对象语义模型 | 第56-66页 |
| ·基本功效层 | 第56-59页 |
| ·实现层 | 第59-63页 |
| ·优化层 | 第63-66页 |
| ·VTOS系统安全需求 | 第66-70页 |
| ·时序逻辑 | 第66-67页 |
| ·消息处理行为的功效完整性安全需求 | 第67-69页 |
| ·进程调度行为的功效完整性安全需求 | 第69-70页 |
| ·中断处理行为的功效完整性安全需求 | 第70页 |
| ·进程行为隔离性需求 | 第70页 |
| ·VTOS设计与安全需求的一致性验证 | 第70-81页 |
| ·微内核OSOSM的Isabelle/HOL方式建模 | 第71-75页 |
| ·时序逻辑在Isabelle中的验证方法 | 第75-78页 |
| ·一致性验证 | 第78-81页 |
| ·本章小结 | 第81-83页 |
| 第六章 OS汇编级形式化设计和验证方法研究 | 第83-97页 |
| ·VTOS状态自动机模型OSSA | 第83-87页 |
| ·软/硬件计算单元 | 第84-85页 |
| ·系统对象状态 | 第85-86页 |
| ·事件 | 第86页 |
| ·VTOS状态自动机模型OSSA框架 | 第86-87页 |
| ·OSSA在Isabelle/HOL的建模 | 第87-90页 |
| ·VTOS论域 | 第88页 |
| ·在Isabelle/HOL中构建OSSA | 第88-90页 |
| ·系统初始化过程汇编级验证 | 第90-93页 |
| ·系统功能模块的汇编级验证 | 第93-96页 |
| ·本章小结 | 第96-97页 |
| 第七章 总结与未来的工作 | 第97-99页 |
| 参考文献 | 第99-111页 |
| 攻读博士学位期间科研成果 | 第111-113页 |
| 致谢 | 第113-114页 |
