本文提出 Pandora，一种面向 Intel SGX 安全飞地运行时的符号执行验证工具。Intel SGX 技术通过硬件级飞地保护应用免受恶意操作系统攻击，但近年来出现了多种针对 SGX 飞地的攻击技术，导致屏蔽运行时（shielding runtime）需要频繁打补丁，验证工作复杂且快速变化。Pandora 的核心创新在于首次实现了对飞地运行时本身的可信、运行时无关的符号执行，它精确模拟被验证的飞地二进制代码，而非依赖抽象模型。Pandora 具备三项原则性基础：攻击者输入的精确污点跟踪（标记来自非可信 OS 的所有数据）、精确的符号飞地内存模型（支持分页、异常和中断等 SGX 特殊机制），以及可插拔的漏洞检测插件（如指针对齐、缓冲区溢出等）。作者在 11 种不同的 SGX 屏蔽运行时上部署了 4 个检测插件，覆盖多种漏洞类型。实验表明，Pandora 能自主发现 200 个新的和 69 个已知的脆弱代码位置。值得注意的是，Pandora 是首个能够对现实世界 SGX 飞地运行时进行大规模生态系统级指针对齐软件缓解措施评估的工具。本文工作对于 SGX 安全性的系统性验证具有重要推动作用。

该论文针对可信执行环境（TEE）中的密文侧信道攻击提出了Cipherfix，一种纯软件的二进制加固方案。背景：TEE依赖硬件辅助安全保证，但主存加密存在确定性行为，导致密文侧信道（如Cipherleaks攻击），攻击者可通过分析密文模式推断秘密数据。现有防御手段（如常数时间代码）和硬件修复均无法有效防御。Cipherfix的核心思路是：通过污点追踪结合静态与动态二进制插桩，识别程序中与秘密数据相关的敏感内存位置；在数据写入内存前，对秘密数据进行随机掩码操作，破坏密文中的依赖模式，即使内存加密仍是确定性的，也无法被攻击者利用。该方法无需重新编译，可直接加固现有二进制程序。实验表明，Cipherfix能有效保护多种常数时间实现（如AES、RSA等），且性能开销在可接受范围内（论文中展示了具体开销数据）。主要贡献：首次提出针对密文侧信道的软件级、可即插即用的缓解方案，填补了硬件修复前的防御空白。适合TEE安全研究人员、云服务安全工程师及系统软件开发者阅读。

这篇论文针对公共机构在资助评审中引入大语言模型（LLM）作为决策辅助工具时面临的治理难题：模型和评分标准不能暴露给申请人以防他们针对优化，但评审过程必须可审计、可质疑且可问责。作者提出了一种基于可信执行环境（TEE）的架构，通过远程证明技术协调上述矛盾。该架构允许外部验证者检查使用的模型、评分规则、提示模板和输入表示，同时不向申请人或基础设施操作者暴露模型权重、专有评分逻辑或中间推理过程。核心成果是“经证明的评审包（attested evaluation bundle）”：一个包含签名和时间戳的记录，关联原始提交哈希、规范化输入哈希、模型与评分规则度量以及评审输出。论文还考虑了场景特定的提示注入风险：申请人控制的文档可能包含隐藏指令影响LLM评估。为此，论文设计了规范化和净化层，用于标准化文档表示并在推理前记录可疑变换。作者将设计置于机密AI推理、可证明AI审计、零知识机器学习、算法问责制和AI辅助同行评议的背景下进行定位。论文的声明刻意狭窄：远程证明不能证明评审是公平或科学正确的，但可以使评审过程的部分环节变得外部可验证。

这篇论文研究了在低功耗微控制器（例如ARM TrustZone-M）上，实时操作系统（RTOS）的时间保持与可信执行环境（TEE）之间的冲突问题。在TrustZone-M架构中，安全世界和非安全世界共享中断控制器等资源。通常，非安全子系统运行RTOS和实时应用，而安全子系统运行预定义的安全操作（如加密），称为可信计算服务。许多RTOS依赖周期性中断（SysTick）来推进其时间概念，这对于维护实时行为至关重要。然而，某些可信计算服务的安全性要求相对于非安全子系统（RTOS所在侧）具有原子性，这需要禁用中断以防止被非安全世界打断，从而阻止了SysTick的处理。这导致RTOS丢失时钟滴答，时间感知出现偏差，破坏实时行为。本文首先刻画了这一冲突，然后提出了一种安全驱动的同步机制：安全世界测量经过的时间，并在重新启用中断并恢复非安全系统执行之前，通过无侵入地更新RTOS的时间保持数据结构（补偿错过的滴答数）来补偿非安全RTOS。该方法恢复了跨世界的一致、单调的时间概念，使得可信计算服务与RTOS能够在微控制器上安全共存。重要地，该方法无需修改底层RTOS，且不引入显著的运行时开销。作者通过实验验证了其有效性。

该论文针对审计专有数据语义属性时的隐私与透明矛盾，提出了一种名为“Agentic Witnessing”的框架。传统方法如零知识证明（ZKP）适用于精确代数约束，但难以验证定性、非结构化属性（如代码库中的逻辑）。该框架将验证从可证明执行扩展到可证明推理，由验证者、证明者和审计者三个智能体组成。验证者被允许提出有限数量的简单布尔问题（真/假），审计者（基于大型语言模型LLM）运行在可信执行环境（TEE）中，通过模型上下文协议（MCP）动态检查证明者的私有数据集，产生是/否结论并附加密审计记录：一条签名哈希链，将推理轨迹绑定到原始数据集和TEE的硬件信任根。论文在21篇同行评审计算机科学论文的GitHub代码库上演示了自动化工件评估，例如验证代码库是否实现了论文描述的系统。将源代码视为私有数据，验证了对应出版物中描述的五项高层属性。实验表明，这一TEE驱动的智能体审计机制能有效实现隐私保护监督，将定性验证与数据披露需求解耦。