PaperlayerView exact revision on arXiv

Source-linked AI summary

Bootstrapping Mutual Attestation with Kleene's Second Recursion Theorem

Takuma Imamura

arXiv:2608.20671v1cs.CRmath.LO

TL;DR

Mutual attestation needs self-contained peer reference values, but mutually embedding them causes an infinite regress. The paper solves this as a mutual fixed-point problem using Kleene’s second recursion theorem, implementing source hashing and reproducible image measurement with PyReflect and NixReflect. The proof-of-concept systems derive peer reference values from built-in data without a TTP or externally supplied values, while image rebuilding is approximately 100× slower than hashing alone.

  • Problem

    Mutual attestation requires each node to know its peers’ reference values, but embedding those values in mutually dependent code creates an infinite regress.

  • Method

    The paper formulates bootstrapping as mutual fixed-point equations and solves them uniformly with Kleene’s second recursion theorem, using transpilers for source and reproducible-image measurements.

  • Results

    The PyReflect and NixReflect proof-of-concept systems derive peer reference values from built-in data, including mutually reproduced Nitro Enclave PCRs; image measurement is approximately 100× slower than hashing alone.

  • Takeaways & Limitations

    The construction provides architecture-independent mutual reference-value bootstrapping without a TTP or externally supplied reference values, while preserving the established attestation flow.

  • Takeaways & Limitations

    The Nitro Enclaves proof of concept derives and announces peer reference values but does not reimplement Nitro attestation-document retrieval and verification; an offloaded build variant also adds trust in the build TEE’s hardware root and endorsement PKI.

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

Mutual attestation requires peers to know one another’s reference values, but embedding those values creates an infinite regress. The paper resolves this bootstrapping problem with mutually fixed-point constructions that avoid trusted third parties and architecture-specific mechanisms while using existing attestation stacks.

  • Motivation: In mutual attestation, every node verifies its peers and must know their reference values before exchanging confidential data.This requirement arises in decentralized systems, cooperating enclave services, and multi-component agentic AI systems.
  • Motivation: Hard-coding peer reference values creates an infinite regress because each code digest depends on code containing the other node’s digest.The paper names constructing mutually consistent, self-contained peer reference values the reference-value bootstrapping problem.
  • Prior approaches: Existing approaches avoid the regress through trusted parties, externally configured values, or architecture-specific measurement processes.These alternatives either reintroduce a trusted party or tie the protocol to a particular isolation architecture.
  • Approach: The paper reformulates bootstrapping as mutual fixed-point equations and solves it with Kleene’s second recursion theorem.The theorem’s uniformity enables automatic generation of mutually referencing programs rather than hand-written constructions.
  • Implementations: For directly measured deployed code, PyReflect reconstructs and hashes peers’ exact source, while a TPM mutual-attestation proof of concept demonstrates self-contained reference values.The approach targets architectures such as Linux IMA that measure deployed code itself.
  • Implementations: For measured build artifacts, NixReflect uses reproducible builds to reconstruct peer images and derive their reference measurements, with approximately 100× higher cost than hashing alone in the Nitro Enclaves proof of concept.The paper expects this gap to widen for more complex applications because rebuilding traverses the full build closure.
  • Scope: The construction replaces only the external Reference Value Provider, while inheriting the underlying one-way-attestation flow’s trust roots, guarantees, and out-of-scope attacks.It requires no modifications to the target architecture’s SDK, signing tools, loader, or attestation stack.
  • Operational consequences: Updates currently propagate across the whole mutually dependent family, although dependency-graph decomposition could confine them to affected strongly connected components.The paper identifies this refinement as beyond its scope.

2 The bootstrapping problem as mutual fixed points

The paper models mutual reference-value bootstrapping as mutual fixed-point equations and solves the system using Kleene’s second recursion theorem. Its uniform construction generates mutually referencing programs whose nodes reconstruct peer source code and derive self-contained reference values without a trusted third party.

  • Model: Each node is modeled as a program whose computable behavior may access the source codes of every family member, including itself.The model assumes computable partial functions and source access for the intended node behaviors.
  • Model: A node’s reference value is computable from its source code, so a mutually attesting family is a tuple of source codes satisfying the mutual fixed-point system.This substantive measurement assumption connects source reconstruction to reference-value computation.
  • Problem: Mutual reference values form a fixed-point problem because hard-coding peer digests creates an infinite regress along dependency cycles.The system models each node’s behavior as depending on the source codes of all family members.
  • Construction: Kleene’s second recursion theorem provides the single-node fixed-point basis, while its simultaneous form supplies mutually referencing tuples of program indices.The theorem guarantees indices e_i = f_i(ē, −), uniformly computable from the component behaviors.
  • Construction: The uniform theorem turns existence into an effective transpilation procedure that generates an entire mutually referencing family from behavior templates.PyReflect and NixReflect operationalize this map from behavior functions to mutually referencing program indices.
  • Consequence: Under the model’s assumptions, every node can reconstruct every family member’s exact code and derive self-contained reference values from built-in data alone.The construction requires neither a trusted third party nor a host-injected measurement.

