形式化验证在Office安全中的应用研究

论文摘要

Office是一个综合的集成办公套件。作为国家,政府和军队日常办公的必备软件,应当具有完善的安全功能,同时Office安全功能扩展也是信息安全保障中重要的应用。 现阶段,我军正在大力推进军用安全操作系统平台下军用Office的研发。由于军队的特殊性,Office安全功能是军用Office的关键组成部分,而如何提高Office安全功能自身的安全性显得尤为重要。 为提高其安全性,通常我们采用传统的开发方法。它只能解决表面上的问题,对于深层次的问题显得力不从心。但是形式化验证技术作为一种基于数学的推理手段,能够消除理论与实现之间的二义性。所以本课题的主要研究内容就是构建Office安全功能并验证设计与实现的一致性并消除实现与设计原形的歧义。 论文主要在以下三个方面进行了研究:第一,在深入研究BLP、Biba和Clark-Wilson等安全模型的基础上,为构建Office安全功能内核提出了一个以消息为主结合参照监视器机制的过滤器结构的方案。第二,基于M-Office并结合《中华人民共和国数字签名法》和“国家密码管理委员会”的相关规定对Office安全功能扩展进行了研究,开发出符合标准的Office安全功能,它包括数字签名、电子印章、手写签名、证书加密。第三,借助形式化验证规范语言—Z,验证了Office安全模型与功能实现之间的一致性,从而提出了构建安全应用自身安全性的一种方法。最后对本文的工作和今后进一步研究的问题进行了总结和展望。

论文目录

• 目录
• 摘要
• Abstract
• 第一章 引言
• 1.1 研究背景
• 1.1.1 Office安全的重要性
• 1.1.2 Office安全功能开发的可行性
• 1.2 论文的研究目标
• 1.3 论文的组织结构
• 第二章 Office安全技术基础
• 2.1 Office文档安全
• 2.2 Office文档内部的安全结构
• 2.2.1 Office签名文档的内部结构
• 2.2.2 Office加密文档的内部结构
• 2.3 构建Office安全功能内核的一些模型
• 2.3.1 Bell-LaPadula模型在Office安全内核中的应用
• 23.2 Biba模型在Office安全内核中的应用
• 2.3.3 Clark-Wilson模型在Office安全内核中的应用
• 2.4 本章小结
• 第三章 Office安全功能及其实现
• 3.1 Office安全功能的开发过程
• 3.1.1 Office的安全功能
• 3.2 Office安全功能的实现目标
• 3.3 Office安全功能的策略
• 3.3.1 Office安全功能的设计方案
• 3.3.2 Office文档—对象间交互
• 3.3.3 Office安全功能内核的行为对象
• 3.3.4 Office安全功能内核的数据容器
• 3.3.5 Office安全功能内核的密钥与证书容器
• 3.3.6 Office安全功能内核的安全属性容器
• 3.3.7 内核对象的内部细节
• 3.3.8 Office安全功能内核对象间通信
• 3.4 本章小结
• 第四章 Office安全功能内核的体系结构
• 4.1 Office安全功能内核实现的基础
• 4.2 Office安全功能内核体系结构的设计目标
• 4.3 Office安全功能内核的安全机制
• 4.3.1 Office安全功能内核
• 4.3.2 Office安全内核消息的处理
• 4.3.3 Office安全功能内核的访问控制列表
• 4.3.4 Office安全功能内核的整体控制流程
• 4.3.5 Office安全功能内核的分离机制
• 4.3.6 Office的可信计算基（TCB）
• 4.4 本章小结
• 第五章 形式化验证技术
• 5.1 形式描述语言——Z语言
• 5.1.1 Z中的系统规范
• 5.1.2 状态描述
• 5.1.3 操作
• 5.1.4 状态限制
• 5.1.5 Z规范语言总结
• 5.2 Z/EVES形式验证系统
• 5.3 Office安全中的形式化验证技术
• 5.4 Office安全功能中的形式化验证策略
• 5.4.1 Office安全功能设计求精的策略
• 5.4.2 Office安全功能算法求精的策略
• 5.5 本章小结
• 第六章 验证过程及结果
• 6.1 Office安全功能的状态描述
• 6.2 Office安全功能的证明
• 6.3 Office安全功能的算法设计
• 6.4 验证结论及方法
• 6.5 本章小结
• 第七章 结论
• 7.1 论文的主要成果
• 7.2 进一步的工作
• 致谢
• 参考文献
• 附录A 在读硕士期间发表的学术论文
• 附录B 在读硕士期间的科研经历