Cairo Unchecked Division

Overview

This detector reports division operations whose divisor is never asserted to be non-zero or bounded. Division in Cairo behaves differently depending on operand type. Over felt252, division is field division — multiplication by the multiplicative inverse — and a zero divisor is undefined and aborts. Over the integer types u256/u128/u64, division by zero panics. Either way, an unguarded divisor that an attacker can drive to zero gives them a cheap way to make the transaction fail.

Field division also has a subtler hazard: because a / b over felt252 means a * b^{-1} mod p, the quotient is a field element, not a rounded integer. Code that treats a felt division result as if it were integer division can produce a value that is mathematically valid in the field but wrong for the intended accounting. An unbounded, attacker-influenced divisor widens the range of such surprising results.

Why This Is an Issue

The most direct impact is denial of service. A function that computes total / n where n comes from the caller will abort whenever the caller passes zero. If that function is on a path other users depend on — a distribution, a settlement, a liquidation — a single attacker-supplied zero can stall it.

The accounting impact is specific to felt division. A developer who writes let share = pool / participants; expecting integer division gets the field inverse instead, which for most operand values is a large, unpredictable field element rather than the intended per-participant amount. If that result feeds a payout, the payout is wrong.

How to Resolve

Assert the divisor is non-zero before dividing, and prefer integer types when integer-division semantics are intended.

// Vulnerable: divisor n is unchecked
#[external(v0)]
fn distribute(ref self: ContractState, total: u256, n: u256) {
    let share = total / n;          // aborts if n == 0
    self.share.write(share);
}

// Fixed: divisor asserted non-zero, integer type for integer division
#[external(v0)]
fn distribute(ref self: ContractState, total: u256, n: u256) {
    assert(n != 0, 'div by zero');
    let share = total / n;          // u256 division: rounds toward zero
    self.share.write(share);
}

When working over felt252, be explicit about whether field division or integer division is wanted; if integer semantics are required, convert to a u* type first.

Detection Methodology

The detector scans each function for operations whose expression contains a division operator, taking care to ignore // comment markers and path separators. For each division it extracts the divisor identifier and checks whether that identifier appears inside any assertion expression collected from the same function. If the divisor is referenced by an assertion, the operation is treated as guarded and skipped; otherwise it is reported.

The divisor extraction is textual and identifier-based, so it matches a named divisor against named assertions rather than performing a semantic check that the assertion truly forces non-zeroness.

Limitations

The non-zero check is satisfied by any assertion mentioning the divisor name, so an assertion that references the divisor without bounding it (a false negative) suppresses the finding.
Divisors that are compound expressions rather than a single identifier may not be matched against their guarding assertion.
The detector does not distinguish field division from integer division, so it cannot separately flag the felt-semantics hazard from the zero-divisor hazard.

Cairo Unchecked Felt Arithmetic — unbounded felt add/sub/mul
Division by Zero Risk — the Circom analogue over a finite field
Unconstrained Divisor — Circom division by a fully prover-controlled signal

References

Sample Sigvex Output

{
  "detector": "cairo-unchecked-division",
  "severity": "medium",
  "confidence": 0.70,
  "title": "Division without divisor check in `distribute` at line 4",
  "template": "distribute",
  "signal": "share",
  "line": 4,
  "description": "Operation `total / n` in function `distribute` divides without asserting that the divisor is non-zero or bounded. Division-by-zero aborts the transaction; unbounded divisors can combine with felt semantics to produce unexpected quotients.",
  "recommendation": "Assert the divisor is non-zero and, where relevant, bounded: `assert(divisor != 0, 'div by zero');`"
}