3 Mutual attestation without builds

For architectures that measure deployed source files directly, nodes reconstruct peers’ exact source and hash it to obtain reference values. PyReflect implements the construction for Python and a TPM PoC demonstrates self-computed values within a standard mutual-attestation flow.

  • Source measurement: For deployed-code measurements such as Linux IMA, a node reconstructs the peer’s exact source and hashes it to obtain the peer’s reference value.The architecture measures loaded file bytes directly, so the source-to-measurement map is a single hash.
  • Attestation flow: The runtime flow reconstructs the peer source, hashes it, and checks the reported measurement against that self-computed reference value using ordinary attestation machinery.Only transpilation is additional; runtime verification needs a hash function and the existing attestation flow.
  • PyReflect: PyReflect accepts templates containing node identifiers as source references and emits one mutually referencing Python file per node.Each identifier occurrence denotes the source code of the referenced node.
  • PyReflect: PyReflect serializes the family into one canonical shared blob and uses runtime reconstruction to regenerate each member’s exact source.The design reduces mutual reference to self-reference of a single system and applies Kleene’s construction.
  • PoC: A two-node TPM PoC uses software TPMs to reconstruct peers’ source byte-for-byte, compute SHA-256 reference values, and perform mutual attestation.The PoC runs in Docker and uses TPM quote machinery with ECDH session binding.
  • PoC limitations: The TPM PoC omits hardware-backed AK–EK authentication and uses PCR 23, so production deployment should use an authenticated TPM path and IMA-backed PCR 10 measurements.These simplifications concern the emulator and measurement setup rather than the reference-value construction.

4 Mutual attestation with reproducible builds

For artifact-measured architectures, the construction reconstructs peer source, reproducibly rebuilds the artifact, and applies the architecture’s measurement function. NixReflect demonstrates this process by reproducing mutually derived Nitro Enclave PCRs from built-in data alone, while the PoC stops short of reimplementing Nitro attestation.

  • Artifact measurement: Artifact-measured architectures derive reference values as μ(β(e)), where β builds an artifact from source e and μ measures the artifact.Examples include enclave images, confidential-VM launch measurements, and confidential-container images.
  • Architecture independence: The fixed-point construction remains architecture-independent because changing the architecture changes μ and β, not mutual source reproduction.The corresponding toolchain and build cost are architecture-specific.
  • Artifact workflow: The artifact workflow reconstructs peer source, rebuilds the peer artifact bit-for-bit, and applies μ to obtain the peer’s reference measurement.This adds rebuilding to the source-level construction while leaving the fixed-point step unchanged.
  • Reproducible builds: Because ordinary builds may be nondeterministic, the construction requires reproducible builds that produce identical measurement-relevant artifacts from the same source description.Pinned dependencies and a reproducible builder ensure the same artifact measurement.
  • NixReflect: NixReflect turns mutually referencing Nix expressions into nodes that reconstruct each member’s exact build definition and supports pinned, reproducible Nitro builds.The transpiler applies the same rewriting mechanism beyond Python and direct source hashing.
  • Nitro PoC: Two Nitro Enclaves reproduced each other’s reference PCR0–2 from built-in data alone on both x86_64 and AArch64-capable parent instances.Each enclave reconstructed the peer definition, rebuilt its EIF, and computed PCR0–2 from the rebuilt image.
  • PoC scope: The Nitro PoC demonstrates reference-value reproduction but does not reimplement Nitro attestation-document retrieval and verification.Composing the reproduced values with Nitro’s established attestation flow is left as the next integration step.

5 Cost

The cost analysis separates source reconstruction from measurement derivation: hashing reconstructed source is negligible, whereas reproducibly rebuilding a peer’s image dominates runtime cost. In the Nitro Enclaves PoC, rebuilding took about two orders of magnitude longer than hashing, with costs increasing for larger build closures.

  • Transpilation: Transpilation emits each node from shared data, a selector, and a rewritten body, with rewriting and transpilation time linear in the relevant template size.A two-node 0.9 KB template produced 3.4 KB nodes each in the Nitro Enclaves PoC.
  • Reference-value derivation: At runtime, nodes reconstruct a peer’s source before either hashing it directly or reproducibly rebuilding it to obtain the peer’s measurement.The build-artifact path performs the second step inside the node, while the direct-measurement path uses a single hash.
  • Benchmark: The benchmark compares NixReflect’s source-digest and reproducible-rebuild variants under identical 2-vCPU, 2 GiB allocations, with separate measurements for each node.Each variant was run in a fresh debug enclave, and all 10 runs per node produced the expected peer values.
  • Results: Approximately 100× separates source-to-image-to-PCR computation from hashing alone in the Nitro Enclaves PoC.The rebuild variant’s cost includes re-staging the peer rootfs, re-packing its ramdisk, and re-running EIF assembly; the digest variant is near-negligible.
  • Scaling: Rebuild time and image size grow with the node’s build closure, potentially increasing runtime and enclave memory requirements for more complex applications.The current PoC variants fit within the same 2 GiB allocation, but larger builds may need more memory for toolchains, inputs, and intermediate artifacts.

