中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
高安全等级操作系统形式化开发技术研究
作者: 李丽萍
答辩日期: 2008-01-15
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 安全操作系统 ; 形式化 ; 形式化安全策略模型 ; 形式化顶层规范 ; 求精 ; 安全体系结构 ; 微内核
其他题名: Research on Formal Development of High Security Level Operating System
摘要: 形式化开发安全保证技术是高安全等级操作系统的关键技术难点,国内尚未见相关研究成果。论文围绕高安全等级操作系统开发的整个生命周期,研究了安全策略模型和顶层规范的形式规范和形式验证技术及系统实现。取得以下几个方面的成果:第一,提出一种通用的状态机安全策略模型的形式规范构造方法。该方法基于Isabelle/HOL语言,对多种安全策略模型通用,且充分考虑了与功能规范的对应性分析的可行性。分析了方法的原理,并给出了SBLP模型的规范和验证实例;第二,提出一种形式化顶层规范的构造方法,并给出实施了SBLP模型的SecLinux文件系统的FTLS实例。首次形式化描述了与POSIX1003.1e兼容的ACL机制,并考虑了强制访问控制机制中客体间的信息流控制;第三,提出一种求精证明方法用于FSPM和FTLS之间的对应性分析。该方法包括一套基于Isabelle/HOL的求精规则,和一个引入了中间层的层次化求精方法。该方法大大降低了求精证明的难度。第四,针对支持动态多策略的需求,分析了当前几种典型安全体系结构在策略重用、策略共存方面的问题。提出一个新型的安全体系结构ELSM,引入模型组合器作为主模块实施模块堆栈管理和模块决策管理。策略决策基于访问控制空间形式规范方法,满足通用性。第五,给出了基于ELSM的FTLS的SecLinux文件系统实现实例。该系统基于Linux资源,为主流操作系统实现高安全等级提供了有意义的参考。第六,提出了一种支持多策略的基于微内核的安全体系结构,并基于此开发和验证一个微内核安全操作系统SecL4。该体系结构模块性强、结构清晰,解决了代码实现层难以形式化的难题。体系结构中的TPM保证了系统的引导和安全组件引入系统的可信性。
英文摘要: Formal development assurance is a critical technology to develop high security level operating system. This thesis centers on formal specification and verification technology and system implementation during whole lifecycle of system development. Several fulfillments are achieved: First, a general FSPM specification method is proposed, which is adapt to multiple security formal models and helpful to FTLS refinement proof. Its principle is analyzed and a SBLP model specification and verification is presented. Second, a FTLS specification method is proposed, and then a FTLS instance of SBLP on SecLinux filesystem is presented, in which POSIX 1003.1e ACL mechanism is formalized for the first time, also information flow control between objects is discussed in MAC mechanism. Third, refinement method for correspondence analysis between FSPM and FTLS is given, which include a series of Isabelle/HOL refinement rules and a layered refinement method. This method makes refinement proof resolvable. Fourth, to achieve the requirement of multi-policy, some current typical architecture and their problems on policy reuse and policy coexistence are discussed. Then a new architecture ELSM is proposed to support multi-policy. Its model combination work as main module to manage module stack and to make decision based on access control space method. Fifth, a SecLinux filesystem is implemented as FTLS refinement using ELSM. The system is based on Linux and provides a valuable reference to enhance mainstream operating system to meet requirement of high security level. Sixth, one secure architecture based on micro-kernel to support multi-policy is constructed and a micro-kernel secure operating system SecL4 is developed and verified. The architecture is strong-modularity and clear-structure so that code formalization is realistic. TPM is also used in this architecture to assurance system secure booting and secure components importing.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7106
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200218015003327李丽萍_paper.pdf(2034KB)----限制开放-- 联系获取全文

Recommended Citation:
李丽萍. 高安全等级操作系统形式化开发技术研究[D]. 软件研究所. 中国科学院软件研究所. 2008-01-15.
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