【作者】 黄勇；

【导师】 潘雪增； 平玲娣；

【作者基本信息】 浙江大学 ， 计算机科学与技术， 2009， 博士

【摘要】 随着计算机和因特网的应用迅速普及与发展,信息安全已日益成为人们关注的焦点。本论文以国家信息系统等级保护标准为主要依据,基于进程代数等形式化方法,对安全模型设计、安全信息流分析以及原型系统实现等重要理论和实践问题展开了研究,取得了如下研究成果:(1)建立了支持动态调节的保密性和完整性统一模型。为了满足兼顾信息保密性和完整性保护的安全需求,本文提出一种基于多级安全策略的动态统一模型(简称DMUM)。模型以保密性和完整性作为安全标识的两个维度,主体当前安全标识根据客体安全标识和主体访问权限的历史过程进行动态调整,一方面实现了BLP模型和Biba模型的有机结合,另一方面通过对非可信主体实施安全级的非管理动态调节,使其无需完全依赖于可信主体的管理调节,从而能够减少一些无法预料的安全风险。同时,给出了可信主体的形式定义,推广了多级可信主体概念,使得可信主体只在指定范围内实施读写权利,从而在多级安全策略范围内满足可信主体的最小特权原则。通过一个实例说明了模型的有效性和可用性。(2)提出了基于进程代数的非传递无干扰时间信息流分析方法。为了揭示安全降密等非传递安全策略系统中的隐蔽时间信息流,本文基于进程代数方法分析了非传递无干扰时间信息流的安全属性。将可信域的概念引入时间安全进程代数(tSPA),扩展了tSPA的表达能力,使其能模拟实际系统中的可信部分。接着以tSPA为工具将非传递无干扰模型由确定系统推广到诸如实时系统之类的时间系统上,提出了非传递时间互拟强无干扰(Ⅰ_tBSNNI)和非传递时间互拟复合不可演绎(Ⅰ_tBNDC)安全属性。为了揭露出Ⅰ_tBNDC在动态环境中不能暴露的安全隐患,提出了要求系统所有可达状态都满足Ⅰ_tBSNNI的Ⅰ_tSBSNNI属性。以一个扩展的时间系统实例分析说明我们所提出的方法的有效性。(3)给出了面向隐蔽通道构建的多级安全形式定义。针对目前多级安全策略形式定义与安全目标关系不清晰的问题,本文形式描述了面向隐蔽通道构建的多级安全性。由于隐蔽通道是安全系统要尽量避免的安全问题,因此,从隐蔽通道构建的角度去定义安全性质会更有助于人们对系统安全本质问题的深入理解。鉴于面向隐蔽通道构建的隔离安全性质不具实用性,我们基于可传递性和非传递性安全策略的特点,将可信域概念引入该理论框架,提出了两个关于传递与非传递安全性质的推论,并给出了相应的证明。在上述理论研究成果的基础上,本文最后介绍了基于可信计算平台的高安全级操作系统原型(图灵安全操作系统)的设计与实现。包括原型系统的设计思路以及功能划分;强制访问机制、恶意代码防护机制、可信恢复以及隐蔽信道处理等若干关键技术的实现方案;功能和性能测试方案与结果等。更多还原

【Abstract】 With the widespread application and rapid development of computer and network technology, information security has increasingly become people’s focus point. Following the national requirements of the classified criteria for information security, this paper studies about the theory of developing high level security system, which consists of security policy model design, information flow analysis and etc. In this paper, our research work focus on the following four interrelated aspects.(1) Present a dynamically modified union model combining confidentiality and integrity. To meet the security need of information confidentiality and integrity, we present a dynamic union model based on MLS policy (called DMUM). The two dimensions of secure model are composed of confidentiality and integrity respectively, of which history label is introduced and each subject’s access range is adjusted dynamically, thus it leads to a compatible integration of BLP model and Biba model. With the unmanaged dynamic adjustment of secure label, untrusted subjects need not totally dependent on the managed adjustment by trusted subjects, which reduce some unexpected security risks. The formal definition of trusted subject is introduced, and also the paper presents the concept of multilevel trusted subject who has the read and write right among specifying access range. This notion of multilevel trusted subject will give a better support of least privilege principle within the MLS policy framework. Finally, examples are illuminated to show the effectivity and usability of this model.(2) Propose an analysis method of intransitive timed information flow based on process algebra. To reveal timing covert information flow of intransitive secure policy, we analyze the real-time intransitive information flow security properties based on process algebra. To simulate trusted parts of real systems, the concept of trust domain is introduced into Timed Secure Process Algebra (tSPA). Based on tSPA, the intransitive noninterference information flow security model is extended from deterministic systems to timed systems such as real-time systems. We present Intransitive Timed Bisimulation Strong Nondeterministic Noninterference (I_tBSNNI) and Intransitive Timed Bisimulation-based Nondeducibility on Composition (I_tBNDC) based on timed weak bisimulation equivalence. In order to discover the potential secure problem that I_tBNDC cannot discover in dynamic context, the I_tSBSNNI property is proposed, which requires that every reachable state of the system must satisfy I_tBSNNI. Furthermore, we analyze intransitive information flow security properties of a real system in a time setting.(3) Provide a new definition of multilevel security based on the construction of covert channels. Aiming at the main problem that the link between the formal definition of multilevel security and security goal is not always clear, we propose a new definition of multilevel security based on the construction of covert channels. Covert channels are the security problem that the security system must avoid as far as possible; therefore, it will be more helpful to understand the nature of system security from the perspective of implementing a covert channel to define multilevel security. Due to the fact that separability property based on the construction of covert channels is not practical, we introduce the concept of trusted domain to the theoretical framework initiated by the characteristics of transitive and intransitive security policy. Following that two intuitive propositions with the corresponding proof are proposed.On the basis of research results mentioned above, we introduce the design and implemention of a high secure operating system (called Tuling SecOS) base on the trusted computing platform. Firstly we give an overview on the design principles and functional modules of prototype system; then intruduce several key technologies such as mandatory access mechanisms, malicious code protection mechanism, trusted recovery, as well as identification and disposition of covert channels in detail; and at last, the functinal and experimental results show the practicability and feasibility of the prototype system.更多还原