6 Trust assumptions and security considerations

The construction relocates reference-value provision into the verifying node while leaving the rest of the RATS flow unchanged. Its security guarantee inherits the underlying architecture’s roots of trust and one-way-attestation threat model.

  • Trust model: The construction moves the Reference Value Provider into the verifying node and introduces no external party into the trust model.All other RATS roles and processing remain unchanged.
  • Threat model: The adversary may control the network and any subset of hosts and nodes, while trust remains placed in the isolation architecture, measurement mechanism, and Endorser certificates.The guarantee applies to each uncompromised verifier rather than to the group as a whole.
  • Verification: A verifier accepts a peer only when its reported measurement equals the digest of the peer’s reconstructed source or reproducibly rebuilt artifact.Passing off different code would require a second preimage under the underlying measurement hash.
  • Scope: The contribution is limited to demonstrating self-contained reconstruction and inherits the underlying one-way-attestation flow’s security semantics.It does not prevent attacks outside that inherited threat model or enable attacks that the model rules out.

7 Discussion

The discussion considers offloading runtime builds and refining update granularity. Offloading can reduce runtime burden but may expand trust requirements, while update effects depend on the reference graph’s connectivity.

  • 7.1 Offloading the run-time build: Build-artifact measurements require each node to carry a full build toolchain and reproducibly rebuild the peer artifact at runtime.In the Nitro Enclaves PoC, the enclave image must include Nix and all pinned inputs.
  • 7.1 Offloading the run-time build: Attestable builds could move source-to-measurement work before deployment by producing a hardware-rooted proof that a specific artifact came from a specific source snapshot.The proof is described as a confidential-computing proof issued by a TEE-backed build sandbox.
  • 7.1 Offloading the run-time build: At runtime, a node can verify an injected measurement and proof against the reconstructed peer source before adopting the measurement as its reference value.A forged or mismatched pair is rejected, so the proof provider need not be trusted as a provisioning party.
  • 7.1 Offloading the run-time build: Offloading requires trust in the build TEE’s hardware root and endorsement PKI, and may expand the verifier’s trust set when build and deployed architectures differ.Using an AMD SEV-SNP build TEE for Nitro Enclaves additionally requires trust in AMD’s attestation chain; revocation and transparency remain future work.
  • 7.2 Updates and redeployment: Under current transpilers, changing one node changes every family member’s source and measurement, so updates require retranspiling and redeploying the entire family.The shared blob records every body verbatim.
  • 7.2 Updates and redeployment: A component-wise refinement could limit update effects to nodes reachable from the changed node by resolving fixed points per strongly connected component.Fully mutual attestation remains the worst case because its reference graph is strongly connected, whereas asymmetric topologies could preserve unaffected members.

8 Related work

Related approaches avoid mutual-reference circularity through trusted providers, deployment-supplied values, hardware-bound fields, certificates, or measurement-specific instrumentation. This construction instead derives peer measurements from reconstructed source and operates unchanged at the source level across architectures.

  • External reference values: Trusted third-party services or signed distributions avoid recursion by keeping reference values outside measured artifacts, but verification depends on that external provider.The Nitro Enclaves Measurement Notary Service exemplifies this approach, whereas the present construction derives measurements from fixed-point representations.
  • Certificate-based approaches: Teaclave loads peer measurements and auditor signatures at runtime, retaining trusted auditors rather than embedding mutually dependent enclave measurements.Its approach removes the need for an online notary during every verification but does not remove auditor trust.
  • DECENT: DECENT uses deployment-time AuthLists and certificates to bind authorised measurements to component identities without changing MRENCLAVE.Its certificates prove which list a component loaded, not that listed measurements came from particular sources.
  • DECENT: Unlike DECENT, this construction reconstructs every peer’s exact source and computes reference values internally without an externally supplied measurement list.Only the architecture’s measurement function varies, while the source-level construction remains unchanged across architectures.
  • Hardware-bound values: Hardware-bound launch fields can carry externally supplied peer values without incorporating them into the measured artifact, but require architecture-specific report support and an external launch path.Intel SGX KSS, Intel TDX MR_CONFIG_ID, and AMD SEV-SNP HOST_DATA illustrate this family of approaches.
  • MAGE: MAGE stores shared pre-measurement hash states plus per-member indices, enabling measurement reproduction without reconstructing source code.Its implementation modifies the SGX SDK, signing tool, and loader, and relies on incremental measurement structure rather than Kleene’s theorem.
  • Architectural scope: MAGE’s portability depends on compatible intermediate hash states and measurement placement, whereas this construction uses the architecture’s measurement function through existing interfaces.The present implementation requires no modification to the TEE SDK, signing tools, loader, or attestation stack.

