| 第一章 引言 | 第1-25页 |
| ·计算机信息系统面临的安全问题 | 第11-14页 |
| ·如何在内核级实现计算机系统的安全保护 | 第14-15页 |
| ·系统设计中形式化方法的作用及其基本架构 | 第15-18页 |
| ·形式化方法在安全操作系统设计中地位的确立 | 第18-19页 |
| ·安全操作系统形式设计面临的问题 | 第19-22页 |
| ·本学位论文的组织结构 | 第22-25页 |
| 第二章 形式模型设计的基本框架 | 第25-31页 |
| ·模型设计的基本原则 | 第25-26页 |
| ·模型的组织结构 | 第26-27页 |
| ·实现模型与分析模型的区分 | 第27-28页 |
| ·实现模型与分析模型设计的技术路线 | 第28-30页 |
| ·小结 | 第30-31页 |
| 第三章 支持多策略模型并存的形式架构 | 第31-43页 |
| ·相关工作 | 第31-34页 |
| ·一个新的支持多策略的形式架构 | 第34-38页 |
| ·实例研究 | 第38-41页 |
| ·小结 | 第41-43页 |
| 第四章 通用计算模型 | 第43-47页 |
| 第五章 DMLR_MLS与DAC的混合模型DBLP | 第47-73页 |
| ·对ABLP模型的分析 | 第50-52页 |
| ·一个改进的机密性策略模型DBLP | 第52-63页 |
| ·模型操作规则 | 第63-69页 |
| ·模型初态及基本安全定理 | 第69-70页 |
| ·实现IPC保护的方法 | 第70-72页 |
| ·相关工作 | 第72页 |
| ·结束语 | 第72-73页 |
| 第六章 基于DTE技术的完整性保护形式模型DTE_IPM | 第73-93页 |
| ·基于DTE实现完整性保护的形式模型 | 第76-90页 |
| ·在操作系统中完整性保护面临的问题 | 第76-78页 |
| ·模型实现完整性保护的原理及相关术语 | 第78-79页 |
| ·组织级安全策略 | 第79-80页 |
| ·模型变量及常量 | 第80-81页 |
| ·模型不变量 | 第81-85页 |
| ·模型规则及限制性条件 | 第85-89页 |
| ·基本安全定理 | 第89-90页 |
| ·对模型的分析及相关的工作 | 第90-91页 |
| ·结束语 | 第91-93页 |
| 第七章 基于权能、角色及DTE的特权控制模型PCM_RBPC | 第93-121页 |
| ·对现有权能机制的分析 | 第97-103页 |
| ·DG／UX的权能机制 | 第99-101页 |
| ·LinSec和Linux的权能机制 | 第101-102页 |
| ·一种新的权能机制 | 第102-103页 |
| ·基于权能、RBAC和DTE的形式模型PCM_RBPC | 第103-117页 |
| ·PCM_RBPC模型的组织级策略 | 第103-104页 |
| ·PCM_RBPC模型变量类型 | 第104页 |
| ·PCM_RBPC模型状态变量 | 第104-106页 |
| ·PCM_RBPC的不变量 | 第106-112页 |
| ·限制性条件和迁移规则 | 第112-116页 |
| ·基本安全定理 | 第116-117页 |
| ·相关的工作 | 第117-118页 |
| ·结束语 | 第118-121页 |
| 第八章 分析模型的设计与分析 | 第121-135页 |
| ·设计与分析的基础 | 第121-128页 |
| ·无干扰理论的基本原理 | 第121-124页 |
| ·无干扰理论应用于安全操作系统策略模型分析的研究现状 | 第124-126页 |
| ·层次化设计方法的基本原理 | 第126-128页 |
| ·抽象分析模型设计 | 第128-132页 |
| ·模型层次结构设计 | 第128-129页 |
| ·模型层次结构与无干扰理论的结合 | 第129-132页 |
| ·相关工作及结论 | 第132-135页 |
| 第九章 对模型解释的初步探讨 | 第135-157页 |
| ·系统体系结构 | 第135页 |
| ·Linux内核的抽象组成 | 第135-138页 |
| ·特权、权能和访问控制过程在系统中的解释 | 第138-143页 |
| ·模型在对象管理器中的表现模式 | 第143-154页 |
| ·文件系统和正规文件 | 第143-148页 |
| ·目录 | 第148-150页 |
| ·IPC对象 | 第150-152页 |
| ·进程 | 第152页 |
| ·设备、管道和命名管道 | 第152-153页 |
| ·符号联结 | 第153-154页 |
| ·网络对象 | 第154页 |
| ·系统控制数据 | 第154页 |
| ·用户 | 第154页 |
| ·模块机制 | 第154页 |
| ·视窗系统 | 第154页 |
| ·小结 | 第154-157页 |
| 第十章 主要成果和研究展望 | 第157-161页 |
| ·主要成果 | 第157-159页 |
| ·研究展望 | 第159-161页 |
| 参考文献 | 第161-171页 |
| 附录一 致谢 | 第171-173页 |
| 附录二 攻读博士学位区间已录用的论文 | 第173-174页 |
