Source-linked AI summary

Bootstrapping Mutual Attestation with Kleene's Second Recursion Theorem

Takuma Imamura

arXiv:2608.20671v1cs.CRmath.LO

TL;DR

In multi-node systems where each node verifies its peers, nodes need their reference values in advance, but mutually embedding those values creates an infinite regress. The paper applies Kleene’s second recursion theorem to generate mutually referencing nodes, and its NixReflect PoC has two Nitro Enclaves reproduce each other’s images and derive reference PCRs from built-in data alone.

  • Problem

    In multi-node systems where each node verifies peers, they need peer reference values in advance, but embedding mutually dependent measurements creates an infinite regress.

    Source: §1 · p. 1
  • Method

    The paper models bootstrapping as mutual fixed-point equations and applies Kleene’s second recursion theorem to generate mutually referencing nodes uniformly.

    Source: §2 · p. 2, §9 · p. 8
  • Results

    The NixReflect PoC has two Nitro Enclaves reproduce each other’s images bit-for-bit and derive PCR0–2 from built-in data; this computation is approximately 100× slower than hashing alone.

    Source: §1 · p. 2, §9 · p. 9
  • Takeaways & Limitations

    The construction provides an architecture-independent route to mutual attestation without a TTP or externally supplied reference values, using existing attestation stacks unchanged.

    Source: §1 · p. 2

    The Nitro PoC demonstrates reference-PCR reproduction but stops short of implementing Nitro attestation; mutual attestation requires composing those values with Nitro’s standard flow.

    Source: §4.2 · p. 5

Abstract

from arXiv · show

Mutual attestation among nodes with no central trusted operator requires each node to hold reference values (expected code measurements) for its peers. The naïve approach of mutually embedding these reference values in the nodes' code leads to an infinite regress. We call the problem of resolving this infinite regress the reference-value bootstrapping problem for mutual attestation. Existing solutions avoid this regress by relying on a trusted third party (TTP), externally supplied reference values, or architecture-specific measurement mechanisms. We instead express the bootstrapping problem as a system of mutual fixed-point equations and solve it by Kleene's second recursion theorem. The construction produces nodes that mutually reference one another's code and reconstruct every peer's exact source from built-in data alone. When a deployed source file is measured directly, as with a Python script, a node obtains the peer's reference value by applying the measurement function directly to the reconstructed source. When a built image is measured, as with AWS Nitro Enclaves, a node instead reproducibly rebuilds the peer's image from the reconstructed source and derives its reference measurement. For the first case, we develop PyReflect, a Python transpiler, and use it to implement a TPM mutual-attestation PoC. For the second, we develop NixReflect, a Nix transpiler, and use it in a PoC in which two Nitro Enclaves reproduce each other's reference PCRs from built-in data alone. Our solution is architecture-independent, requires neither a TTP nor externally supplied reference values, and works with existing attestation stacks unchanged.

1 Introduction

The paper addresses the infinite regress in giving mutually attesting nodes self-contained reference values, solving it with Kleene’s second recursion theorem and demonstrating source- and build-measurement implementations.

Introduction

  • Mutual attestation requires every node to know its peers’ reference values before data exchange, but embedding those values recursively creates an infinite regress.The paper calls constructing nodes with mutually consistent, self-contained peer reference values the reference-value bootstrapping problem. Such settings include decentralized computing, cooperating enclave services, peer-to-peer confidential-computing networks [10], and multi-provider confidential-VM AI systems [1].Source: §1 · p. 1
  • Prior approaches delegate reference-value distribution to a TTP, use architecture-specific credentials, configure out-of-scope report fields, or exploit architecture-specific measurement [3].The paper characterizes these approaches as reintroducing a trusted party or tying the protocol to a particular isolation architecture.Source: §1 · p. 1
  • The paper formulates bootstrapping as mutual fixed-point equations solved by Kleene’s second recursion theorem [9], targeting an architecture-independent solution without a TTP or external reference values.Its approach uses the existing software and attestation stack without modifying the SDK, signing tools, or loader; theorem uniformity also permits automatic generation of mutually referencing programs.Source: §1 · p. 2
  • For architectures measuring deployed source, PyReflect reconstructs and hashes a peer’s exact source, demonstrated in a TPM mutual-attestation proof of concept.PyReflect transpiles templates—families of programs referencing one another’s source—into mutually referencing nodes, using TPM quote machinery backed by a userland software TPM.Source: §1 · p. 2
  • For architectures measuring build artifacts, NixReflect reproducibly rebuilds a peer’s image bit-for-bit before deriving its measurement; its two-Nitro-Enclave proof of concept reproduces peer reference PCRs from built-in data.The rebuild must match the deployed artifact exactly for the recomputed reference value to match.Source: §1 · p. 2
  • Approximately 100× slower: the Nitro Enclave proof of concept’s source-to-image-to-PCR computation takes roughly 100 times as long as hashing the peer’s Nix source alone.Because rebuilding traverses the workload’s full build closure, the paper expects this gap to widen for more complex applications.Source: §1 · p. 2
  • The construction replaces only the external Reference Value Provider; each uncompromised verifier derives the expected value and verifies its peer within its own TCB, inheriting the underlying one-way flow’s trust roots and limitations.Attestable builds can remove runtime toolchain and build latency, but require trust in the Build TEE’s hardware root and endorsement PKI when it does not share a root with deployed nodes. Updates currently propagate across the mutually dependent family, though dependency-graph decomposition could confine them to affected strongly connected components.Source: §1 · p. 2

