fix(verification): prevent verifier artifact commitment divergence in Gnark/Circom paths

[doomhammerhell]

Summary

There appears to be a semantic binding gap between the verifier artifact committed into the batch Merkle leaf and the verifier artifact actually consumed by the verifier backend for Gnark and Circom proof systems.

VerificationData can carry both verification_key and vm_program_code. The SDK commitment logic prioritizes vm_program_code whenever it is present, regardless of the selected proving system. However, the Gnark and Circom verifier paths use verification_key during actual proof verification.

This creates a reachable state where the Merkle leaf commits to one auxiliary artifact, while the proof is verified against another one.

This issue is not only about accepting unused fields or request bloat. The core concern is that the on-chain inclusion evidence can describe a stronger or different verifier context than the one actually used during off-chain verification.

Component

SDK commitment generation, batcher verifier adapters, operator verifier adapters, and AlignedLayerServiceManager.verifyBatchInclusion.

Related issues / PRs checked

I noticed that #1743 appears related because it discusses stricter verification_data validation, but it seems to frame unused fields primarily as validation/resource bloat.

Issues/PRs such as #1042 and #1083 also appear related to binding verification keys, but the current implementation still seems to allow the committed auxiliary artifact to differ from the verifier artifact actually used by the Gnark/Circom verifier paths.

If this has already been fully addressed elsewhere, I would appreciate a pointer to the relevant fix.

Description

The protocol documentation describes the batch Merkle leaf as binding the proof commitment, public input commitment, and the relevant verifier auxiliary object:

• a VM/program commitment for SP1/Risc0-style proof systems;
• a verification-key commitment for Gnark/Circom-style proof systems.

However, the implementation does not appear to enforce a one-to-one relation between proving_system and the valid auxiliary field.

For Gnark and Circom, verification_key is the artifact consumed by the verifier backend. But if vm_program_code is also present, the SDK commitment logic commits to vm_program_code instead of verification_key.

As a result:

AuxCommitted(vd) != AuxUsed(vd)

can hold for an accepted verification object.

No cryptographic forgery is required. The submitter only needs a valid proof under the verification key that the verifier actually consumes.

Violated invariant

For every accepted inclusion leaf derived from a VerificationData object, the committed verifier artifact should be exactly the artifact consumed by the verifier backend.

Formally, let:

vd = VerificationData

PS(vd)  = proving-system identifier
P(vd)   = proof bytes
PI(vd)  = public input bytes
VK(vd)  = verification_key
VM(vd)  = vm_program_code

AuxUsed(vd) =
  VK(vd), for Gnark/Circom proof systems
  VM(vd), for SP1/Risc0 proof systems

AuxCommitted(vd) =
  auxiliary artifact committed into the Merkle leaf

The expected invariant is:

For every accepted inclusion leaf L derived from vd:

  Accepted(L) =>
    AuxCommitted(vd) = H(AuxUsed(vd) || PS(vd))
    and
    Verify_PS(vd)(P(vd), PI(vd), AuxUsed(vd)) = true

The current implementation appears to enforce the weaker predicate:

Accepted(L) =>
  AuxCommitted(vd) =
    if VM(vd) is present then H(VM(vd) || PS(vd))
    else if VK(vd) is present then H(VK(vd) || PS(vd))
    else 0

For Gnark/Circom, this is weaker than the required invariant because AuxCommitted(vd) can be derived from VM(vd), while AuxUsed(vd) is VK(vd).

Technical root cause

The SDK commitment logic selects vm_program_code first:

let proving_system_aux_data_commitment =
    if let Some(vm_program_code) = &verification_data.vm_program_code {
        hasher.update(vm_program_code);
        hasher.update([proving_system_byte]);
        hasher.finalize_reset().into()
    } else if let Some(verification_key) = &verification_data.verification_key {
        hasher.update(verification_key);
        hasher.update([proving_system_byte]);
        hasher.finalize_reset().into()
    } else {
        [0u8; 32]
    };

The Gnark and Circom verifier paths, however, consume verification_key.

For Gnark:

ProvingSystemId::GnarkPlonkBls12_381
| ProvingSystemId::GnarkPlonkBn254
| ProvingSystemId::GnarkGroth16Bn254 => {
    let Some(vk) = verification_data.verification_key.as_ref() else { ... };
    verify_gnark(..., vk)
}

For Circom:

ProvingSystemId::CircomGroth16Bn256 => {
    let Some(vk) = verification_data.verification_key.as_ref() else { ... };
    verify_circom(..., vk)
}

The operator verifier appears to follow the same semantic split by passing VerificationKey into the Gnark and Circom verification paths.

The on-chain inclusion check receives only the resulting commitments and cannot detect whether the committed auxiliary artifact was the same artifact consumed during verification:

bytes memory leaf = abi.encodePacked(
    proofCommitment,
    pubInputCommitment,
    provingSystemAuxDataCommitment,
    proofGeneratorAddr
);

bytes32 hashedLeaf = keccak256(leaf);
return Merkle.verifyInclusionKeccak(...);

Execution trace

Assume an application expects a Gnark proof to be included with:

provingSystemAuxDataCommitment = H(VK_expected || GnarkGroth16Bn254)

A submitter can construct:

