| 摘要 | 第1-9页 |
| ABSTRACT | 第9-11页 |
| 第一章 绪论 | 第11-15页 |
| ·课题背景 | 第11-12页 |
| ·研究现状和存在的问题 | 第12-13页 |
| ·本文主要工作 | 第13-14页 |
| ·论文结构 | 第14-15页 |
| 第二章 相关技术 | 第15-26页 |
| ·形式化验证技术的基本概念 | 第15页 |
| ·已有的基于模型的形式化验证方法 | 第15-23页 |
| ·基于Kripke 结构和时序逻辑的验证方法 | 第15-20页 |
| ·基于Petri 网的模型验证 | 第20-22页 |
| ·一阶迁移系统（FTS） | 第22-23页 |
| ·Alloy 建模基础 | 第23-25页 |
| ·本章小结 | 第25-26页 |
| 第三章 EFSOS 模型验证技术和反向建模 | 第26-37页 |
| ·对路径建模的验证方法 | 第26-27页 |
| ·EFSOS 模型 | 第27-31页 |
| ·EFSOS 模型的提出 | 第27页 |
| ·扩展的一阶逻辑系统(EFOL) | 第27-29页 |
| ·EFSOS 模型的定义 | 第29-30页 |
| ·EFSOS 模型的特点分析 | 第30-31页 |
| ·用Alloy 描述和验证EFSOS 模型 | 第31-33页 |
| ·用Alloy 定义状态 | 第31-32页 |
| ·用Alloy 定义操作 | 第32页 |
| ·用Alloy 定义状态转换序列 | 第32-33页 |
| ·反向建模 | 第33-36页 |
| ·概述 | 第34页 |
| ·反向建模的具体步骤 | 第34-36页 |
| ·本章小结 | 第36-37页 |
| 第四章 Windows Vista UAC 和MIC 机制的EFSOS 建模 | 第37-52页 |
| ·UAC 和MIC 机制的原理 | 第37-41页 |
| ·Windows 基本安全体系结构 | 第37-38页 |
| ·UAC 机制的原理 | 第38-40页 |
| ·MIC 机制的原理 | 第40-41页 |
| ·Windows Vista 特权和完整级反向建模 | 第41-51页 |
| ·模型的定义 | 第41页 |
| ·模型的解释 | 第41-51页 |
| ·本章小结 | 第51-52页 |
| 第五章 模型的分析与验证 | 第52-60页 |
| ·验证方法 | 第52页 |
| ·期望属性的提出 | 第52-53页 |
| ·期望属性2 的验证 | 第53-59页 |
| ·把期望属性转换为断言 | 第53-54页 |
| ·断言的验证结果分析 | 第54-57页 |
| ·实验确认 | 第57-59页 |
| ·改进建议 | 第59页 |
| ·本章小结 | 第59-60页 |
| 第六章 结束语 | 第60-62页 |
| ·本文工作总结 | 第60页 |
| ·展望 | 第60-62页 |
| 致谢 | 第62-64页 |
| 参考文献 | 第64-67页 |
| 作者在学期间取得的学术成果 | 第67页 |