2 The bootstrapping problem as mutual fixed points

The bootstrapping problem can be expressed as mutual fixed-point equations for nodes whose behaviors may use the source code of every node. Under the stated assumptions, Kleene’s simultaneous recursion theorem provides a solution computable uniformly from the nodes’ behaviors.

2 The bootstrapping problem as mutual fixed points

  • Under three assumptions—programs represented by source-code indices, behaviors able to access every node’s source, and deterministic computable measurement—a mutually attesting family is a tuple of source codes solving mutual fixed-point equations.The equations equate each program’s computed partial function with its intended behavior using the family’s source codes.Source: §2 · p. 2
  • Repeated hard-coding leads to infinite regress when the dependency graph contains a directed cycle, while the system as a whole is a mutual fixed-point equation.Hard-coding works as expected when the dependency graph is acyclic.Source: §2 · p. 2
  • For any tuple of computable behaviors, the simultaneous recursion theorem yields indices satisfying the mutual equations, uniformly computable from the behavior indices.The paper identifies this constructive map from behavior templates to mutually referencing programs as the idea mirrored by PyReflect and NixReflect.Source: §2 · p. 3
  • Under the assumptions, the solution lets each node compute every node’s exact code and reference value from built-in data alone, without a trusted third party or host-injected measurement.The reference value follows from the source code because measurement is assumed to be a deterministic computable function of that code.Source: §2 · pp. 2–3
  • The substantive measurement assumption is realized differently by architecture: direct source-code measurement uses a plain hash, while artifact measurement uses reproducible builds.The paper treats these cases in Sections 3 and 4, respectively.Source: §2 · p. 3

3 Mutual attestation without builds

For deployed-code measurements, nodes can reconstruct each peer’s exact source from built-in data and hash it to obtain reference values without external input. PyReflect implements the construction for Python, and a TPM proof of concept uses the values in mutual attestation.

3 Mutual attestation without builds

  • For deployed-code measurements, nodes reconstruct each peer’s exact source, hash it for a reference value, then use the standard attestation flow to check the peer’s evidence.Transpilation is a one-time step; runtime reconstruction, hashing, and attestation require only a hash function and ordinary attestation machinery.Source: §3 · p. 3

3.1 The PyReflect transpiler

  • PyReflect emits one Python file per node, each able to reconstruct every family member’s byte-exact source from built-in data.It serializes the family into a shared canonical blob with a per-node selector, then rewrites node-id references as calls to a runtime reconstruction function that regenerates the embedding line.Source: §3.1 · p. 3

3.2 PoC: TPM-backed mutual attestation

  • The two-node TPM proof of concept self-computes peer references from reconstructed source and uses TPM quotes to attest measurements while binding quotes to an ECDH session.Each node checks the peer’s quote, PCR digest, signature, and qualifying data; the PCR carries the measurement, while the qualifying data binds freshness and the ephemeral key exchange.Source: §3.2 · pp. 3–4
  • The PoC trusts emulator-generated attestation keys and uses resettable PCR 23, so it does not demonstrate hardware-backed identity or bind the code hash to the running program.A production deployment could authenticate keys through a vTPM’s hardware attestation or a physical TPM’s endorsement path, and measure files with IMA against PCR 10; session binding remains in qualifying data.Source: §3.2 · p. 4