VerificationData {
    proving_system: ProvingSystemId::GnarkGroth16Bn254,
    proof: P_attacker,
    pub_input: Some(PI_claim),
    verification_key: Some(VK_attacker),
    vm_program_code: Some(VK_expected),
    proof_generator_addr: attacker_or_zero,
}

Then:

1. The SDK computes:

proofCommitment = H(P_attacker)
pubInputCommitment = H(PI_claim)
provingSystemAuxDataCommitment = H(VK_expected || GnarkGroth16Bn254)

because vm_program_code is present.

2. The batcher/operator verifier executes the Gnark verifier using:

VK_attacker

because the Gnark path reads verification_key.

3. The proof verifies successfully under VK_attacker.

4. Operators sign the batch root.

5. The result is submitted on-chain.

6. The application calls verifyBatchInclusion using:

H(P_attacker),
H(PI_claim),
H(VK_expected || GnarkGroth16Bn254),
proofGeneratorAddr,
batchMerkleRoot,
merkleProof,
index,
senderAddress

7. verifyBatchInclusion returns true.

The accepted on-chain inclusion object now appears to be bound to VK_expected, while the off-chain verifier actually accepted the proof under VK_attacker.

Minimal property-level PoC

let vd = VerificationData {
    proving_system: ProvingSystemId::GnarkGroth16Bn254,
    proof: proof_valid_under_vk_attacker,
    pub_input: Some(public_inputs),
    verification_key: Some(vk_attacker),
    vm_program_code: Some(vk_expected),
    proof_generator_addr,
};

let c = VerificationDataCommitment::from(vd.clone());

assert_eq!(
    c.proving_system_aux_data_commitment,
    keccak256(vk_expected || [ProvingSystemId::GnarkGroth16Bn254 as u8])
);

// But the verifier path consumes vk_attacker, not vk_expected.
assert!(gnark_verify(vd.proof, vd.pub_input, vk_attacker));

This is enough to falsify the semantic binding invariant, even without requiring a full end-to-end exploit fixture.

Impact

The impact is an application-level semantic mismatch over proof verification.

A proof can be accepted as included under a verifier artifact commitment that was not the artifact used by the verifier. Applications relying on verifyBatchInclusion as evidence that a proof was verified against an expected verification key/program may accept unintended statements.

This does not require breaking the underlying proof system. The issue is in the binding between:

what the Merkle leaf claims was verified

and:

what the verifier backend actually verified

That distinction matters because the inclusion proof becomes an external evidence object consumed by applications.

Why this is reachable

The path appears reachable through normal request processing:

• VerificationData supports both fields.
• The SDK commitment path permits both fields and prioritizes vm_program_code.
• The batcher verifier permits both fields and uses verification_key for Gnark/Circom.
• The operator verifier uses verification_key for Gnark/Circom.
• The on-chain verifier only receives the final commitments and cannot reconstruct which field was consumed off-chain.

Since the submitter is also the party signing the request, request authentication does not prevent a malicious submitter from intentionally creating this inconsistent object.

Suggested mitigation

A robust mitigation would be to enforce a typed relation between proving_system and the auxiliary verifier artifact.

For example:

SP1:
  vm_program_code must be present
  verification_key must be absent

Risc0:
  vm_program_code must be present
  verification_key must be absent

Gnark*:
  verification_key must be present
  vm_program_code must be absent

Circom:
  verification_key must be present
  vm_program_code must be absent

Additionally:

1. Compute provingSystemAuxDataCommitment from the exact artifact consumed by the verifier backend.

2. Reject semantically irrelevant auxiliary fields before commitment generation, queue insertion, batch serialization, and operator verification.

3. Consider replacing the competing optional fields with a typed enum, so invalid combinations are unrepresentable.

4. Add a versioned domain prefix to the leaf encoding, for example:

leaf = H(
  "ALIGNED_VERIFICATION_DATA_V2",
  proving_system_id,
  proof_commitment,
  pub_input_commitment,
  verifier_artifact_commitment,
  proof_generator_addr
)

5. If backward compatibility is needed, explicitly version old and new leaf semantics.

Suggested formal property

A Rust property test could assert that the committed auxiliary artifact always equals the artifact actually consumed by the verifier backend:

proptest! {
    #[test]
    fn committed_auxiliary_artifact_equals_verifier_artifact(vd in arbitrary_verification_data()) {
        if validate_verification_data_shape(&vd).is_ok() {
            let committed = VerificationDataCommitment::from(vd.clone())
                .proving_system_aux_data_commitment;

            let used = verifier_auxiliary_artifact(&vd).unwrap();
            let expected = hash_auxiliary_artifact(used, vd.proving_system);

            prop_assert_eq!(committed, expected);
        }
    }
}

Negative tests should reject mixed auxiliary fields:

assert!(validate(Gnark {
    verification_key: Some(vk),
    vm_program_code: Some(bytes),
    ..
}).is_err());

assert!(validate(Circom {
    verification_key: Some(vk),
    vm_program_code: Some(bytes),
    ..
}).is_err());

assert!(validate(SP1 {
    verification_key: Some(vk),
    vm_program_code: Some(elf),
    ..
}).is_err());

A TLA+-style invariant could be:

CommittedAuxMatchesVerifierAux ==
  ∀ b ∈ AcceptedBatches:
    ∀ p ∈ b.proofs:
      p.leaf.auxCommitment =
        Hash(VerifierAux(p.verificationData), p.provingSystem)