面包板的使用.pdf.pdf

2010信息技术与应用学术会议基于DTE策略的安全域可信隔离模型陈银镜,蔡勉,司丽敏,郭颖(北京J二业人学计算机学院,北京100124) 摘要:安全域隔离技术是构造可信系统的基本技术之一。本文运用可信计算的思想,在现有的安全域隔离模型的基础上,定义了安全域问信任关系,提出了域问可信通信的可信管道 Ydt$0,给出了安全域可信隔离模型的可信性状态,构建并形式化描述了基于DTE策略的安全域可信隔离模型,提供了验证模型可信的形式化分析方法,为安全域的可信隔离技术的实现和验证奠定了基础。关键字:安伞域可信隔离;可信管道:形式化中图分类号:TP309 文献标识码:A 文章编号: ASecurity Domain Trusted Separation Model Based on DTE Policy Chen Yinjing,Cai Mian,Si Limin,Guo Ying (School puter,Beijing University ofTechnology,Beijing 100124,China) Abstract Security domain isolated technology one basic technologies ofconstructing acredible thispaper,it uses Oiltheexisting security domain isolated model,it defines thetrusted relationship between thesecurity domain,puts forward thebelievable pipe mechanism munication between the domain,gives thecredibility state ofcredible isolation model ofsecurity domain, constructs and formal describes thesecurity domain credible isolationmodel based on the strategy ofDTE,provides aformal analysis method ofvalidatecredible model,laids the foundation fortheimplementation and verification ofbelievable isolation technology of security domain. Key words security domain trusted separation;assured pipeline;formalization. 1 引言可信计算的基本思想是:首先构建一个信任根,再建立一条信任链,从信任根丌始到硬件平台,到操作系统,再剑应用,一级认证‘级,一级信任一‘级,把这种信任扩展到整个计算机系统,从I叮确保整个计算机系统‘町信fl】。信任链传递到应用层时,不l一的应用程序具有不同的信任度,应用程序之问不做任何隔离的通信会使得信任度产生衰减,【21。 DTE(domain and typeenforcement)‘31以及其前身TE(typeenforcement)141作为有效实施细粒度强制访问控制的安全策略机制,自提出后已经被广泛的应用于多个系统和产品中进行安全配置拍“一1。安全域隔离技术作为构建可信系统的些本要求之一,是操作系统核心强制执行的一种访问控制机制,特点是通过严格的隔离阻止安全域内部和外部丰体非授权地访问被保护资源,从而实现保密性、完整性、最小特权等安全保护‘8·9‘。文献 86 2010信息技术与应用学术会议¨1给出安全域隔离模璎,但在可信系统构建中,要运用可信计算理论,构建安全域可信隔离模型,研究安全域问的信任关系和域问可信通信问题。本文的研究基于TCGn训和ISO/IEC?1对可信的定义,认为在操作系统运行中的一个实体可信,、输出以及动作序列。在实现其预期目标时,严格地按照预期进行,并得到预期结果。本文基于可信计算的思想,采用z形式规范语言,在借鉴安全域隔离模型埔’的基础上,定义并分析了安全域问信任关系及其性质,提出域问可信通信的通信机制,构建了安全域可信隔离模型,并给出了对安全域町信隔离模型进行形式化分析验证方法。 2安全域可信隔离模型文献ml使用z形式规范语占定义了系统状态,将DTE策略进行形式化建模,分析了域问信息流,给出安全域隔离模型。本文借鉴其对系统状态的定义,分析域问信任关系及其性质