💻 computer science

Bootstrapping Mutual Attestation with Kleene's Second Recursion Theorem

本文通过应用克莱尼第二递归定理来构建能够仅凭内置数据相互重建并验证彼此精确源代码的节点，从而解决了相互证明的无限回归问题，进而消除了在不同计算架构之间对可信第三方或外部参考值的需求。

原作者： Takuma Imamura

发布于 2026-08-24

📖 1 分钟阅读☕ 轻松阅读

原作者： Takuma Imamura

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在安全计算领域，有一个根本性的需求，即证明一台计算机程序确实如其所声称的那样。这个过程被称为远程度量（remote attestation），它是数字世界中安全人员在允许进入受限建筑前检查驾驶执照的行为。保安会将照片和详细信息与一份关于有效执照应有的样子之信任数据库进行对比。如果细节匹配，此人即可进入。在数字领域，一个计算机程序会生成一个唯一的指纹，称为“度量值”（measurement），该值会与验证者持有的参考值（一个已知的、预期的指纹）进行比较。当一方检查另一方时，这套系统运作得非常完美；但当两台或多台计算机需要同时互相检查时，它就会撞上一堵逻辑之墙。如果计算机 A 需要知道计算机 B 的指纹来验证它，而计算机 B 也需要知道计算机 A 的指纹来验证它，那么双方都无法在已经拥有答案之前开始这个过程。这创造了一个循环依赖：每台机器都在等待对方提供它开始验证所需的证明。

位于日本名古屋的 Acompany Co., Ltd. 的研究人员找到了一种方法，可以在不依赖中央权威机构或预先存在的信任代码列表的情况下打破这个循环。他们并没有将这个问题视为一个安全谜题，而是将其视为一个逻辑和自我引用问题。通过应用被称为克莱尼第二递归定理（Kleene's second recursion theorem）的数学原理，他们证明了一组计算机可以通过编程，使其自身的内存中包含其他所有成员的精确源代码。这使得每台机器都能从零开始重建其同伴的代码，实时计算出正确的指纹，并在无需向外部请求答案的情况下验证对方的身份。该团队构建了工作原型来证明这一概念，展示了两台安全计算机如何仅利用自身携带的数据便成功实现了相互的完整性验证。

问题的核心在于现代安全环境（如可信执行环境，Trusted Execution Environments）的本质，这些环境是隔离的空间，可以在其中处理敏感数据而无需担心被窥视或篡改。在典型的设置中，单台计算机向服务器证明其可信度。服务器持有批准的代码指纹列表，并将计算机的报告与该列表进行比对。然而，在一个多台计算机必须协作完成机密任务的去中心化网络中，每台机器既是检查者，也是被检查者。如果它们试图将伙伴的预期指纹硬编码到自己的软件中，就会陷入无限循环。为了知道伙伴 B 的指纹，计算机 A 必须知道 B 的代码。但 B 的代码包含了 A 的指纹，而获取 A 的指纹又需要知道 A 的代码，而 A 的代码又包含了 B 的指纹，如此循环往复，永无止境。以往解决这一困境的方法包括引入一个受信任的第三方来分发指纹，或者依赖特定的硬件特性在启动时注入这些数值。这些方法虽然有效，但它们重新引入了信任中心点，或者将解决方案与特定类型的硬件绑定，从而限制了其应用范围和方式。

研究人员通过将一组计算机视为一个单一的、互连的系统，提出了另一条路径。他们意识到，如果每台计算机都能从一组共享指令中生成其同伴的代码，那么循环依赖就可以得到解决。利用一种允许程序引用其自身源代码的计算机科学概念，他们设计了一种方法，将一组程序转化为一组自包含的单元。每个单元都携带了整个程序家族的完整描述。当一台计算机启动时，它会读取这种内部描述，重建其伙伴的精确源代码，然后计算出伙伴的指面值。由于重建过程是在内部完成的，计算机不需要信任外部列表；它只需根据已拥有的数据计算出答案。这种方法消除了对中央权威机构的需求，并且可以在不同的安全硬件类型上运行，无需对底层的安全工具进行更改。

