Description

The function UniversalBatchVerifierChip::check_padding in circuits/src/batch_verify/universal/chip.rs is intended to perform step 1a of the specification. This is done by constructing a bitmask that will have 1 for entries that may be arbitrary and 0 for entries that must be padding. This bitmask is obtained as follows:

// Bitmask computation
let max_len = entry.public_inputs.0.len();
let number_of_non_padding_elements =
    self.gate().add(ctx, entry.len, entry.has_commitment);
self.range().check_less_than_safe(
    ctx,
    number_of_non_padding_elements,
    (max_len + 1) as u64,
);
let bitmask = first_i_bits_bitmask(
    ctx,
    self.gate(),
    number_of_non_padding_elements,
    max_len as u64,
);

According to the specification, the intention here is to enforce that entry.len + entry.has_commitment <= max_len, and the left-hand side is then used for the bitmask.

However, if entry.len = F::MODULUS - 1, and entry.has_commitment = 1, then a wraparound will happen on the addition, and we will have number_of_non_padding_elements = 0, which will then pass the inequality check. So in that case, UniversalBatchVerifierChip::check_padding does not constrain entry.len as it should according to the specification of 1a.

Impact

We can first note that changing the len field of a batch entry to a different value will change the circuit ID, so it is unlikely an attacker would be able to profit from the bug described so far.

However, due to other constraints, it is actually not possible in practice to prove the UniversalBatchVerifier circuit with entry.len = F::MODULUS - 1 and entry.has_commitment = 1. This is due to the function UniversalBatchVerifierChip::constrain_commitment_hash, which is implemented as follows:

fn constrain_commitment_hash(
    &self,
    ctx: &mut Context<F>,
    entry: &AssignedBatchEntry<F>,
) {
    let max_len = entry.public_inputs.0.len() as u64;
    let bitmask = ith_bit_bitmask(ctx, self.gate(), entry.len, max_len);
    let bits = bitmask.iter().map(|b| QuantumCell::<F>::from(*b));
    let lth_public_input = self.gate().inner_product(
        ctx,
        entry.public_inputs.0.iter().copied(),
        bits,
    );
    let expected =
        self.gate()
            .mul(ctx, entry.commitment_hash, entry.has_commitment);
    ctx.constrain_equal(&lth_public_input, &expected);
}

As entry.len = F::MODULUS - 1, the bitmask used here will be all zero, so then lth_public_input will also be zero. As we have entry.has_commitment = 1, we will then need to have entry.commitment_hash = 0. The rest of the circuits imply that this requires an attacker to find a keccak preimage of a multiple of F::MODULUS, which should be computationally infeasible.

Recommendations

We recommend ensuring the intended inequality in UniversalBatchVerifierChip::check_padding by ruling out the wraparound, for example by performing a range check on entry.len that ensures that entry.len must be smaller than F::MODULUS - 1.

Remediation

This issue has been acknowledged by Nebra, and a fix was implemented in commit 3af8a51e↗.