云计算环境信任链系统安全性理论研究

The security of chain of trust is the premise of security of cloud computing. However, there is no in-depth researches on security analysis for chain of trust of trusted cloud, which will affect the application of existing open systems such as cloud platform, virtualization platform..This project will research on theory and practice for chain of trust of cloud computing system based on non-interference theory and composition security theory. (1) As for issue of trusted measurement based on non-transistor non-interference model for chain of trust, this project will research the determination method between real behavior and expected behavior, and establish mathematical model and verification way. (2) As to problem of modelling security properties for multi-components in chain of trust system, this project will construct composiable information-flow model and put forward the verification method for security features of chain of trust in cloud computing system. (3) As for the flaw of DRTM chain of trust in cloud computing system, this project will solve the design security problem for DRTM system by using StatVerif calculus..Based on above work, this project will set up security analysis theory of chain of trust in trusted cloud computing system, and explore how to convert models to realistic application.

可信系统信任链是保证云计算环境安全的根本前提，但国内外尚没有对可信云信任链系统安全性进行全面深入的理论分析，这将影响现有开放系统的实际应用。.本项目拟以无干扰理论和组合安全理论为基础，围绕云计算环境下信任链安全性分析理论与实践展开研究。(1)针对非传递无干扰理论下的信任链可信度量理论问题，研究信任链真实执行与预期执行的一致性判定方法，建立可信计算信任链数学模型和验证方法。(2)针对基于组合安全理论的信任链多系统复合安全属性验证问题，通过构造可组合的信息流模型，给出云计算环境下多系统信任链安全属性验证方法。(3)针对云计算环境下DRTM信任链安全形式化分析问题，通过基于StatVerif演算的动态度量技术安全形式化建模、分析与验证，解决DRTM实际应用系统的设计安全性问题。.基于以上研究，将初步建立可信云平台下信任链安全性分析理论，并探索模型的实际应用。

基础设施安全是云计算安全的三个重要研究方向之一。可信计算技术是解决安全性和隐私性和增强云计算基础设施的重要方式。作为可信计算度量功能基础的可信链，缺少真正面向可信性的可信度量数学模型、缺少云计算环境下多系统组合安全理论、信任链规范的安全性没有得到充分论证、信任链关键机制需要进行安全性分析等。研究云计算环境下信任链的理论、建模、分析、验证等问题是十分必要的。. 本项目以信任链技术在可信云中的作用为应用导向，以无干扰理论和组合安全理论为基础，研究了可信云信任链的可信度量数学模型、复合安全属性验证和动态度量DRTM安全形式化分析机制，研究了导致当前云计算环境下信任传递不可靠的特征和机理，给出了动态行为可信的判定等式、基于状态递归等价的行为可信性判定定理；针对理论的实践应用问题，根据无干扰模型的定义，选择系统调用作为基本原子动作，将软件真实行为定义为原子动作的序列，并根据系统调用所属安全域之间的无干扰关系定义预期行为规范。针对可信计算的完整性报告协议（IRP）在实际应用过程中存在的安全问题，对形式化描述语言StatVerif进行了语法扩展，增加了与完整性度量相关的构造和析构算子，给出了安全增强后的完整性报告协议，在协议应答者与平台配置证明信息之间建立了授权约束，解决了实际交互过程中应答者提交平台配置信息前存在的命令接口攻击，以及提交平台配置信息后存在的中间人攻击，有效提高了完整性报告协议的安全性。揭示了信任链理论和技术在云计算生产和生活中运用的科学规律，探索开发出了一套简单有效、能够确实应用于现实云计算环境中的信任链构建机制，可解决当前可信云及其云计算产业发展的理论瓶颈，为我国云计算安全的科研和产业发展做出了有益的探索。