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