9 Conclusion

The paper formulates mutual reference-value bootstrapping as mutual fixed-point equations and solves it uniformly with Kleene’s second recursion theorem. PyReflect and NixReflect demonstrate self-contained reconstruction for source measurements and reproducibly built artifacts, while exposing operational costs and inherited attestation semantics.

  • Mutual attestation bootstrapping is solved as a system of mutual fixed-point equations using the simultaneous form of Kleene’s second recursion theorem.The uniform construction automatically generates mutually referencing nodes rather than requiring them to be written by hand.
  • PyReflect demonstrates self-contained reference-value reconstruction when architectures measure deployed source code directly.The construction transpiles mutually referencing nodes and hashes reconstructed peer sources in a TPM mutual-attestation proof of concept.
  • NixReflect makes two AWS Nitro Enclaves reproduce each other’s images bit-for-bit and derive each other’s reference PCR0–2 from built-in data alone.For the simple proof-of-concept target, source-to-image-to-PCR computation is approximately 100× slower than hashing alone.
  • The construction establishes feasibility without replacing or strengthening the underlying architecture-specific attestation mechanism.Each verifier retains the trust model and security semantics of its architecture’s one-way-attestation flow.
  • The self-contained form removes trusted reference-value providers, external launch-time injection, architecture-specific fixed-point mechanisms, and changes to existing TEE stacks.The paper contrasts this with MAGE’s need for intermediate measurement state and TEE stack modifications.
  • Artifact-measured nodes incur reproducible-build closure and runtime costs, while changes in a fully mutual family currently require redeploying every member.Attestable builds and finer-grained dependency graphs are identified as future directions with corresponding trust and lifecycle considerations.

B Proofs of Kleene’s recursion theorems

The appendix presents classical recursion-theoretic proofs because the transpilers mirror their constructive self-application pattern. The mutual construction yields node codes that reproduce every family member’s file, including themselves.

  • Theorem 2.2 and Corollary 2.3 are classical recursion-theory results whose proofs are included because the transpilers mirror their constructive self-application pattern.The syntactic correspondence between the theorems and implementations is recorded in Appendix C.
  • The simultaneous recursion construction reduces the mutual case to the single-function theorem through a computable isomorphism.The proof of Corollary 2.3 uses the computable isomorphism between N^k and N.
  • Each constructed node reproduces every member’s file byte-for-byte, including its own file.This follows from applying the rendering construction to a node identifier, including self-application.

C Design of the emitted nodes

The emitted-node design packages a rewritten mutually referencing family into shared canonical data and reconstructs each selected source at runtime. Self-application regenerates the otherwise unembeddable data line, making the replay reproduce the deployed file verbatim.

  • Figure 1 maps the shared blob to byte-identical shaded segments and distinguishes them from node-specific segments and the regenerated data line.The framework’s render operation reassembles a complete file from the blob, selector, and self-generated data line.
  • PyReflect rewrites node-source references into runtime render calls that reconstruct each target node from embedded data.The rewritten bodies serve the role of the computable function used in the recursion-theorem construction.
  • The transpiler serializes the rewritten family, shared header, and framework into one canonical JSON blob used by every emitted node.A per-node selector recovers the corresponding node from the shared description.
  • Each emitted file contains a header, selector line, framework, rewritten body, and embedded data blob.The header, framework, and bodies are shared with or drawn from the blob, while the selector line is node-specific.
  • The runtime framework reconstructs a target node by combining the shared data with its selector and regenerating the running node’s own data line.The data line cannot be contained directly in the shared blob, so it is produced as repr of the running node’s blob.
  • The replay reproduces the deployed file verbatim, including the node itself, because canonical serialization makes the blob byte-identical across nodes.The structurally identical render function realizes the defining fixed-point equation.

D Complete benchmark environment

Table 4 records the complete host and software configuration used for the Nitro Enclaves cost benchmark.

  • Table 4 records the complete host and software configuration used for the Nitro Enclaves cost experiment.
Loading 2608.20671v1…