动态远程证明协议及其形式化分析

辛思远，赵 勇，王 婷

（1.解放军信息工程大学 电子技术学院，河南 郑州450004；2.北京工业大学 计算机学院，北京100124；3.中国科学院软件研究所 信息安全国家重点实验室，北京100049；4.65047部队，辽宁 沈阳110000）

0 引 言

远程证明是可信计算技术的重要内容，利用可信平台模块 （trusted platform module，TPM）的可信度量与报告功能向远程验证方证明计算平台的可信状态，远程证明在开放环境下的网络应用中具有良好的应用前景。现有的远程证明研究当中，基于配置的远程证明［1－2］、基于属性的远程证明［3－4］等方法都是使用计算组件启动前的静态度量，在计算组件加载前度量其映像文件的完整性，证明的内容实质上是计算平台启动过程中的历史信息，即证明计算平台最近一次启动的固件、软件配置或其属性。然而，当计算平台启动运行至操作系统、应用程序等软件层之后，其动态性显著增强，操作系统及各种应用程序并发运行，程序运行可能受到非预期干扰，启动时刻的状态信息不足以证明程序当前的状态可信。平台的各层软件在运行过程中可能受到缓冲区溢出［5］、DMA攻击［6］等动态的攻击行为，使系统进入非预期的状态，此时再将启动时刻的平台状态信息报告给远程平台会造成失效的远程证明。此外，攻击者也可在执行完恶意程序之后重启机器，将机器重新启动到正常的状态，此时进行远程证明也无法发现异常［7］。因此，证明计算平台的当前实时可信状态对于建立平台间的动态信任关系具有重要意义，是远程证明亟待解决的重要问题。……