4 Mutual attestation with reproducible builds

For artifact-measured TEEs, the method reconstructs peer source, reproducibly rebuilds the artifact, and applies its measurement function to derive reference values. The Nitro Enclaves proof of concept verifies that each node can derive its peer’s PCRs from built-in data alone.

4.1 From source to measurement

  • For artifact-measured architectures, the reference is μ(β(e)); because builds may be nondeterministic, reproducibly rebuilding measurement-relevant contents is essential, while the fixed-point construction remains unchanged.Pinning build dependencies by hash and using a reproducible builder ensures the same complete source description yields the same artifact and measurement [11]; implementations must carry the toolchain and pay the build cost.Source: §4.1 · p. 4

4.2 NixReflect and PoC: reproducing Nitro Enclave PCRs

  • NixReflect uses Kleene’s trick to let mutually referencing Nix expressions reconstruct each peer’s exact build definition, including the pinned toolchain, dependencies, and sources.The Nitro PoC uses Nix via monzo/aws-nitro-util to build bit-identical EIFs from pinned inputs, since the stock nitro-cli pipeline is not reproducible.Source: §4.2 · pp. 4–5
  • On both x86_64 and AArch64 Nitro Enclaves-capable instances, each enclave reconstructed its peer’s definition, rebuilt its EIF, and computed matching reference PCR0–2 from built-in data alone.Reproducibility makes the rebuilt-image PCRs equal the measurements of the peer’s deployed image.Source: §4.2 · p. 5
  • The PoC derives and announces peer reference PCRs rather than implementing Nitro attestation; composing those values with standard document verification enables mutual attestation without an external Reference Value Provider.The paper identifies this self-contained reference-value derivation as the bootstrap ingredient and contrasts it with AWS’s measurement notary.Source: §4.2 · p. 5

5 Cost

Transpilation scales linearly with template-body size, while reference derivation is negligible when hashing reconstructed source but can be dominated by reproducible rebuilding. In the NixReflect PoC, rebuilding took approximately two orders of magnitude longer than hashing, though its absolute cost remained modest.

5 Cost

  • Transpilation time is linear in template-body size, and a 0.9 KB two-node template yields nodes of 3.4 KB each.Rewriting each node-id occurrence changes it by a constant, while blob encoding inflates by a constant factor.Source: §5 · p. 5
  • Reference derivation reconstructs the peer’s source linearly, then either hashes it directly or reproducibly rebuilds it, a step expected to dominate cost.Without a build, measurement is a single hash and the whole derivation is negligible; with a build, absolute cost is not determined by the construction.Source: §5 · p. 5
  • The unchanged attested handshake is outside derivation cost and requires exactly two one-way attestations per pair, up to k(k−1) /2 pairs group-wide.Source: §5 · p. 5
  • Rebuilding took approximately two orders of magnitude longer than hashing, but remained under ten seconds from cold launch to the peer’s reference PCRs.Re-staging the peer’s rootfs, re-packing its ramdisk, and re-running EIF assembly took under seven seconds; the digest variant’s sub-0.1 s timing is near console-timing resolution and is best read as negligible.Source: Table 3 · p. 6, §5 · p. 6
  • Rebuild time and image size grow with node closure, and larger builds may require more enclave memory than hashing, making runtime-build offloading more attractive for complex applications.The compared variants fit within the same 2 GiB allocation, but a larger build may need memory for its toolchain, inputs, and intermediate artifacts.Source: §5 · p. 6

6 Trust assumptions and security considerations

The construction moves the Reference Value Provider into each verifying node without adding an external party to the trust model. It demonstrates self-contained reference-value reconstruction while inheriting the underlying one-way-attestation threat model and security semantics.

6 Trust assumptions and security considerations

  • The construction relocates the Reference Value Provider into the verifier and introduces no external party into the trust model.It changes that single role in the RATS architecture and leaves the rest untouched.Source: §6 · p. 6
  • Each verifier trusts the underlying architecture’s roots of trust, and an uncompromised node’s peer verification remains independent of other group members.The assumed roots are the isolation architecture, its measurement mechanism, and the Endorser’s certificates; the guarantee belongs to each verifier, not the group as a whole.Source: §6 · p. 6
  • A peer is accepted only when its reported measurement matches the digest of the reconstructed source or reproducibly rebuilt artifact.Passing off different code requires a second preimage against the underlying architecture’s measurement hash.Source: §6 · p. 6
  • The contribution demonstrates feasibility of self-contained reconstruction and neither prevents attacks outside the inherited threat model nor enables attacks it rules out.Its security semantics are those of the underlying one-way-attestation flow.Source: §6 · p. 6

