一种基于无干扰模型的信任链传递分析方法  

A Formal Method Based on Noninterference for Analyzing Trust Chain of Trusted Computing Platform

作　　者：张兴[1,2] 黄强[3] 沈昌祥[1] 

机构地区：[1]信息工程大学电子技术学院,郑州450004 [2]北京工业大学计算机学院,北京100022 [3]海军计算技术研究所,北京100036

出　　处：《计算机学报》2010年第1期74-81,共8页Chinese Journal of Computers

基　　金：国家"九七三"重点基础研究发展规划项目基金(2007CB311100);国家"八六三"高技术研究发展计划项目基金(2006AA01Z440)资助

摘　　要：基于可信计算组织(TCG)的完整性度量只能保证组件没有被篡改,但不一定能保证系统运行可信性.其问题在于,当组件运行时,受其它组件的干扰,出现非预期的信息流,破坏了信任链传递的有效性.文章在分析可信计算平台的信任模型基础上,基于无干扰理论模型,提出了一种分析和判定可信计算平台信任链传递的方法,用形式化的方法证明了当符合非传递无干扰安全策略时,组件之间的信息流受到安全策略的限制,隔离了组件之间的干扰,这样用完整性度量方法所建立的信任链才是有效的.The integrity measurement of TCG can only insure that the components of a computing platform are tamper-proofed,which is not enough for avoiding the interference between components at runtime for building the trust chain.The interference of other components results in the unexpected information flow.The trust model of Trusted Computing Platform is analyzed in this paper.Based on the intransitive noninterference model,a formal method of analyzing the trust chain transfer is proposed.It formalized specifies the security policy isolating the interference between components that can make the trust chain valid after integrity measurement.

关 键 词：可信计算 信任链 无干扰模型 安全策略 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]