可信计算环境测评理论和技术研究

随着可信计算平台在国家重要信息系统和重大工程中的广泛应用，提高可信计算平台软件及其环境的可信性已经成为了国家信息化发展的战略需求，也是可信软件基础研究和发展的必然趋势。针对软件环境可信性验证和度量的科学问题，本项目重点研究基于TPM/TCM的可信计算环境测评理论与方法，为改善国家重大应用中的软件可信性提供科学支撑。首先对TPM/TCM安全芯片和可信计算协议形式化建模，建立以密码算法协议为基础，以安全芯片为核心的可信计算环境测评模型；然后针对可信计算协议匿名性、隐私性等安全属性难以分析的问题，提出基于零知识证明的等价关系分析和协议状态规约的方法，并改进协议验证工具对其进行机械化分析；最后通过TPM/TCM安全功能分析提出基于测试用例等价类划分的自动化测试方法，并进一步研制涵盖算法检测、协议验证以及安全芯片测试等的可信计算环境综合测评系统，验证以上可信计算环境测评方法的科学性和有效性。

可信计算是保障网络空间安全的重要支撑技术，可信计算平台已经在信息技术中得到广泛应用。可信计算技术的快速发展和应用，迫切需要展开对可信计算环境测评理论和技术研究。可信计算环境涉及算法协议、安全芯片、可信计算平台等，目前的可信计算测评还缺乏有效理论方法和实用技术指导，现有的测评技术还无法直接应用于可信计算环境测评。.本课题针对可信计算环境的软件可信性分析和验证这类科学问题，重点研究基于TPM/TCM的可信计算环境检测评估、安全性分析的理论与方法，以密码设计分析、形式化分析理论、自动化检测模型为理论基础，研究由算法协议、环境接口分析、产品测评认证为核心的可信计算测评关键支撑技术，最后针对可信计算环境、可信计算产品研制相应的测评工具，并在国内重要测评机构开展测评示范应用。.在项目开展期间，课题组在算法协议、API安全分析，以及测评系统设计和推广方面取得了一系列重要研究成果：提出了针对移动可信设备的流密码算法条件掩码攻击，设计了适用于可信芯片场景的高效安全MAC算法等新型算法；使用形式化方法对新一代的可信安全芯片接口进行了安全性分析，发现新规范在DAA接口、授权接口、认证密钥协商功能接口方面存在的安全隐患，该结果已被TCG国际标准组织所采纳，对TPM2.0标准的修订产生了重要影响；设计了基于有限状态机理论的安全芯片测评方法，实现了相应的测评系统，并将该测评系统应用于数家国家权威信息安全测评中心，取得了良好的社会应用效果。项目的代表性成果发表于Crypto、EuroCrypt、AsiaCrypt、IEEE T PARALL、THEOR COMPUT SCI等国际会议和期刊上。本项目总共发表SCI/EI学术论文66篇，申请国内专利12项，软件著作权14项，发布《可信密码模块符合性测试规范》国内密码行业标准1项，完成《可信密码模块保护轮廓》和《可信计算直接匿名证明规范》可信计算标准草案2项，完成“可信计算环境理论和技术研究报告”技术报告一份。.上述研究成果对可信计算环境测评理论与方法、可信计算产品验证、可信计算产业发展等都具有重要的意义：丰富了可信计算环境测评模型理论，提高了我国可信软件测评理论研究水平；突破了可信计算环境分析和测评关键技术，为可信计算产品测评提供了技术支持；促进了自主可信计算产品的成熟，带动了我国自主可信计算产业的发展。