Integer Overflow & Underflow

Domain

Web3 & smart contracts

ROOTVIEL support

Verified by ROOTVIEL — A deterministic, LLM-free verifier settles a specific property under stated assumptions — either a structural property over a graph, or an effect reproduced in execution. It does not by itself mean the whole system is secure, nor that an end-to-end exploit was run beyond what the evidence scope states.

Evidence scope

Observed in execution — Reproduced in an isolated sandbox or local fork — the effect was actually triggered under stated conditions.

Analysis family

RootRaven

CWE

CWE-190, CWE-191

OWASP

SC08

An integer overflow occurs when an arithmetic operation produces a value larger than the maximum representable by its type; an underflow when it produces a value below the minimum. Because EVM integers are fixed-width two’s-complement (for signed) or unsigned binary of a declared bit-width, the out-of-range result is not rejected — it is reduced modulo 2^N, so the value "wraps" to the opposite end of the range.

In the context of a smart contract the danger is not the wrap itself but what the wrapped value is then used for: a balance, a supply total, an allowance, a loop counter, a price, or a comparison that gates access. A single wrap can turn "subtract 1 from a zero balance" into "balance is now 2^256 − 1", which downstream code reads as near-infinite funds.

This class spans two eras of Solidity. Before version 0.8.0, all arithmetic wrapped silently and contracts defended themselves with library wrappers (the SafeMath pattern) applied by hand to every operation. From 0.8.0 onward the compiler emits overflow/underflow checks by default, reverting on wrap — which moved the risk from "forgot to use SafeMath" to "deliberately opted out of the checks".

• ▸Pre-0.8 contracts (still live and still forked) where any unprotected +, −, * can wrap.
• ▸Modern contracts using unchecked { ... } blocks for gas savings in loops or math the author believes cannot overflow.
• ▸Narrowing casts such as uint256 → uint128 / uint64, which truncate high bits with no check even under 0.8.
• ▸Inline assembly (Yul) arithmetic (add, sub, mul, mod), which never carries the compiler’s checks.
• ▸Fixed-point token math where a multiply by 10^18 before dividing pushes an intermediate value past the type’s range.

The EVM word is 256 bits. Every value ultimately lives in a 256-bit slot, and the native arithmetic opcodes (ADD, SUB, MUL) operate modulo 2^256 with no notion of signedness and no trap on carry. Signed interpretation (SDIV, SMOD, SLT, SGT) is layered on top by the compiler; the hardware itself only ever computes modular results. "Overflow checking" is therefore not a CPU feature the EVM provides — it is extra bytecode the compiler chooses to emit.

Solidity types narrower than 256 bits (uint8 … uint248, intN) are stored in the 256-bit word but are conceptually masked to their width. When you assign a wider value into a narrower variable, or cast down, the high bits are discarded. This is distinct from arithmetic overflow: it is truncation, and the 0.8 default checks do not catch it — casts are explicit and the language treats them as the author’s intent.

Modular (wraparound) arithmetic

Results reduced modulo 2^N for an N-bit type, so MAX + 1 == 0 and 0 − 1 == MAX.

Checked arithmetic

