基于验证操作系统内核的可信计算环境关键技术研究

In open networks, information systems are facing more and more serious security threats. By combining the software and hardware, Trusted Computing is capable of supporting trusted execution environment for software applications. However, as the serious vulnerability problem in operating system kernel layer of the software runtime environment, these security mechanisms cannot even guarantee their own reliability in open networks. We propose to research in the area of Trusted Computing Environment based on certified operating system kernel, in these following directions: (1) The general principles and methodologies for designing and implementing certified operating system kernel with trusted computing support; (2) The key mechanisms for constructing trusted execution environment of software applications, with certified operating system kernel and trusted computing; (3) Formal verification of trust chain based on security chips, in certified OS kernel. By taking advantage of the recent progress in formal verification on operating system kernel, this program will greatly advance the research area of certified operating system kernel with Trusted Computing support.

在开放网络环境下,信息系统面临日益严重的安全威胁。可信计算技术可以通过软硬件结合的机制，为应用程序的运行提供可信计算环境的支撑。然而在现有的软件运行环境中，由于操作系统层的缺陷，仍然难以保证基于可信计算的安全机制自身的可靠性。为此，本项目将会针对基于验证操作系统内核的可信计算环境在以下方面开展研究：（1）设计和构造基于可信计算机制的验证操作系统内核的通用原理和方法；（2）基于验证操作系统和可信计算机制构建可信软件运行环境的关键机制；（3）在验证操作系统内核中，针对基于安全芯片的可信计算信任链的形式化验证。本项目将基于已有针对操作系统内核形式化验证的最新进展，推动融合可信计算技术的验证操作系统内核的发展。

针对开放网络环境下软件运行环境所面临的问题，本项目开展了一系列针对可信计算技术研究进展的调研分析，并对可信计算在开源操作系统中的实现进行了系统分析，持续跟踪和调研了学术界在可信计算研究的进展，也探索了可信计算在云计算、容器等环境中的应用进展。本项目研究了基于验证操作系统内核构造和保障可信计算环境的关键理论和方法，探索如何在实际的验证操作系统内核中设计、实现和验证基于可信计算技术的安全保护机制，建立起从TPM到应用程序的可靠信任链。本项目尝试了一系列创新性技术研究，具体如下： .结合CertiKOS探索和尝试了基于可信计算的验证操作系统内核的构造方法，并结合虚拟化技术实验了利用可信计算技术增强的可验证操作系统内核需要的关键技术，在CertiKOS上尝试了TPM驱动的集成。.探索和尝试了针对内核中可信计算信任链的验证框架，以支持对基于TPM的内核设备驱动进行验证，并利用组合验证框架对可信计算信任链的验证。.基于CertiKOS针对时间隐秘通道(Time side channel)的防御进行了研究，并提出了一种基于确定状态虚拟机的方式来降低时间隐秘通道的信息泄露频率。.作为支持云计算环境下的引用安全可信执行环境的研究扩展，进一步的探索和研究了基于SDN的云安全解决方案和云安全资源池的核心技术，并探索和尝试了面向容器运行环境的安全增强机制，并发表了相关论文。 .针对云计算环境软件缺陷的弱点，开展了针对云端服务基于缺陷的服务选择机制研究，并应用了可信计算相关的技术来保障云服务组合机制的可靠安全，相关工作发表在ICWS 2015。.针对大数据安全的核心算法进行了探索研究，并联合进行了一系列的核心算法优化工作，发表了相关论文。.本项目开展了一系列的相关研究，并与多所高校、科研机构和企业进行了联合研究协作，取得了一系列的研究成果，支持发表了10多篇高水平学术论文。