Cowrie Research

circom-ecdsa-bigmod-remainder-range-check-omission-noncanonical-remainder-near-miss-2022-03-30

11 min read

circom-ecdsa BigMod Remainder Range-Check Omission / Non-Canonical Remainder Near Miss (2022-03-30)

  • Name: circom-ecdsa BigMod remainder range-check omission / non-canonical remainder near miss
  • Date: 2022-03-30
  • Protocol: circom-ecdsa / BigInt
  • Chain: Ethereum ecosystem
  • Category: bit-length precondition omission / bigint remainder canonicalization failure / library-level near miss
  • Loss: no public live exploit was documented, but any downstream circuit that treated BigMod’s mod[] output as a proper canonical bigint remainder could have been reasoning about a weaker statement than intended
  • Summary: circom-ecdsa’s BigMod(n, k) circuit used a helper long_div routine to witness a quotient div[] and remainder mod[] for big-integer modulo operations. The circuit correctly range-constrained each quotient limb with Num2Bits(n) but forgot to do the same for the remainder limbs. That omission mattered because the bigint library explicitly distinguished between proper representation and wider signed overflow representation: without per-limb width constraints on mod[], the remainder could satisfy the arithmetic identity while still living outside the canonical n-bit representation downstream consumers expected. In other words, a = q*b + r could hold in the circuit, yet r was not guaranteed to be the normal proper-form remainder other gadgets assumed they were receiving. Andrew He reported the issue in March 2022, and the merged fix added a mod_range_checks[k] loop so each remainder limb now passes through Num2Bits(n) before the result can be trusted as a canonical bigint object.
  • Trigger / entry point:
    • The affected circuit was BigMod(n, k) in circom-ecdsa’s bigint library.
    • BigMod obtained quotient and remainder witness arrays from the helper long_div function.
    • In the vulnerable code shape, the circuit instantiated one component range_checks[k + 1] array and applied Num2Bits(n) only to div[i] for 0 <= i <= k.
    • There was no sibling mod_range_checks[k] loop for mod[i], so the quotient was range-constrained into proper form while the remainder was merely assigned from the witness.
  • Root cause:
    • The circuit proved the algebraic division relation but not the full representation claim downstream consumers were relying on.
    • In this bigint library, proper representation is a stronger statement than some field elements that satisfy the same arithmetic equation.
    • Because mod[] lacked per-limb width checks, the remainder could remain in a wider or signed-overflow-style representation even while the top-level modulo relation still held.
    • The circuit therefore silently downgraded canonical remainder object into arithmetic witness that happens to satisfy the equality.
  • Failure path:
    1. A caller uses BigMod(n, k) and expects mod[] to be a proper k-limb base-2^n remainder.
    2. The witness generator produces quotient limbs div[] and remainder limbs mod[] via long_div.
    3. The circuit range-checks every quotient limb with Num2Bits(n) but leaves every remainder limb unconstrained at that representation boundary.
    4. The arithmetic identity tying a, b, div[], and mod[] can still verify even if mod[] is not in canonical proper representation.
    5. A downstream gadget or application that assumes mod[] is canonical may then derive proofs, comparisons, or reductions from a weaker object than intended.
  • What the attacker or failure needed to be true:
    • A downstream circuit had to consume BigMod under the assumption that mod[] was already in proper representation.
    • The vulnerable pre-fix BigMod implementation had to be in use.
    • The prover had to control witnesses tightly enough to exploit the missing remainder-width constraint.
    • No later canonicalization step could collapse or reject the non-canonical remainder before it influenced further logic.
  • Technical anatomy worth remembering:
    • This is a pure bit-length precondition omission case: the arithmetic helper relation was enforced, but one output object’s canonical-width assumption was never proven.
    • The asymmetry is the tell. The quotient already had a Num2Bits(n) loop; the remainder did not. That is exactly the kind of half-complete canonicalization reviewers should treat as suspicious in bigint circuits.
    • The library’s own representation model made the bug sharper. The circom-ecc spec defines a proper BigInt representation as limbs satisfying 0 <= a[i] < 2^n, while signed overflow representation only requires each limb to stay below roughly r/2 and interprets it through toZ(...). Leaving mod[] without limb-width checks therefore did not merely leave the remainder a little loose; it left it in the broader signed-overflow family when downstream gadgets were likely expecting proper base-2^n form.
    • The fix was minimal and revealing: split the old quotient-only range_checks array into div_range_checks plus a new mod_range_checks[k] loop, each using Num2Bits(n) on the corresponding limb. No exotic arithmetic redesign was needed; the real missing invariant was the width proof on the output object.
  • Representative circuits and artifacts:
    • Vulnerable circuit: circuits/bigint.circom template BigMod(n, k)
    • Vulnerable witness source: long_div(...) feeding div[] and mod[]
    • Missing invariant before the fix: no Num2Bits(n) range check over mod[i]
    • Spec artifact that made the bug semantically sharp: the circom-ecc spec’s distinction between proper BigInt representation and signed overflow representation
    • Report / fix PR: 0xPARC/circom-ecdsa#10 — BigMod incorrectly omits range checks on the remainder
    • Merged fix commit: 08c2c905b918b563c81a71086e493cb9d39c5a08
    • Patch shape: rename quotient checks to div_range_checks and add a new mod_range_checks[k] loop applying Num2Bits(n) to every mod[i]
  • Response / mitigation:
    • The maintainers merged the patch adding explicit Num2Bits(n) checks on the remainder limbs.
    • That restored the missing guarantee that mod[] is a proper canonical bigint object, not merely a witness satisfying the arithmetic equation.
    • The durable review lesson is broader than this one library: every bigint helper must prove canonical representation for every output other gadgets are expected to interpret semantically, not just for the output that looked more obviously dangerous at first glance.

