中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
安全操作系统开发中的形式化技术应用研究
作者: 陈坤
答辩日期: 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模型的安全操作系统的测试用例自动生成,并从安全为导向的视角,分析了这种方法在安全操作系统开发过程中的应用特性,即对测试一个安全操作系统是否正确实现了模型功能的确认工作做出了探索。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6004
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200428015029080陈坤_paper.doc(504KB)----限制开放-- 联系获取全文

Recommended Citation:
陈坤. 安全操作系统开发中的形式化技术应用研究[D]. 软件研究所. 中国科学院软件研究所. 2007-06-08.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[陈坤]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[陈坤]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace