Cairo Unchecked Felt Arithmetic

Overview

Cairo’s native numeric type is felt252, an element of the Starknet field whose order is a prime close to 2^251. Every +, -, and * on a felt252 is implicitly taken modulo that prime. There is no overflow trap: a sum that exceeds the field order wraps back into range, and a subtraction that goes below zero wraps to a value near the prime. This is identical in spirit to modular arithmetic in any other prime field, and it is the opposite of how Cairo’s u256/u128 integer types behave, which abort on overflow.

This detector flags felt252 arithmetic inside functions that can change contract state and that contain no assert at all. The reasoning is that an author who has bounded their operands will normally have written at least one assertion to document and enforce that bound. A state-changing function performing raw felt arithmetic with zero assertions is the pattern most likely to feed an attacker-influenced, silently-wrapped value into storage, a return value, or an external call. Pure view helpers that do not mutate state are excluded, since for them a wrapped value is a correctness concern rather than a direct exploitability one.

Why This Is an Issue

A balance update written as let new = old + amount; over felt252 looks correct by inspection. If amount is large enough that old + amount exceeds the field prime, the stored result is old + amount - p, a small number. An attacker who controls amount can drive a balance, a counter, or an accounting total to an arbitrary value without any operation appearing to fail. The transaction succeeds, the event logs look normal, and the contract’s internal invariant is quietly broken.

The same hazard applies to subtraction used as an underflow-sensitive check. In the field, 5 - 10 is p - 5, an enormous value that passes any naive “is this positive” test. Comparison logic written for two’s-complement integers does not translate to field elements.

How to Resolve

Bound the operands before using the result, or move the arithmetic to an integer type that traps on overflow. The integer-type approach is usually the cleaner fix for value-bearing quantities such as balances and amounts.

// Vulnerable: raw felt arithmetic feeds storage, no bound asserted
#[external(v0)]
fn deposit(ref self: ContractState, amount: felt252) {
    let new_total = self.total.read() + amount; // wraps mod p silently
    self.total.write(new_total);
}

// Fixed: use a trapping integer type for value arithmetic
#[external(v0)]
fn deposit(ref self: ContractState, amount: u256) {
    // u256 addition reverts on overflow instead of wrapping
    let new_total = self.total.read() + amount;
    self.total.write(new_total);
}

If the value genuinely must stay a felt252, assert the operands fit a known range before the operation: assert(amount < MAX_DEPOSIT, 'amount too large');.

Detection Methodology

The detector walks each parsed function and collects its felt-arithmetic operations. A function is a candidate only when it performs at least one such operation, changes or can change state, and contains no assertion anywhere in its body. Functions that assert something are treated as having an author-supplied bound and are skipped, as are pure view helpers that do not mutate state. Each unguarded felt operation in a candidate function is reported individually so the finding points at the specific line.

The assertion check is deliberately coarse: any assert is taken as evidence that the author considered ranges, even if that particular assertion does not bound the operands of every operation. This keeps false positives low at the cost of missing functions that assert one thing but compute another.

Limitations

• Treating the mere presence of an assert as a range guard means a function that asserts an unrelated property suppresses the finding (a false negative).
• The detector does not perform value-range analysis, so it cannot tell a provably-bounded felt operation from a dangerous one; it relies on the assert heuristic.
• Arithmetic split across helper functions is analysed per function, so a bound established in a caller is not propagated to a callee.

Related Detectors

• Cairo Unchecked Division — division without a non-zero divisor guard
• Cairo Narrow Int Return — felt downcast to a narrow integer without a range check
• Field Overflow — the Circom analogue for field-prime wrapping

References

• Cairo Book: Felt252
• Cairo Book: Integer Types and Overflow
• Starknet Documentation: Cairo and the Sequencer
• Bailey, B., Miller, A. “An Empirical Study of ZK Circuit Bugs.” IACR ePrint 2023/190.

Sample Sigvex Output

{
  "detector": "cairo-unchecked-felt-arithmetic",
  "severity": "medium",
  "confidence": 0.70,
  "title": "Unchecked felt arithmetic in `deposit` at line 4",
  "template": "deposit",
  "signal": "new_total",
  "line": 4,
  "description": "Operation `self.total.read() + amount` in function `deposit` performs felt arithmetic but the function has no `assert` statements. Felt252 values wrap modulo the Starknet prime (~2^251); arithmetic that feeds storage or return values can silently produce wrapped results if operands are attacker-controlled.",
  "recommendation": "Bound operands with explicit assertions (e.g. `assert(a < MAX, 'overflow')`) before using the result, or use `u256`/`u128` arithmetic which traps on overflow."
}