Skip to content

Z007.md

Latest commit

 

History

History
83 lines (58 loc) · 2.48 KB

Z007.md

File metadata and controls

83 lines (58 loc) · 2.48 KB
Raw

Z007: Under-Constrained Circuit Inputs

Severity

HIGH - Enables field-overflow attacks on ZK circuits

Description

Detects circuit signals/inputs used in arithmetic or comparisons without accompanying range-check constraints, allowing attackers to exploit field overflow to bypass validation logic.

Vulnerable Pattern (Circom)

// ❌ BAD: No range constraint
signal input amount;
signal input balance;
signal output isValid;

// Field overflow possible - amount could be negative in field arithmetic!
isValid <== amount < balance;

Attack: Attacker provides amount = p - 1 (where p is field modulus), which wraps to -1, bypassing the check.

Secure Pattern (Circom)

// ✅ GOOD: Range check enforced
signal input amount;
signal input balance;
signal output isValid;

// Ensure amount is in valid range (64 bits)
component amountCheck = Num2Bits(64);
amountCheck.in <== amount;

component balanceCheck = Num2Bits(64);
balanceCheck.in <== balance;

// Now safe to compare
isValid <== amount < balance;

Why This Matters

Under-constrained circuits are the #1 finding in ZK audits. Field overflow allows:

  • Bypassing balance checks (send more than you have)
  • Manipulating age/time constraints
  • Breaking merkle proof validation
  • Forging identity credentials

Detection Method

Requires circom/Noir circuit source parsing (#1227):

  1. Parse circuit and build signal dataflow graph
  2. Find signals used in arithmetic (+, -, *, /) or comparisons (<, >, ==)
  3. Check for preceding range-check templates:
    • Circom: Num2Bits, LessThan, RangeCheck
    • Noir: assert_max_bit_size, range constraints
  4. Flag unconstrained signals

Dependencies

  • #1227: Circom parser integration (BLOCKS THIS RULE)
  • #1192, #1194: ZK infrastructure

Deep Verification (SMT)

When invoked with --deep-verify, Sanctifier translates the circuit constraint set into Z3 SMT assertions and checks whether each signal used in a comparison is provably bounded (see smt::circuit_range and ADR-006).

This is an optional, computationally expensive pass that goes beyond heuristic pattern matching to provide a formal proof of under-constrained signals.

References

Examples

See fixtures after #1227 integration.