为了证明这一理论，团队创建了两个工作演示。第一个侧重于直接测量运行中代码的系统，例如标准的 Linux 系统。他们构建了一个名为 PyReflect 的工具，该工具可以接收代码模板并自动生成具有自我引用能力的程序。在测试中，由软件安全模块支持的两台虚拟机成功交换了验证报告。每台机器都重建了对方的代码，计算了预期的指纹，并确认了对方正在运行正确的软件。第二个演示针对的是测量编译后的构建产物（build artifact）的系统，例如 AWS Nitro Enclaves，这些是专门的安全容器。在这里，过程更加复杂，因为计算机不仅必须重建源代码，还必须精确地重建最终的可执行文件。他们开发了名为 NixReflect 的工具来处理这一过程。在实验中，两个安全隔离区被启动，每个隔离区都独立地从其自身内存中存储的数据里重建了对方的整个镜像。随后，它们计算了重建镜像的指纹，并将其与对方报告的指纹进行对比。结果完全匹配，证明了机器可以仅凭其内部数据推导出正确的参考值。

研究人员还测量了这种方法的成本。在安全隔离区的案例中，重建对方镜像的过程比仅仅计算代码哈希值的过程要慢得多。在他们的特定测试案例中，重建和构建过程耗时约 6.8 秒，而简单的哈希计算耗时不到 0.1 秒。这种差异预计会随着应用程序变得更加复杂而增大，因为计算机必须遍历整个依赖链来重建软件。尽管存在这种时间成本，实验仍证实了该方法是可行的，且不需要任何新硬件或受信任的第三方。团队指出，对于更复杂的系统，可以将重建过程卸载到部署前的安全构建环境中，从而降低运行时成本，但这会引入关于构建环境本身的一套新的信任假设。

这项工作的意义在于它能够解决长期阻碍完全去中心化安全计算的逻辑死锁。通过展示可以通过自包含重建实现相互度量，研究人员为那些不信任单一实体的点对点网络提供了一条前进的道路。该方案是架构无关的，这意味着它可以应用于各种类型的安全硬件，而无需对硬件的安全栈进行定制化修改。它依赖于计算的基本属性而非特定的硬件特性，使其成为未来机密计算的一种通用工具。虽然目前的原型只是概念验证演示，但它们确立了参考值引导（reference-value bootstrapping）问题可以在没有受信任第三方的情况下得到解决，为更强大、更独立的网络铺平了道路。

技术摘要：利用克莱尼第二递归定理实现引导式相互度量（Bootstrapping Mutual Attestation）

1. 问题陈述

本文探讨了相互度量中的参考值引导问题（reference-value bootstrapping problem）。在去中心化或点对点系统中，节点必须相互验证彼此的完整性（同时扮演证明者 Attester 和验证者 Verifier），每个节点都需要其对等节点的参考值（即对等体代码的哈希值）。

一种简单的解决方案——将对等体的参考值硬编码到节点的代码中——会因为**无限回归（infinite regress）**而失败。如果节点 A 嵌入了节点 B 的参考值（B 代码的哈希），且节点 B 嵌入了节点 A 的参考值，则这些依赖关系会形成一个循环且无法终止的链条。现有的解决方案通常通过以下方式解决此问题：

依赖可信第三方（TTP）来分发参考值。
使用特定于架构的凭据或外部授权列表。
将配置置于度量范围之外。
利用特定硬件架构特有的度量机制。

作者旨在不依赖 TTP、不使用外部提供的参考值，且以一种与架构无关的方式，仅利用现有的软件栈和度量机制来解决这一问题。

2. 方法论

作者将引导问题重新表述为一个相互不动点方程组（system of mutual fixed-point equations），并利用**克莱尼第二递归定理（Kleene's Second Recursion Theorem）**来求解。

理论基础

模型： 一个由 $k$ 个节点组成的组被建模为：每个节点 $i$ 计算一个部分函数 $f_i$ ，该函数取决于该组内所有节点（包括其自身）的源代码 $\vec{e} = (e_1, \dots, e_k)$ 。
方程： 目标是找到一组源代码 $\vec{e}$ ，使得对于每一个 $i$ ，由 $e_i$ 计算出的函数都等价于 $f_i(\vec{e}, -)$ 。
克莱尼第二递归定理： 本文利用了该定理的同步形式（推论 2.3），它保证了对于任何一组可计算行为 $f_1, \dots, f_k$ ，都存在一组可计算的索引（源代码） $\vec{e}$ 来满足这种相互依赖关系。
构造性方法： 该定理意味着存在一个转译器（transpiler），能够自动从一个将对等体源码视为自由变量的模板中，生成这些相互引用的程序。

实现策略

作者根据目标架构执行度量的方式，提出了两种不同的实现方案：

A. 直接代码度量（例如 Linux IMA, TPM）

