Cowrie Research

zk-email-verify-revealsubstring-lessthan-exclusive-upper-bound-bit-width-omission-near-miss-2025-11-12

10 min read

zk-email-verify RevealSubstring LessThan Exclusive-Upper-Bound Bit-Width Omission Near Miss (2025-11-12)

  • Name: zk-email-verify RevealSubstring LessThan exclusive-upper-bound bit-width omission near miss
  • Date: 2025-11-12
  • Protocol: zk-email-verify / RevealSubstring
  • Chain: Ethereum ecosystem
  • Category: bit-length precondition omission / exclusive-upper-bound comparator overflow / library-level near miss
  • Loss: no public live exploit was documented, but RevealSubstring’s boundary checks were instantiated outside circomlib LessThan(n)’s intended domain whenever an exclusive upper-bound constant itself was a power of two; the helper could therefore prove a weaker or malformed substring-bound statement than downstream circuits thought they were getting
  • Summary: zk-email-verify’s RevealSubstring(maxLength, maxSubstringLength, shouldCheckUniqueness) helper added three LessThan(...) checks to keep substring start, substring length, and start + length inside bounds. The mistake was subtle and classic: each comparator width was computed from the exclusive upper-bound constant itself. That is safe only when the constant is strictly below the comparator’s maximum representable value. When maxLength, maxSubstringLength + 1, or maxLength + 1 is a power of two, the constant equals 2^n while LessThan(n) expects both operands to fit in [0, 2^n - 1]. The result is a hidden-domain bug right at the range-check boundary: the circuit still looks like it is proving substringStartIndex < maxLength, substringLength <= maxSubstringLength, and substringStartIndex + substringLength <= maxLength, but it is doing so with a comparator call whose semantic preconditions have already failed. The public bug report pointed to commit 800b9a1, and the follow-up fix PR corrected the formulas to leave one extra representable value of headroom — log2Ceil(maxLength + 1), log2Ceil(maxSubstringLength + 2), and log2Ceil(maxLength + 2) — while also adding a focused regression test.
  • Trigger / entry point:
    • The affected helper was packages/circuits/helpers/reveal-substring.circom in zk-email-verify.
    • RevealSubstring used circomlib LessThan(n) to validate three boundary conditions before extracting and optionally uniqueness-checking a revealed substring.
    • The vulnerable formulas derived n from the exclusive upper-bound constants themselves instead of from the maximum value any comparator input might actually take.
    • That becomes wrong whenever one of those constants is a power of two.
    • The repository’s own test circuit instantiated RevealSubstring(256, 16, 1), so the first check concretely became LessThan(8)([substringStartIndex, 256]) — exactly the kind of constant = 2^n call shape the report flagged.
  • Root cause:
    • The circuit treated log2Ceil(bound) as if it were automatically the right comparator width for a proof of x < bound.
    • But when the bound itself is an input to LessThan(n), the comparator needs enough width to represent the bound too, not just honest values below it.
    • RevealSubstring therefore encoded exclusive upper bound as if it were largest representable operand, collapsing two different facts into one formula.
    • The circuit was proving some comparator relation over field elements rather than the sharper intended claim these dynamic indices are bounded by these exact exclusive upper limits inside the comparator's sound domain.
  • Failure path:
    1. A caller instantiated RevealSubstring with a power-of-two boundary such as maxLength = 256, or with some other parameters that made maxSubstringLength + 1 or maxLength + 1 a power of two.
    2. The helper computed comparator widths as log2Ceil(maxLength), log2Ceil(maxSubstringLength + 1), and log2Ceil(maxLength + 1).
    3. At least one resulting LessThan(n) call then received an upper-bound constant equal to 2^n, which is outside the helper’s documented input domain.
    4. The boundary check bit no longer cleanly meant this witness is inside the intended substring bound; it only meant this witness satisfied a comparator invocation that was already operating outside its intended width assumptions.
    5. Any downstream circuit reusing RevealSubstring inherited that weaker or malformed range statement at exactly the point where substring extraction was supposed to become semantically safe.
  • What the attacker or failure needed to be true:
    • A downstream circuit had to rely on the vulnerable RevealSubstring implementation introduced in commit 800b9a1.
    • Parameters had to make one of the exclusive upper-bound constants land exactly on a power-of-two boundary.
    • Witness-controlled substring indices or lengths had to matter to correctness, uniqueness checks, or proof semantics downstream.
    • No later constraint or wrapper could independently re-prove the same bounds with correct headroom.
  • Technical anatomy worth remembering:
    • This is the exclusive upper bound is itself a comparator operand version of bit-length precondition omission. The bug is not that LessThan was missing; the bug is that the circuit forgot that bound also has to fit in the comparator’s operand domain.
    • The smell is LessThan(log2Ceil(bound))([x, bound]). For strict < bound checks, that formula fails exactly where systems often like to parameterize things: powers of two.
    • The repository’s own RevealSubstring(256, 16, 1) test fixture is the crisp preserved example. 256 is a natural byte-oriented bound, but it makes the vulnerable start-index check instantiate the forbidden bound = 2^n shape directly.
    • The fix is revealing because it is tiny and semantic. Nothing about substring extraction changed; only the comparator widths gained one extra representable value of headroom so the boundary checks finally proved the intended statement instead of a folklore approximation of it.
  • Representative circuits and artifacts:
    • Vulnerable helper: packages/circuits/helpers/reveal-substring.circom
    • Vulnerable start-index check: LessThan(log2Ceil(maxLength))([substringStartIndex, maxLength])
    • Vulnerable length check: LessThan(log2Ceil(maxSubstringLength + 1))([substringLength, maxSubstringLength + 1])
    • Vulnerable sum check: LessThan(log2Ceil(maxLength + 1))([sum, maxLength + 1])
    • Public issue report: zkemail/zk-email-verify#289 ([Bug] Incorrect LessThan bit-widths when comparing against constants)
    • Public fix PR: zkemail/zk-email-verify#321 (fix: correct RevealSubstring LessThan bit widths)
    • Concrete power-of-two instantiation in repo tests: packages/circuits/tests/test-circuits/reveal-substring-test.circom with component main = RevealSubstring(256, 16, 1);
    • Fix shape: widen comparator widths to log2Ceil(maxLength + 1), log2Ceil(maxSubstringLength + 2), and log2Ceil(maxLength + 2) and add packages/circuits/tests/reveal-substring-bit-width.test.ts
  • Response / mitigation:
    • The public fix PR updates all three comparator-width formulas to leave one representable value of headroom for the exclusive upper-bound constants themselves.
    • The PR also adds a regression test that checks for the corrected formulas in source, preserving the exact boundary arithmetic that failed here.
    • As of this review, the public issue and fix PR were still open, so the preserved lesson is not only how to fix it but also how easy it is for a helper-domain bug to linger in a widely reused proof component after disclosure.