Pattern tags

  • bit-length-precondition-omission
  • BigMod proved enough to show a division relation but not enough to guarantee that the remainder object lived in the canonical n-bit limb representation downstream circuits assumed.
  • The decisive failure was output-width asymmetry: div[] was range-checked into proper form, while mod[] was still trusted as if the same proof had already happened.

Three remainder-canonicalization promotions this incident collapsed

  1. A remainder-shaped object existed at all

    • long_div(...) emitted a witness array mod[], and the top-level division identity could still be satisfied with that witness.
    • That much only proved some field-element remainder object participates in this arithmetic relation; it did not yet prove this is the proper base-2^n bigint remainder other gadgets mean when they say mod.

  2. That witness still counted as canonical bigint remainder truth

    • The live bug sat here. BigMod quietly promoted mod[] satisfies the arithmetic identity alongside q and b into mod[] has already been proved to live in the canonical n-bit limb representation.
    • In other words, downstream consumers were handed a remainder object that looked like proper bigint output even though the circuit had never sealed the exact representation boundary that made it a proper-form remainder rather than a wider signed-overflow-style object.

  3. That accepted remainder truth still deserved downstream proof authority

    • Once the unchecked mod[] array was read as canonical bigint truth, later gadgets could compare it, hash it, reduce it again, or otherwise reuse it as if the representation question had already been settled.
    • The dangerous authority question was therefore not only did the modulo relation hold? but why did a remainder object that never earned canonical-form status still get to inherit downstream statement authority?

Why the exploit worked

  • The circuit enforced the arithmetic story but skipped part of the representation story. That gap matters in bigint libraries because consumers usually rely on both at once.
  • A non-canonical remainder can still satisfy the top-level equation while failing the stronger claim this is the unique proper-form remainder object that later gadgets expect.
  • Because quotient limbs were already range-checked, the remaining omission was easy to miss in review: the code looked like it had already done the serious canonicalization work.
  • This is why the bug belongs in bit-length precondition omission, not validation-output nonconsumption. The circuit was not ignoring a boolean check; it was failing to prove the width precondition on one of the outputs whose representation downstream code cared about.

Detection and audit pivots

  • In bigint gadgets, list every output and ask which of them are guaranteed to be in proper representation versus merely algebraically related to the inputs.
  • When one output array has Num2Bits checks and a sibling output array does not, assume the unchecked one is suspect until the representation argument is written out explicitly.
  • Treat quotient, remainder, carry, borrow, and limb-decomposition outputs as separate canonicalization problems; checking one does not make the others safe.
  • Audit helper libraries against their own representation taxonomy. If docs distinguish proper from signed overflow forms, any missing range proof can flip consumers into the wrong family.
  • Build adversarial tests for non-canonical outputs that still satisfy the base arithmetic identity; do not stop at honest quotient / remainder examples.

Why this incident matters

  • It gives the corpus a clean bigint-output exemplar for the bit-length precondition omission family, complementing comparator-style cases like Dark Forest.
  • It preserves an important zk review habit: arithmetic correctness and representation correctness are different claims, and protocols often need both.
  • It also shows how library-level zk bugs can sit latent as capability bugs rather than one named exploit: any downstream consumer that trusted the unchecked remainder could have inherited the weaker statement.

Failure-prevention checklist

  • Range-check every semantic output object of a bigint helper, not just the output that looks obviously primary.
  • Treat proper representation as a first-class proof obligation wherever downstream gadgets interpret limb arrays semantically.
  • Mirror constraints across symmetric outputs like quotient and remainder unless there is a written reason the representations may differ.
  • Build regression tests for non-canonical limb families that still satisfy the base arithmetic equation.
  • Keep library docs explicit about representation families and make the circuit prove the family each output claims to inhabit.
  • Review any helper returning multiple arrays for one is canonicalized, one is merely assigned asymmetry.
  • During audits, ask not only is the equation true? but also is the resulting object in the exact representation the next gadget assumes?
  • Prefer checked wrapper templates whose outputs are already canonical over helpers that hand later callers a raw arithmetic witness and expect them to remember extra range proofs.

Audit prompts

  • Which outputs of this bigint helper are guaranteed to be in proper representation, and where is each guarantee enforced?
  • Could a witness satisfy the top-level equation while leaving one output in signed-overflow or otherwise non-canonical form?
  • Are downstream consumers comparing, hashing, or reusing an output as if it were canonical even though the helper never proved that representation?
  • If quotient limbs are range-checked but remainder limbs are not, what exact argument says the remainder is still uniquely safe?
  • Does the library’s spec distinguish representation families more carefully than the circuit actually enforces?
  • After a refactor, which tests would fail if one output array silently lost its Num2Bits checks while the rest of the arithmetic still verified?

Lessons that should already be standard

  • Bigint arithmetic is not finished when the equation balances; the output object still needs a canonical representation proof.
  • Quotient-safe does not imply remainder-safe.
  • Representation-family bugs are especially dangerous in helper libraries because many downstream circuits inherit the same unchecked assumption at once.
  • Asymmetric canonicalization is a review smell. If sibling outputs are supposed to be semantically comparable, they usually need parallel width proofs.
  • A circuit that distinguishes proper from signed overflow representation in prose must also distinguish them in constraints.
  • The minimal patch often reveals the true missing invariant: here it was just the absent Num2Bits(n) loop on mod[].

Internal linkages

Control surface

Graph View

Backlinks