Solidity ≥0.8 default: the compiler inserts a comparison after +/−/* and reverts with Panic(0x11) on overflow/underflow.

unchecked block

A Solidity ≥0.8 scope in which the inserted checks are suppressed, restoring pre-0.8 wraparound for gas savings.

Narrowing cast

uintM(x) where x has more significant bits than M — the extra high bits are truncated silently, with no check even under 0.8.

Panic(0x11)

The standard revert reason the checked path raises on arithmetic overflow/underflow; useful as a detection signal in tests and traces.

The root cause is a mismatch between the programmer’s mental model of arithmetic (unbounded integers over the reals) and the machine’s model (fixed-width residues modulo 2^N). The contract computes a value assuming it cannot exceed a natural bound, but the type permits it to wrap, and the wrapped value is accepted as valid by the surrounding logic because no invariant re-checks it.

In pre-0.8 code the defect is omission: a missing SafeMath call. In modern code it is commission: an unchecked block entered on a false premise ("this sum can never overflow"), a cast chosen for packing without re-validating the magnitude, or assembly written to save gas. In every case the deeper cause is the same — an arithmetic bound that the code relies on but never enforces at the point where the value is produced.

The canonical shape is an underflow on a subtraction whose minuend the attacker controls, turning a decrement into a maximal balance; the overflow variants are symmetric.

1. 1The attacker locates an arithmetic expression on a value they influence (a balance, an amount parameter, a loop bound) that is not re-validated against its natural bound.
2. 2They supply inputs that drive the operation past the type edge — e.g. transferring an amount greater than their balance into balances[msg.sender] -= amount in a pre-0.8 contract, or a crafted amount inside an unchecked block.
3. 3The operation wraps: a subtraction below zero becomes a value near 2^256, or an addition past the maximum becomes a small value.
4. 4The wrapped value is written back to storage and treated as authoritative by the rest of the contract — the attacker now "owns" a balance they never funded, or an accounting total has been zeroed.
5. 5The attacker monetises the corrupted state: withdrawing, transferring, or redeeming against the inflated figure before any invariant notices the inconsistency.

A synthetic, minimal token. The pre-0.8 pragma means every operation wraps, so the subtraction in transfer underflows when amount exceeds the sender’s balance. The modern variant below it shows the same bug reintroduced under 0.8 via an unchecked block and a narrowing cast.

synthetic — do not use; pre-0.8 silent wraparound
// SPDX-License-Identifier: MIT
pragma solidity ^0.7.6;            // no built-in overflow checks

contract WrappingToken {
    mapping(address => uint256) public balanceOf;

    function transfer(address to, uint256 amount) external {
        // UNSAFE: if amount > balanceOf[msg.sender], this UNDERFLOWS.
        // balanceOf[msg.sender] becomes ~2**256, not a revert.
        balanceOf[msg.sender] -= amount;
        balanceOf[to] += amount;   // may also overflow 'to'
    }
}

synthetic — 0.8 with the checks deliberately removed
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;           // checked by default...

contract RewardVault {
    mapping(address => uint128) public shares;   // packed to uint128

    function accrue(address user, uint256 delta) external {
        // UNSAFE #1: narrowing cast truncates high bits with NO check.
        uint128 d = uint128(delta);

        // UNSAFE #2: unchecked disables the default overflow guard,
        // so a large d wraps shares[user] back toward zero.
        unchecked {
            shares[user] += d;
        }
    }
}

• ▸Fund theft / unbacked supply: an underflowed balance or an overflowed mint lets an attacker hold tokens that no deposit backs, then drain pools or peers that honour the figure.
• ▸Accounting corruption: a wrapped supply total, fee accumulator, or index breaks every downstream calculation that reads it, often silently.
• ▸Access-control bypass: when a wrapped value feeds a comparison (require(x <= limit) where x underflowed to a huge number, or a gate that expected a counter to stay small), the check passes or fails against a nonsensical value.
• ▸Denial of service (0.8 path): a Panic(0x11) revert on an unexpected overflow can brick a function permanently if the overflowing value is stuck in storage and every call re-hits it.

No single technique is sufficient; each answers a different question, and they produce evidence of different strengths.

Static analysis

Flags the structural precondition: pre-0.8 pragmas, unchecked blocks, narrowing casts, and assembly arithmetic on tainted values. Fast and broad, but a flag is a SIGNAL that an operation can wrap — not proof that it does with reachable inputs.

Dynamic / unit testing

Executes concrete inputs and observes a wrap or a Panic(0x11) revert. A failing test is strong local evidence for the tested path; a passing suite proves nothing about untested inputs.

Symbolic execution

Explores paths with symbolic inputs and asks a solver whether any assignment drives an operation out of range; a returned model is a concrete counterexample. Limited by path explosion and loop/solver timeouts, so absence of a model within budget is UNKNOWN, not safety.

Fuzzing

Property/invariant fuzzers (Echidna, Foundry invariant tests) hammer the contract with randomized sequences to break a stated invariant (e.g. sum of balances == totalSupply). A broken invariant is a reproducible counterexample; survival of the campaign is UNKNOWN.

Formal verification

Proves a bounded property holds for all inputs (e.g. via the SMTChecker or an external prover). A discharged proof is the strongest evidence, but only for exactly the property and assumptions stated — it does not generalise to un-modelled behaviour.

An autonomous investigator treats "this arithmetic can wrap" as a hypothesis to be tested, not a conclusion to be reported. A disciplined agent loop proceeds from observation to evidence rather than from pattern to verdict.

1. 1Observe: parse the source and bytecode for arithmetic on externally influenced values — pragma version, unchecked scopes, casts, assembly opcodes — and record each as a candidate site.
2. 2Hypothesise: for each site, state the concrete claim ("transfer underflows balanceOf[msg.sender] when amount > balance, yielding a near-maximal balance that withdraw then honours").
3. 3Experiment: generate inputs — by symbolic solving for a model, by fuzzing toward the type edge, or by hand — and execute them against the actual compiled contract in a sandbox.
4. 4Collect evidence: capture the post-state (the wrapped storage value, the Panic code, the resulting transfer) rather than the model’s narrative about it.
5. 5Decide: only promote to a finding when a real execution reproduced the wrap and a consequential effect; otherwise record UNKNOWN with the reason (unreached, solver timeout, guarded upstream).

RootRaven is evidence-first. For integer overflow and underflow it does not stop at flagging an unchecked block or a pre-0.8 pragma; it attempts to prove the wrap by executing a real attack against the contract on a disposable, local blockchain (or a local fork of real state), and it confirms the outcome with a deterministic, AI-free verifier. The language model’s only role is to compose candidate attacks; it never signs off on the result.

Observation

Static pass marks arithmetic sites on attacker-influenced values (version, unchecked, casts, assembly) as candidates — a SIGNAL, not a finding.

Hypothesis

A precise, testable claim about one site: the operation, the input that wraps it, and the state change it should produce.

Experiment

Deploy to a local chain or local fork, submit the candidate transaction(s), and record the resulting state and revert reason. No live-network attack mode exists.

Evidence

The observed post-state: the wrapped storage slot value, a Panic(0x11), or an unbacked transfer that actually executed.

Verification

A deterministic checker re-reads the post-state and confirms the invariant break (e.g. recovered amount > deposited amount) with no model in the loop.

Finding

Promoted only when a real execution reproduced the wrap AND a consequential effect, with the transcript attached. Everything else is UNKNOWN.

• ▸Use Solidity ≥0.8 and rely on the default checked arithmetic; treat removing a check as a decision requiring justification, not a default.
• ▸For pre-0.8 code that cannot be upgraded, apply a vetted SafeMath-style library to every +, −, * — not just the ones that "look risky".
• ▸Enter unchecked blocks only when the no-overflow precondition is proven from surrounding code (e.g. a loop index bounded by an array length), and document that proof at the call site.
• ▸Before any narrowing cast, bound the value explicitly (require(x <= type(uint128).max)) so truncation cannot silently discard significant bits.
• ▸Keep intermediate magnitudes small: order fixed-point math to avoid multiplying up to a value that overflows before the compensating division (mulDiv-style helpers), and prefer audited libraries for 10^18 scaling.
• ▸Audit inline assembly arithmetic by hand — the compiler adds no checks there — or avoid it where the gas saving does not justify the risk.

The corrected token relies on 0.8 checked arithmetic for the balance math (an over-transfer now reverts with Panic(0x11) instead of wrapping) and bounds the cast before packing so truncation is impossible. The reward path keeps unchecked only where a proven bound makes overflow impossible.

synthetic — checked math + bounded cast
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

contract SafeToken {
    mapping(address => uint256) public balanceOf;
    mapping(address => uint128) public shares;

    function transfer(address to, uint256 amount) external {
        // WHY: on 0.8 this subtraction reverts if amount > balance,
        // so an underflow is impossible — the attacker cannot mint a
        // near-maximal balance; the call simply fails.
        balanceOf[msg.sender] -= amount;
        balanceOf[to] += amount;
    }

    function accrue(address user, uint256 delta) external {
        // WHY: bound BEFORE narrowing so the cast cannot drop high bits.
        require(delta <= type(uint128).max, "delta too large");
        uint128 d = uint128(delta);

        // Checked add (NO unchecked): overflow of shares reverts instead
        // of wrapping toward zero.
        shares[user] += d;
    }
}

Verify by trying to reproduce the wrap against the fixed contract and confirming it can no longer occur within the tested scope. The tests below are conceptual Foundry/Echidna-style sketches; they illustrate the shape of a reproducible check, not a guarantee of immunity.

conceptual — Foundry-style regression (fuzz + expected revert)
// Confirms the over-transfer path now reverts instead of underflowing.
function testFuzz_overTransferReverts(uint256 amount) public {
    vm.assume(amount > token.balanceOf(address(this)));
    vm.expectRevert();                 // Panic(0x11) on checked underflow
    token.transfer(bob, amount);
}

// Invariant: no address can hold more than total deposits.
function invariant_noUnbackedBalance() public {
    assertLe(token.balanceOf(attacker), totalDeposited);
}

conceptual — Echidna-style property
// Echidna explores random call sequences trying to break this.
// A counterexample would be a reproduced bug; survival is UNKNOWN,
// not proof of safety.
function echidna_supply_equals_sum() public view returns (bool) {
    return sumOfBalances() == token.totalSupply();
}

• ▸Detection: a static flag on an unchecked block or cast is a SIGNAL; many such sites are provably safe (bounded loop indices), so flags without a reproduced wrap are not findings.
• ▸Reachability: an arithmetic site may be unreachable with valid inputs or guarded upstream; RootRaven reports these as UNKNOWN, not clean.
• ▸Logic-in-range errors: checked arithmetic and this detector do nothing for calculations that are wrong but never exceed the type — those belong to precision/rounding and logic-error classes.
• ▸Casts and assembly: narrowing casts and Yul arithmetic carry no default checks; coverage depends on the analyzer modelling them explicitly.
• ▸DoS trade-off: moving from wrap to revert can introduce a liveness bug; verifying the fix means checking both corruption and availability.
• ▸Maturity caveat: reproduction is strong for straightforward wraps but weaker where state setup is complex; a clean campaign is never reported as a guarantee.

Arithmetic wraps are frequently the primitive that other DeFi attacks weaponise: a precision-loss or rounding error is the in-range sibling where no wrap occurs but the result is still wrong, and share-inflation accounting exploits combine rounding with magnitude. Flash loans supply the capital to drive a value to the type edge in a single transaction, and oracle manipulation can feed a contract the extreme number that an unchecked multiply then overflows on.