7 Discussion

The discussion identifies run-time reproducible builds as the dominant cost of built-artifact measurements and considers attestable-build proofs to offload that work, with additional trust-root requirements. It also explains why updates currently require redeploying the whole family and outlines a dependency-component refinement.

7.1 Offloading the run-time build

  • Runtime build measurements impose the dominant overhead: each node carries a full toolchain and rebuilds its peer’s artifact, including Nix and pinned inputs in the Nitro PoC.Source: §7.1 · p. 6
  • Attestable builds [8] can move source-to-measurement work before deployment: nodes verify an injected measurement and CCP against reconstructed peer source, then need no toolchain or build latency.The CCP proves that a specific artifact measurement was produced from a source snapshot.Source: §7.1 · p. 6
  • Offloading remains TTP-free because mismatched pairs are rejected, but requires trust in the build TEE’s hardware root and endorsement PKI; different trust roots expand the verifier’s trust set.For example, an AMD SEV-SNP build TEE for Nitro Enclaves additionally requires trust in AMD’s attestation chain.Source: §7.1 · pp. 6–7

7.2 Updates and redeployment

  • Under current transpilers, changing one node changes every family member’s source and measurement, so updates require re-transpiling and redeploying the entire family.The shared blob records every node body verbatim.Source: §7.2 · p. 7
  • A proposed refinement would resolve fixed points per strongly connected component: only nodes that can reach the changed node need updating, though fully mutual attestation remains global.The refinement shares blobs within components and could benefit asymmetric topologies; working it out is beyond the paper’s scope.Source: §7.2 · p. 7

8 Related work

Related work avoids mutual-reference circularity by placing reference values outside measured artifacts, deriving them through hardware-specific measurement mechanisms, or reducing attestation overhead. The paper’s construction instead derives peer references from built-in representations, with a source-level method that leaves existing attestation stacks unchanged.

8.1 Trusted third parties (TTPs)

  • TTP-based approaches avoid embedding reference values in measured artifacts, but require trust in an authority or signer and may depend on an online provider.AWS Nitro Enclaves use a Measurement Notary Service, while Teaclave relies on trusted auditors’ signatures; this construction derives measurements from built-in representations instead.Source: §8.1 · p. 7

8.2 Self-attestation certificates

  • DECENT certifies deployment-supplied AuthLists, eliminating circularity because the lists do not alter MRENCLAVE, whereas this construction derives references from peer sources internally.DECENT’s certificates bind a component’s list to its key and code digest, but do not prove that listed measurements derive from particular sources; the construction is architecture-independent at source level.Source: §8.2 · p. 7

8.3 Hardware-rooted reference-value injection

  • Hardware-rooted injection avoids circular hard-coding by placing peer values in attested fields outside the measurement, but requires architecture-specific fields and launch-time input.The approach also supports confidential-VM fields such as Intel TDX MR_CONFIG_ID and AMD SEV-SNP HOST_DATA; unlike it, this construction derives values from built-in source representations without injection fields.Source: §8.3 · p. 8

8.4 Measurement-specific reference-value derivation

  • MAGE derives peer MRENCLAVE values from shared pre-measurement hash states and SGX’s load-order hashing, but cannot reconstruct peer code and depends on measurement-specific tooling.Its construction is measurement-level analogous to a shared blob plus per-node selector, but cuts circularity through incremental MRENCLAVE structure rather than Kleene’s trick; the paper’s source-level construction works unchanged with each architecture’s measurement function and existing tooling.Source: §8.4 · p. 8

8.5 Scalability of mutual attestation

  • Careful Whisper [10] reduces pairwise mutual-attestation overhead from up to N(N−1)/2 handshakes to linear under ideal conditions, while a designated attester requires group trust.Both approaches use intermediary verifiers and presuppose correct reference values, which this construction supplies for either topology, including a designated-attester star.Source: §8.5 · p. 8

9 Conclusion · A Open Science

