| 题名 | 安全操作系统开发中的形式化技术应用研究 |
| 作者 | 陈坤 |
| 学位类别 | 博士 |
| 答辩日期 | 2007-06-08 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 软件研究所 |
| 关键词 | 安全操作系统 形式化分析 状态机模型 测试用例生成 Isabelle工具 |
| 其他题名 | Research of Formal Technology Application in Secure Operating System Development |
| 中文摘要 | 近年来，形式化方法——即在计算机系统和软件的规范、设计和构造中使用基于数学模型和离散数学的技术的工具的方法，被广泛应用于高等级安全操作系统的开发过程中。TCSEC的B2级和CC的EAL5级中规定了高安全等级操作系统必须使用形式化技术进行分析验证。 从形式化的角度确认一个操作系统是安全的，是指证明它满足某一给定的以安全模型形式描述的安全策略。只有有效保证从设计者到用户都相信模型本身正确无矛盾（验证Verification），而实现代码准确地体现了模型（确认Validation）时，该操作系统才可以说是安全的。 本文首先介绍了几种有代表性的安全操作系统模型，以及结合了几种模型优点的可信进程模型。并且和其他组员共同进行形式化工具的调研，选定了Isabelle作为我们接下来形式化分析的环境。 接下来依据上述验证确认两部分的思想，首先结合安全操作系统状态机模型的特点，提出了一套直观的使用形式化工具Isabelle对其进行描述的方法。并且通过实际验证一种典型的状态机模型——可信进程模型，总结出了有效的使用Isabelle形式化设计、分析、验证模型的策略，即实现了对模型本身的验证；接着根据前人提出的一套使用Isabelle的基于DNF（析取范式）来提取测试用例的方法，进行了基于DBLP模型的安全操作系统的测试用例自动生成，并从安全为导向的视角，分析了这种方法在安全操作系统开发过程中的应用特性,即对测试一个安全操作系统是否正确实现了模型功能的确认工作做出了探索。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 60 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6004]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 陈坤. 安全操作系统开发中的形式化技术应用研究[D]. 软件研究所. 中国科学院软件研究所. 2007. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论