Pattern tags

  • bit-length-precondition-omission
  • RevealSubstring visibly had range checks, but the checks were parameterized with comparator widths that stopped one bit too early whenever the exclusive upper-bound constant itself hit a power of two.
  • The decisive failure was not validation result ignored; it was validation helper called outside the width domain that made its result mean the intended bound statement.

Why the exploit worked

  • The helper conflated bit length of the exclusive bound with bit length required to represent every operand passed into the comparator.
  • That distinction disappears for non-power-of-two constants, which is why the bug is easy to miss in review. It becomes sharp exactly at power-of-two boundaries, where protocol authors often prefer to parameterize lengths, buffer sizes, or byte-oriented limits.
  • Once bound = 2^n, the call shape LessThan(log2Ceil(bound))([x, bound]) no longer proves the intended semantic claim. The circuit still consumes the comparator output, but it is consuming the output of a helper that has already left its sound domain.
  • This is why the incident belongs in bit-length precondition omission, not validation-output nonconsumption. The checks were present and enforced; the hidden width premise that made those checks meaningful was not.

Detection and audit pivots

  • Grep for LessThan(log2Ceil( or similar Comparator(widthFromBound) patterns and inspect every place where the bound constant is also passed as an operand.
  • Treat x < bound and bound fits in the comparator domain as separate proof obligations. They only look like one formula until the first power-of-two parameter shows up.
  • Add tests for bound = 2^n, bound = 2^n + 1, and adjacent parameterizations rather than stopping at small non-power-of-two examples.
  • When auditing reusable substring, slice, index, or parser helpers, check whether boundary parameters are natural byte multiples or powers of two; those configurations are where exclusive-upper-bound comparator bugs hide most cleanly.
  • Distinguish helper called, helper output enforced, and helper output meaningful. This family fails at the third step.

Why this incident matters

  • It gives the corpus a very clean power-of-two exclusive upper bound exemplar for the bit-length precondition omission family, complementing Dark Forest’s signed-coordinate comparator case and circom-ecdsa’s bigint-output canonicalization case.
  • It preserves a review habit that matters far beyond email circuits: any time a helper compares a dynamic value against a constant upper bound, the constant itself still has to fit the helper’s operand domain.
  • It also shows how these bugs can survive in innocuous-looking parsing or reveal helpers rather than only in obviously monetary circuits. Once such a helper becomes a shared proof component, the bug’s blast radius is every later circuit that inherits its boundary semantics.

Failure-prevention checklist

  • For every strict upper-bound check of the form x < bound, size the comparator from the largest operand it will see, not from the honest range of x alone.
  • Treat bound is representable as an explicit constraint requirement whenever bound is passed into a proof helper as data rather than staying compile-time folklore.
  • Add regression tests specifically for power-of-two bounds and +1 / +2 headroom formulas.
  • Keep reusable substring and parser helpers self-checking: if a template advertises bounded extraction, it should prove the exact comparator-domain assumptions internally.
  • Review byte-oriented constants (32, 64, 128, 256, 1024) with extra suspicion in Circom comparator code; they are where hidden width mistakes often become real.
  • Preserve source-level tests for width formulas in addition to witness examples so future refactors cannot silently collapse the headroom again.
  • When a helper is library-level, treat open bug reports as transitive risk for downstream circuits until the patched statement is what production actually compiles.

Audit prompts

  • If this comparator checks x < bound, where is the proof that bound itself fits in the comparator’s operand domain?
  • What happens when the configured bound is exactly 2^n rather than 2^n - 1?
  • Is the circuit sizing its comparator from the semantic bound or from the largest actual operand value?
  • Are natural byte-sized or power-of-two configuration values disproportionately likely to hit a hidden helper-domain boundary?
  • Would a source-level regression test fail if someone rewrote log2Ceil(bound + 1) back to log2Ceil(bound) during refactoring?
  • Does the downstream circuit rely on this helper as a complete semantic admission check, or is there another correctly bounded wrapper later in the statement?

Lessons that should already be standard

  • x < bound is not one proof obligation when bound itself is also a runtime comparator operand.
  • Power-of-two bounds are where width folklore breaks.
  • A visible range check can still be semantically weak if its helper is instantiated one bit outside its sound domain.
  • Reusable parser or substring helpers are proof-boundary code, not harmless utility code.
  • The smallest arithmetic patch often reveals the missing statement invariant most clearly: here it was one extra representable value of headroom for each exclusive upper-bound constant.
  • Open fix PRs still count as live review evidence that the old proof statement remains reachable somewhere.

Internal linkages

Control surface

Graph View

Backlinks