The conclusion presents mutual reference-value bootstrapping as a fixed-point problem solved uniformly by Kleene’s second recursion theorem, with PoCs showing source-to-measurement reconstruction for directly measured code and built images. The construction enables self-contained reference reconstruction without replacing or strengthening the underlying attestation mechanism.

9 Conclusion

  • The simultaneous form of Kleene’s second recursion theorem solves mutual reference-value bootstrapping as fixed-point equations, uniformly generating the mutually referencing nodes.The nodes are generated automatically rather than written by hand.Source: §9 · p. 8
  • For architectures that measure deployed code directly, PyReflect generates mutually referencing nodes, and a userland software TPM PoC demonstrates the missing reference-value step.The approach transpiles the code and hashes the resulting source.Source: §9 · p. 8
  • NixReflect lets two Nitro Enclaves reproduce each other’s images bit-for-bit and derive reference PCR0–2 from built-in data alone.For the simple PoC target, source-to-image-to-PCR computation is approximately 100× slower than hashing alone; the gap is expected to widen for more complex applications.Source: §9 · p. 9
  • The results establish feasibility of self-contained reference-value reconstruction, but do not replace or strengthen attestation; each verifier retains its architecture’s one-way-attestation trust model and security semantics.Source: §9 · p. 9
  • The self-contained construction removes the need for a trusted Reference Value Provider, external launch-time injection, or an architecture-specific fixed-point mechanism, and unlike MAGE requires no intermediate measurement state or stack changes.It leaves the TEE’s SDK, signing tools, loader, and attestation stack unchanged.Source: §9 · p. 9
  • Artifact-measured nodes carry the reproducible-build closure and runtime cost, while changing a fully mutual family currently requires redeploying every member.Attestable builds can remove runtime toolchain and latency without a trusted provisioning party, but may add trust in the Build TEE hardware root.Source: §9 · p. 9
  • Managing attestable-build proof lifecycles and exploiting finer-grained dependency graphs for updates remain future work.Source: §9 · p. 9

B Proofs of Kleene’s recursion theorems

The appendix proves classical recursion-theory results underlying the construction, emphasizing that the transpilers mirror their constructive self-application pattern. It connects that pattern to emitted node files that can be reconstructed byte-for-byte.

B Proofs of Kleene’s recursion theorems

  • The proofs explain how the transpilers mirror the constructive self-application pattern of Theorem 2.2 and Corollary 2.3, with the syntactic correspondence detailed in Appendix C.The paper gives these proofs because the transpilers of Sections 3.1 and 4.2 follow that pattern.Source: B Proofs of Kleene’s recursion theorems · p. 9
  • Corollary 2.3 is reduced to the k = 1 case using a computable isomorphism between N^k and N, and a more concrete proof clarifies the transpilers’ connection.The proof states that the general case follows from Theorem 2.2.Source: B Proofs of Kleene’s recursion theorems · pp. 9–10
  • Each node’s render function reassembles every family member’s complete file byte-for-byte, including its own, using shared data and the running node’s blob.Shared byte-identical segments and node-specific bodies are recorded in D; the DATA line is regenerated from the running node’s blob, mirroring self-application.Source: Figure 1 · p. 10

C Design of the emitted nodes

PyReflect resolves source self-reference by rewriting node references into run-time reconstruction calls and embedding a shared description of the node family. NixReflect uses the same emitted layout with Nix expressions, and the framework reproduces each deployed source verbatim.

C Design of the emitted nodes

  • PyReflect rewrites each node-id reference as a run-time call that reconstructs the referenced node’s source; NixReflect uses the same layout with Nix expressions.The rewritten bodies play the role of g in the fixed-point construction.Source: C Design of the emitted nodes · p. 10
  • Each node embeds the same base64-encoded canonical JSON blob describing the rewritten family, while a node-specific selector distinguishes its file.The five-part layout comprises the header, selector line, embedded data, framework, and rewritten body; the header, framework, and bodies are shared or drawn from the blob.Source: C Design of the emitted nodes · p. 10
  • Canonical serialization and a structurally identical rendering function let each node reconstruct any peer’s deployed source verbatim, realizing the fixed-point equation φ_e = f(e, −).The running node regenerates its own data line from its blob because that line cannot be contained in the shared data itself.Source: C Design of the emitted nodes · pp. 10–11

D Complete benchmark environment

The benchmark’s complete host and software configuration is documented in Table 4.

Loading 2608.20671v1…