机制： 架构度量部署的原始代码（例如对文件进行哈希）。
解决方案： PyReflect，一个 Python 转译器。
- 它接收一个引用彼此源代码的模板。
- 它将整个源代码族序列化为一个单一的共享数据块（data blob），并将其嵌入到每个节点中。
- 在运行时，每个节点从该数据块中重建对等体的精确字节级源代码，并直接计算其哈希值。
- 这消除了对构建步骤的需求；“度量”仅仅是对重建后的源代码进行哈希。

B. 构建产物度量（例如 AWS Nitro Enclaves, SGX, 机密虚拟机）

机制： 架构度量的是构建产物（例如 Enclave 镜像文件或容器镜像），而非原始代码。其度量值为 $\mu(\beta(e))$ ，其中 $\beta$ 是构建过程。
挑战： 构建过程 $\beta$ 必须是确定性的（可重现的），这样重建的源代码才能产生正确的度量值。
解决方案： NixReflect，一个 Nix 转译器。
- 它使用 Nix 包管理器来确保可重现构建（reproducible builds）。
- 节点从内置数据中重建对等体的 Nix 表达式（构建定义）。
- 节点随后在其自身环境中可重现地重新构建对等体的产物（例如 Nitro Enclave 镜像文件）。
- 它从重建的产物中推导出参考度量值（例如 PCRs）。

3. 核心贡献

理论重构： 将问题表达为相互不动点方程组，并利用克莱尼第二递归定理求解，证明了可以在没有 TTP 的情况下构建自包含的参考值。
PyReflect（直接度量）： 一个 Python 转译器，生成的相互引用节点能够重建对等体源码并直接对其进行哈希。通过使用软件 TPM (swtpm) 进行相互度量的概念验证（PoC）展示了其可行性。
NixReflect（产物度量）： 一个 Nix 转译器，生成的节点能够可重现地重建对等体产物。通过两个 AWS Nitro Enclave 相互重建彼此的 Enclave 镜像并仅从内置数据推导出参考 PCR 的 PoC 展示了其可行性。
架构无关性： 该方案不需要修改目标硬件的底层 SDK、签名工具、加载器或度量栈。它仅通过本地自包含的推导过程替换了外部“参考值提供者”的角色。

4. 结果与性能

可行性： 两个 PoC 均成功演示了节点能够仅通过内置数据推导出对等体的参考值，从而在没有外部干预的情况下解决了无限回归问题。
开销分析（Nitro Enclaves）：
- 本文比较了两种变体：一种仅对重建的源码进行哈希（digest），另一种是可重现地重建产物（rebuild）。
- Digest 变体： 推导时间极短（约 0.07s）。
- Rebuild 变体： 推导时间大约慢 100 倍（约 6.8s），因为它必须遍历完整的构建闭包以再生产物。
- 作者指出，对于复杂的应用程序，重建成本可能会进一步增加，因此对于产物度量架构，将构建步骤外包给预部署阶段（使用可度量的构建）可能是减少运行时延迟的手段。
代码规模： 转译引入了相对于源代码族总量的线性代码规模开销，但增幅较小（例如，0.9 KB 的模板生成了 3.4 KB 的节点）。

5. 重要性与主张

本文声称提供了首个满足以下条件的相互度量引导问题的解决方案：

架构无关性： 能够在不同的 TEE 和度量类型之间工作，无需自定义硬件特性。
无 TTP： 不需要可信第三方或外部参考值提供者。
非侵入性： 不需要更改硬件厂商的度量栈或 SDK。

局限性与范围：

作者明确指出，其贡献仅限于自包含重建的可行性。他们并不声称增强了底层硬件的安全性保证；其信任模型与标准的单向度量（依赖硬件根信任和背书 PKI）完全一致。
该方案无法防止标准威胁模型之外的攻击（例如受损的硬件）。
运行约束：
- 对于一个完全相互依赖的家族，更新通常需要重新部署所有节点，因为共享数据块包含了整个家族的源代码。
- 对于产物度量系统，可重现重建的运行时成本显著，但作者建议使用“可度量构建”（将构建过程外包给 TEE 支持的沙箱）作为潜在的缓解方案，这通过将运行时成本转化为对构建时 TEE 的信任来进行权衡。

总之，本文确立了可以通过使用递归理论进行软件构造来实现相互度量引导，从而消除了此前必须依赖可信第三方或特定架构黑科技的循环依赖问题。