本文面向可信执行环境（TEE）中飞地程序的安全性问题，特别是状态连续性（State Continuity）的验证，提出了一种形式化验证方法。状态连续性指飞地程序在执行过程中，即使遭遇异常中断、迁移或恶意系统软件干扰，其内部状态仍能保持一致和完整。作者基于程序逻辑和定理证明技术，构建了状态连续性的形式化模型，定义了验证规则，并可能使用了自动化工具进行验证。该研究有助于从数学上保证飞地程序的状态安全，防止回滚、重放等攻击。论文的主要贡献包括状态连续性属性的精确刻画、验证框架的设计与实现，以及基于典型飞地应用的案例研究。这项工作对TEE安全研究者和开发可信应用的安全工程师具有重要参考价值。

本文提出 NARRATOR，一个面向云环境中可信执行环境（TEE）的状态连续性保护方案。TEE 如 Intel SGX 和 AMD SEV 能够保护运行时代码和数据的机密性与完整性，但缺乏对状态连续性的原生支持：当 TEE 实例崩溃、迁移或休眠后，其内部状态可能丢失或无法安全恢复。现有方案如远程证明和状态加密存在性能开销大或安全假设强的问题。NARRATOR 通过引入轻量级的、基于硬件的单调计数器与持久化加密存储，实现了高效且安全的状态输入输出（state I/O）机制。核心创新包括：(1) 设计了一种无需依赖外部可信第三方即可验证状态新鲜性的协议；(2) 利用 SGX 的密封（sealing）和单调计数器，保证了状态的持久性和单调递增；(3) 在状态恢复时仅需少量通信轮次，避免了全量重新计算。实验评估在 Intel SGX 平台上进行，测试了多种云应用（如键值存储、机器学习推理），结果显示 NARRATOR 在状态保存与恢复操作中引入的延迟在毫秒级，性能开销远低于现有方案（如基于远程证明的恢复）。该工作为构建弹性、可迁移的 TEE 应用提供了实用基础，尤其适用于需要长期运行或跨节点迁移的云原生工作负载。