Missing Range Constraints for Sha256Bytes Allow Forged Inputs to Pass Verification

[ArmanKolozyan]

I would like to report a security vulnerability related to missing range checks at the call sites of the Sha256Bytes template, which internally uses the Sha256General template.

Issue Description

The Sha256General template (which is instantiated inside Sha256Bytes ) implements SHA-256 hashing over padded input blocks. It enforces several constraints to ensure correct operation:

1. It checks that the input padded bit length paddedInLength is less than or equal to a maximum, using LessEqThan(n).
2. It checks that paddedInLength is a multiple of 512, via an equality constraint with inBlockIndex * 512.
3. It uses the value inBlockIndex - 1 as an index for the internal selector logic (implemented using ArraySelector or ItemAtIndex), which uses LessThan(n) internally to verify that the index lies within bounds.

However, these comparator templates (LessEqThan(n), LessThan(n), etc.) from circomlib assume that their inputs are already bounded to n bits and do not enforce such constraints internally (for performance reasons). This introduces a vulnerability: if the input is not explicitly range-constrained using Num2Bits(n) before being passed into these comparators, the circuit can be tricked into accepting out-of-range values.

According to the Sha256General template documentation, it is assumed that:

@input paddedInLength Length of the padded message; assumes to be in `ceil(log2(8 * maxByteLength))` bits

This assumption must be enforced by the "caller" of the template.

For background on this type of issue, please see:

• zk-bug-tracker #4: Mismatching Bit Lengths
• BlakeMScurr/comparator-overflow

Problematic Call Sites

In this project, the Sha256Bytes template is used in ShaBytesDynamic without applying the required range checks. The callers of ShaBytesDynamic also do not seem to do any range checks.

Exploits

We demonstrate two exploits that highlight this vulnerability:

1. Length Check Bypass (LessEqThan only)

We hereby bypass the LessEqThan check with a value > maxBitsPadded, which is intended to enforce the constraint in_len_padded_bits ≤ maxBitsPadded. To set up this example, we instantiate the Sha256General template with:

maxBitsPadded = 3 * 512 = 1536

This corresponds to 3 full 512-bit SHA-256 blocks. From this value, the following internal parameters are derived in the template:

maxBitsPaddedBits = ceil(log2(1536)) = 11

This leads to the instantiation of:

component bitLengthVerifier = LessEqThan(11);
bitLengthVerifier.in[0] <== in_len_padded_bits;
bitLengthVerifier.in[1] <== 1536;
bitLengthVerifier.out === 1;

Notice that LessEqThan(11) assumes that in[0] is less than 2¹¹ = 2048, but this is not enforced anywhere! A malicious prover can thus supply a much larger field element, cause an overflow, and pass the check. Specifically, we set:

in_len_padded_bits = p − 1

where p is the BN254 scalar field modulus used by Circom:

p = 21888242871839275222246405745257275088548364400416034343698204186575808495617

We also satisfy the accompanying equality:

in_len_padded_bits === inBlockIndex * 512

by setting:

inBlockIndex = (p − 1) / 512 = 42750474359061084418450011221205615407321024219562567077535555051905875968

All remaining lines until the LessThan consist of assert statements and weak assignments using <--, which do not contribute any constraints that are enforced by the verifier. As a result, they can be ignored in the context of our attack.

The LessEqThan(11) check passes because it internally performs the check by computing:

z = in[0] + 2^11 − 1536 = in[0] + 2048 − 1536 = in[0] + 512

and then decomposes z into 12 bits using Num2Bits(12) (this check is for the difference calculated inside the template, not for the inputs!). The check passes if:

0 ≤ z < 2^12 = 4096

It then verifies that the most significant bit of the 12-bit decomposition of z is zero. In other words, that:

0 ≤ z < 2^12 = 4096

In our case, we set:

in[0] = in_len_padded_bits = p − 1

So:

z = p − 1 + 512 ≡ 511 mod p

Since 511 < 4096, the check passes, even though in_len_padded_bits ≫ 1536! This allows the constraint to be satisfied despite the value being well outside the intended range.

The following files are included to reproduce and validate the exploit:

• sha256_lessthan_attack.circom: A template containing all the relevant constraints.
• input_lessthan.json: The specific inputs that satisfy the constraints while triggering the overflow.

2. Selector Bypass (latest update has prevention in place!)

If we continue looking at what happens further in the Sha256General template with the same forged values used in Exploit 1, we find a second vulnerability, this time in the ArraySelector component.

After computing inBlockIndex (which we set to (p − 1) / 512), the template computes an index:

index = inBlockIndex − 1

This index is then passed into 256 parallel instances of ArraySelector, each of which selects one SHA-256 output word based on the provided index. Internally, each ArraySelector includes the following comparator:

component lt = LessThan(bits);
lt.in[0] <== index;
lt.in[1] <== choices;
lt.out === 1;

This is intended to check that index < choices, where:

choices = maxBlocks = maxBitsPadded / 512 = 3
bits = maxBlocksBits = ceil(log2(3)) = 2

However, just like LessEqThan(n), the LessThan(n) comparator assumes that its inputs are less than $2^n$, and does not internally enforce this with a Num2Bits check.

We now exploit this by continuing from our earlier forged values, but adjusting inBlockIndex to be:

inBlockIndex = 0
index = inBlockIndex − 1 = p − 1

Now the internal value that LessThan(2) computes is:

z = index + 2^2 − 3 = (p − 1) + 4 − 3 = p ≡ 0 mod p

Since z = 0, the check passes because 0 < 2^2 = 4, and the MSB of its 3-bit binary decomposition is zero. Thus, lt.out === 1, even though index ≫ choices = 3.

This allows the prover to silently bypass the intended range check on the selector index.

The attack continues as follows: each ArraySelector tries to compare the index to values i ∈ [0, 1, 2] using IsEqual(i, index). But since index = p − 1, no equality will succeed. As a result:

eqs[i].out = 0  for all i
calcTotal.sum = 0

Each of the 256 selectors will output zero, and so Sha256General returns an all-zero SHA-256 output, even though no valid compression block was selected. All constraints still pass.

In practice, this means that a malicious prover can convince the verifier that a padded message hashes to a block of all-zero bits, while the verifier has no way of detecting that the output is completely detached from the real SHA-256 state.

We include the following files to reproduce and validate this exploit:

• sha256_attack.circom: A template containing all the relevant constraints.
• input.json: The crafted witness values that satisfy all constraints while bypassing the selector range check.

Note: The latest version of the zk-email verifier has replaced ArraySelector with ItemAtIndex, which enforces correctness by checking that exactly one index matches. This prevents my second exploit by design.

Recommendations

This vulnerability can be fixed at the call sites by explicitly constraining the input using Num2Bits:

component lenBits = Num2Bits(maxBitsPaddedBits);
lenBits.in <== in_len_padded_bytes * 8;