EVM Threat Models

0x07-SMOD

18 min read

Opcode Summary

PropertyValue
Opcode0x07
MnemonicSMOD
Gas5
Stack Inputa, b
Stack Outputa % b (signed, two’s complement)
BehaviorSigned 256-bit modulus. The result has the same sign as the dividend a, not the divisor. If b == 0, returns 0 silently. The relationship a == (a / b) * b + (a % b) holds when paired with SDIV (truncation toward zero).

Threat Surface

SMOD is the signed counterpart of MOD (0x06) and the remainder companion to SDIV (0x05). Its threat surface is more subtle than either, because SMOD’s dangers rarely produce dramatic exploits in isolation — instead they inject systematic numeric bias that accumulates into exploitable discrepancies over time.

The central issue is the sign convention of the remainder. In the EVM, SMOD returns a result whose sign matches the dividend (first operand), not the divisor. This means -7 % 5 = -2 and 7 % -5 = 2. This convention matches C, C++, Java, Rust, and Solidity, but differs from Python (-7 % 5 = 3), Ruby, and mathematical modular arithmetic (where the result is always non-negative or matches the divisor’s sign). Developers porting algorithms from these languages will silently get wrong results.

Beyond sign confusion, SMOD introduces three additional threat vectors:

  • Silent mod-by-zero: Like MOD and DIV, a % 0 returns 0 with no exception. In signed contexts, 0 is a perfectly valid and meaningful remainder, making it impossible to distinguish “remainder is zero” from “divisor was zero” without an explicit check.
  • Signed/unsigned confusion: The EVM stack is untyped. SMOD and MOD interpret the same 256-bit word completely differently. A value like 0xFFFF...FFFF is 2^256 - 1 to MOD but -1 to SMOD. Using the wrong opcode in inline assembly produces silently incorrect results.
  • Interaction with SDIV overflow: The identity a == (a / b) * b + (a % b) means SMOD is mathematically tied to SDIV. When a == int256.min and b == -1, SDIV overflows (returning int256.min instead of +2^255), but SMOD correctly returns 0. However, any contract that computes both the quotient and remainder for this input pair will have a correct remainder paired with an incorrect quotient — a subtle inconsistency that can corrupt reconstruction logic.

Smart Contract Threats

T1: Sign Convention Confusion (High)

The EVM’s SMOD follows the truncation-toward-zero (T-division) convention: the remainder’s sign matches the dividend. This differs from other common conventions:

ExpressionEVM SMOD (T-division)Python % (F-division)Mathematical mod
-7 % 5-233
7 % -52-32
-7 % -5-2-2-2 (or 3)

Developers porting algorithms from Python, Ruby, or mathematical specifications will silently get wrong results when negative values are involved. This is especially dangerous for:

  • Cyclic index calculations: array[index % length] where index can be negative. SMOD produces a negative index, causing an out-of-bounds access or array underflow, while the developer expected wrapping to a valid positive index.
  • Time bucketing: timestamp % interval for reward distribution epochs. If timestamp is represented as a signed delta from some reference, negative timestamps produce negative bucket indices.
  • Hash-to-range mapping: Reducing a signed hash value to a range [0, N) via SMOD yields negative results for negative hashes, breaking uniform distribution assumptions.

T2: Signed/Unsigned Modulus Confusion (High)

The EVM stack has no type system. SMOD interprets operands as two’s complement signed integers, while MOD treats them as unsigned. The same 256-bit value produces completely different results:

Value (hex)MOD interpretationSMOD interpretation
0xFFFF...FFFF2^256 - 1 (max uint)-1
0x8000...00002^255-2^255 (int256.min)

Using the wrong opcode — especially in inline assembly or Yul — produces silently incorrect results:

assembly {
    // BUG: Using smod for unsigned values
    // If a = 0xFFFF...FFFE (uint256.max - 1) and b = 3:
    //   MOD:  (2^256 - 2) % 3 = 0
    //   SMOD: (-2) % 3 = -2 (0xFFFF...FFFE as signed)
    let result := smod(a, b)
}

This confusion is amplified by Solidity’s Yul IR code generation pipeline, where type information can be lost during optimization passes. A uint256 variable compiled through the Yul pipeline could theoretically end up in an smod instruction if the optimizer’s type tracking is incorrect.

T3: Silent Mod-by-Zero (Medium)

SMOD returns 0 when the divisor is zero, with no exception or revert. In signed arithmetic contexts, 0 is a valid remainder (e.g., 6 % 3 = 0), making it impossible to distinguish a legitimate zero remainder from a division-by-zero error without an explicit pre-check.

int256 bucket = value % int256(numBuckets);
// If numBuckets == 0: bucket = 0, silently
// Contract assigns everything to bucket 0 instead of reverting

This is identical to MOD’s and DIV’s behavior, but the signed context makes it more dangerous because contracts often use signed modulus in financial calculations where a zero result has a specific meaning (e.g., “position is perfectly hedged” or “no remainder to distribute”).

T4: Negative Remainder in Financial Math (High)

DeFi protocols using signed arithmetic for PnL calculations, funding rates, or fee distribution must handle negative remainders correctly. SMOD’s sign-follows-dividend behavior creates systematic bias:

  • Fee distribution: When distributing totalFees among N participants, totalFees % N gives the undistributed remainder. If totalFees is negative (a refund), SMOD produces a negative remainder, which may be incorrectly added rather than subtracted, creating or destroying value.
  • Periodic settlement: accruedFunding % settlementPeriod where accruedFunding can be negative produces a negative result. A contract expecting a positive “residual” will mishandle the negative case.
  • Rounding bias accumulation: The relationship a == (a / b) * b + (a % b) means SDIV’s truncation-toward-zero combines with SMOD’s signed remainder to create asymmetric rounding. For positive a, the remainder is always non-negative. For negative a, the remainder is always non-positive. Over many iterations (e.g., per-block funding rate calculations across thousands of blocks), this bias accumulates into an exploitable imbalance between long and short positions.

T5: The int256.min % -1 Edge Case (Medium)

When a == int256.min (-2^255) and b == -1, SMOD correctly returns 0 (since -2^255 is exactly divisible by -1). However, this edge case is dangerous in context:

  • The companion SDIV operation for the same inputs (int256.min / -1) overflows, returning int256.min instead of +2^255.
  • Any contract that computes both quotient and remainder (e.g., for Euclidean division reconstruction) gets q = int256.min, r = 0, and reconstructs q * b + r = int256.min * (-1) + 0 = int256.min — which is “correct” only because the quotient itself is wrong. Code that validates a == q * b + r will pass, masking the SDIV overflow.
  • Solidity 0.8.0+ reverts on int256.min / -1 but does not revert on int256.min % -1 (since the SMOD result itself is correct). Code paths that compute only the remainder bypass the SDIV overflow protection while still operating on the same dangerous input pair.

Protocol-Level Threats

P1: EVM Client Implementation Divergence (Medium)

SMOD’s signed arithmetic logic is a known source of implementation bugs in EVM clients. The opcode requires correct handling of two’s complement sign extraction, signed-aware modulus computation, and sign application to the result:

  • Revm (2024): PR #1248 fixed the i256_mod function’s handling of divisor-is-zero. The div-by-zero check was originally in the smod opcode handler rather than the underlying i256_mod function, creating an inconsistency with i256_div’s handling. The fix also removed misleading “overflow check” comments from the modulo code path.
  • LambdaClass Ethrex (2024): The negate() overflow bug discovered by FuzzingLabs in the SDIV handler also affected SMOD, since both opcodes share signed arithmetic helpers for converting between signed and unsigned representations before performing the operation.
  • Solidity Formal Verification (2020): Issue #9802 revealed that the SMOD implementation in Solidity’s formal verification test suite (test/formal/opcodes.py) incorrectly used SMT’s smod function instead of the EVM’s SMOD semantics. The SMT convention returns a result matching the divisor’s sign, while EVM SMOD matches the dividend’s sign. This meant formal proofs of SMOD-using code were verified against wrong semantics.

Any client that returns a remainder with the wrong sign, mishandles the int256.min % -1 case, or panics on edge inputs would diverge from the canonical chain.

P2: Compiler-Level Sign Handling (Low)

Different Solidity compiler versions handle signed modulus edge cases differently:

  • Pre-0.8.0: No overflow checks. SMOD is emitted directly. The companion SDIV overflow (int256.min / -1) is also unchecked.
  • 0.8.0+: The compiler inserts overflow checks for SDIV but not for SMOD itself (since SMOD cannot overflow). However, the int256.min % -1 case may or may not trigger the SDIV overflow check depending on whether the compiler also generates a division for the same expression.
  • Signed Immutables Bug (0.6.5–0.8.8): Signed immutable values shorter than 256 bits lacked proper sign extension when read via inline assembly. A int8(-2) immutable read as +254 would produce wrong SMOD results: 254 % 3 = 2 instead of (-2) % 3 = -2.

P3: No DoS Vector (Low)

SMOD costs a fixed 5 gas regardless of operand values. It operates purely on the stack with no memory, storage, or external access. It cannot be used for gas griefing or computational DoS.

Edge Cases

Edge CaseInputResultSecurity Implication
int256.min % -1-2^255 % -10Correct, but companion SDIV overflows. Masks SDIV bug in reconstruction checks.
Negative % Positive-7 % 5-2Sign follows dividend. Differs from Python (3). Breaks ported algorithms.
Positive % Negative7 % -52Sign follows dividend (positive). Divisor sign ignored for result sign.
Negative % Negative-7 % -5-2Both negative; result negative (matches dividend).
a % 0any % 00Silent failure. Indistinguishable from a legitimate zero remainder.
0 % b0 % any0Correct, but EVM implementations must not apply sign to the zero result. (Ethrex negate(0) bug.)
int256.min % 1-2^255 % 10Correct. No overflow.
int256.min % int256.min-2^255 % -2^2550Correct. Self-modulus is always 0.
-1 % int256.min-1 % -2^255-1Correct. -1 / -2^255 truncates to 0, remainder is -1.
int256.min % 2-2^255 % 20Correct. -2^255 is even.
Large negative % small positive-2^255 % 3-2 or -1 (depends on exact value)Sign is negative; developers expecting positive index get negative.

Real-World Exploits

Exploit 1: Solidity Formal Verification — Wrong SMOD Semantics (2020)

Root cause: The SMOD implementation in Solidity’s formal verification test suite used SMT’s smod function, which has different sign semantics than the EVM’s SMOD opcode.

Details: GitHub issue #9802 reported that test/formal/opcodes.py in the Solidity repository implemented SMOD using the Z3 SMT solver’s built-in smod function. The SMT convention defines smod such that the result’s sign follows the divisor, while the EVM’s SMOD returns a result matching the dividend’s sign. For example:

  • EVM SMOD: -7 % 5 = -2 (sign of dividend -7)
  • SMT smod: -7 % 5 = 3 (sign of divisor 5)

This meant all formal proofs of Solidity code involving signed modulus were verifying against incorrect behavior. A contract proven “safe” by the formal verification toolchain could still produce unexpected negative remainders at runtime.

Impact: The severity was rated low because the bug was confined to the test infrastructure, not the compiler itself. However, it undermined the trustworthiness of formal verification for any contract using signed modulus — a tool that auditors and high-value DeFi protocols rely on for security guarantees.

References:

Exploit 2: LambdaClass Ethrex EVM — Signed Arithmetic Crash Affecting SMOD (2024)

Root cause: Arithmetic overflow in the negate() helper function shared by SDIV and SMOD code paths in the Ethrex EVM implementation.

Details: FuzzingLabs discovered that LambdaClass’s Ethrex EVM used a negate() function (!value + U256::one()) that panicked on specific inputs. While the primary trigger was through SDIV, the SMOD code path used the same negate() function for converting between signed and unsigned representations before computing the modulus. An input where the remainder was zero but the dividend was negative would invoke negate(0), computing !0 + 1 = U256::MAX + 1, causing a panic.

The initial fix using saturating_add introduced a second bug: negate(0) returned U256::MAX instead of 0, producing a non-zero remainder when the correct result was zero.

Impact: Denial of service against Ethrex nodes. A crafted transaction with SMOD inputs costing only 5 gas could crash the node. On a network using Ethrex as a consensus client, this would cause a chain split.

SMOD’s role: The shared negate() helper meant SMOD inherited the same crash vulnerability as SDIV. The zero-remainder edge case (a % b == 0 where a < 0) was the specific SMOD trigger.

References:

Exploit 3: Revm — Inconsistent Div-by-Zero Handling in i256_mod (2024)

Root cause: The division-by-zero check for SMOD was in the opcode handler rather than the underlying i256_mod function, creating an inconsistency with how i256_div handled the same case.

Details: In revm (the Rust EVM implementation used by reth), the smod opcode handler checked for a zero divisor before calling i256_mod, while the analogous sdiv handler delegated the zero check to i256_div itself. PR #1248 standardized the behavior by moving the check into i256_mod, ensuring that i256_mod(a, 0) == 0 regardless of call site. The PR also removed misleading comments about “overflow checks” in the modulo code, which described behavior that belonged to SDIV, not SMOD.

Impact: While not directly exploitable (the zero-check existed, just in the wrong layer), this architectural inconsistency risked introducing bugs during refactoring. If a new call site invoked i256_mod directly without the zero check, it would produce undefined behavior. Revm is used in reth, one of the major Ethereum execution clients.

References:

Exploit 4: Vyper — Signed/Unsigned Comparison Bug in Range Loops (2024)

CVE: CVE-2024-32481

Root cause: The Vyper compiler (versions 0.3.8 through 0.4.0b1) used unsigned comparison instructions (LE) instead of signed comparison instructions (SLE) when evaluating range loop bounds involving signed integers.

Details: When a Vyper contract used range(start, start + N) with a signed integer start, the compiler generated code that compared the loop variable against the bounds using unsigned less-than-or-equal (LE) instead of signed less-than-or-equal (SLE). A negative start value, whose two’s complement representation has the MSB set, appears as an extremely large unsigned integer. The unsigned comparison would always fail, causing the loop body to never execute or the transaction to revert unexpectedly.

While this vulnerability involves SLT/SGT comparison opcodes rather than SMOD directly, it illustrates the broader class of signed/unsigned confusion that SMOD is susceptible to: the same 256-bit value is interpreted completely differently by signed vs. unsigned opcodes, and choosing the wrong variant produces silently incorrect behavior.

Impact: CVSS 5.3 (Medium). Contracts compiled with affected Vyper versions that used signed integers in range loops would fail to execute the loop body when the start value was negative, potentially skipping critical state updates or distributions.

References:

Attack Scenarios

Scenario A: Negative Index from Signed Modulus

contract VulnerableRoundRobin {
    address[] public validators;
 
    function getValidator(int256 slot) external view returns (address) {
        // BUG: If slot is negative, SMOD returns negative remainder
        // e.g., slot = -7, validators.length = 5:
        //   -7 % 5 = -2 (EVM SMOD)
        //   Cast to uint256: 0xFFFF...FFFE (enormous index)
        //   Array access reverts or reads garbage
        int256 index = slot % int256(uint256(validators.length));
        return validators[uint256(index)];
    }
}

Attack: Any negative slot value produces a negative remainder, which wraps to an enormous uint256 index when cast, causing a revert or (in unchecked contexts) reading from an unintended storage slot.

Scenario B: Fee Distribution Rounding Exploit

contract VulnerableFeeDistributor {
    int256 constant PRECISION = 1e18;
 
    function distributeFunding(int256 totalFunding, int256 numPositions)
        external
        pure
        returns (int256 perPosition, int256 residual)
    {
        // SDIV truncates toward zero; SMOD gives signed remainder
        perPosition = totalFunding / numPositions;
        residual = totalFunding % numPositions;
        // When totalFunding = -1000, numPositions = 3:
        //   perPosition = -333 (truncated toward zero, not -334)
        //   residual = -1
        //   Reconstruction: -333 * 3 + (-1) = -1000 ✓
        // But the protocol expects positive residual for redistribution
        // residual is negative, so adding it to a pool SUBTRACTS value
    }
}

Attack: An attacker manipulates positions to ensure totalFunding is negative. The negative residual is added to a redistribution pool as if positive, draining 1 wei per settlement period. Over thousands of blocks, this accumulates.

Scenario C: Mod-by-Zero Bypass in Access Control

contract VulnerableTimeLock {
    mapping(address => int256) public lastAction;
 
    function canAct(address user, int256 cooldownPeriod) external view returns (bool) {
        int256 elapsed = int256(block.timestamp) - lastAction[user];
        // BUG: If cooldownPeriod == 0 (uninitialized or attacker-controlled):
        //   elapsed % 0 = 0
        //   0 == 0 is true, so the check passes
        return (elapsed % cooldownPeriod) == 0;
    }
}

Attack: If cooldownPeriod is zero (e.g., for an unconfigured action type), SMOD returns 0, and the equality check passes, bypassing the time-lock entirely.

Scenario D: Signed/Unsigned Confusion in Assembly

contract VulnerableHashBucket {
    function getBucket(bytes32 hash, uint256 numBuckets) external pure returns (uint256) {
        uint256 bucket;
        assembly {
            // BUG: smod treats hash as signed
            // A hash with MSB set (50% of hashes) is interpreted as negative
            // Negative % positive = negative in SMOD
            // Result wraps to huge uint256 when returned
            bucket := smod(hash, numBuckets)
        }
        return bucket;
    }
}

Attack: Half of all hash values (those with the MSB set) produce negative SMOD results, wrapping to enormous uint256 values. The function returns indices far outside the expected [0, numBuckets) range, breaking any bucketing or routing logic downstream.

Mitigations

ThreatMitigationImplementation
T1: Sign convention confusionConvert SMOD result to non-negative when a positive remainder is neededint256 r = a % b; if (r < 0) r += (b > 0 ? b : -b); for Euclidean modulus
T1: Ported algorithmsUse explicit Euclidean mod functionImplement modE(a, b) that always returns [0, abs(b))
T2: Signed/unsigned confusionNever use smod for unsigned values in assemblyUse mod for uint256, smod only for int256; audit all Yul/assembly
T2: Type system bypassAvoid raw assembly for signed arithmeticLet Solidity’s type system enforce correct opcode selection
T3: Mod-by-zeroAlways validate divisor before modulusrequire(divisor != 0, "mod by zero")
T4: Negative remainder in financeUse absolute-value-then-sign patternCompute abs(a) % abs(b), then apply correct sign per protocol spec
T4: Rounding biasChoose and document rounding conventionImplement modFloor(a, b) / modEuclidean(a, b) wrappers
T5: int256.min % -1 interactionGuard both SDIV and SMOD inputs togetherrequire(!(b == -1 && a == type(int256).min)) before any signed division/modulus pair
General: Assembly auditsFlag all smod usage in security reviewsStatic analysis: Slither custom detectors, Mythril signed arithmetic checks
General: Compiler versionUse Solidity >= 0.8.9Fixes signed immutables bug; includes SDIV overflow checks

Compiler/EIP-Based Protections

  • Solidity 0.8.0+ (2020): Automatic revert on int256.min / -1 via SDIV overflow check. SMOD itself does not overflow, but the compiler’s protection on SDIV prevents the most dangerous companion operation.
  • Solidity 0.8.9+ (2021): Fixes the Signed Immutables Bug, ensuring signed values shorter than 256 bits are properly sign-extended when read, preventing corrupted SMOD inputs.
  • EIP-6888 (Proposed): Would add arithmetic verification flags to the EVM state, including a signed overflow flag (sovf) set when b == 0 ∨ (a == INT_MIN ∧ b == -1) for SMOD/SDIV. This would allow contracts to branch on division-by-zero without compiler-inserted checks.
  • SafeInt256 libraries: Notional Finance’s SafeInt256 and OpenZeppelin’s SignedMath provide safe wrappers that explicitly check edge cases before performing signed arithmetic.
  • Static analysis tools: Slither can detect signed/unsigned type confusion and missing zero-divisor checks. Mythril and Certora can formally verify that SMOD is never called with a zero divisor.

Euclidean Mod at EVM Level

When a protocol requires non-negative remainders (Euclidean modulus), the standard conversion from SMOD:

// Euclidean mod: result always in [0, |b|)
// Given: r = SMOD(a, b)
// If r < 0: result = r + |b|
// Else: result = r

PUSH a
PUSH b
SMOD          // r = a smod b  (sign of a)
DUP1          // r, r
PUSH 0
SLT           // r < 0?  (signed comparison)
ISZERO
jumpi @done   // If r >= 0, we're done
DUP1          // r, r
PUSH b
DUP1          // b, b, r, r
PUSH 0
SLT           // b < 0?
jumpi @neg_b
ADD           // r + b  (b is positive)
jump @done
@neg_b:
SUB           // r - b  (b is negative, so r - b = r + |b|)
@done:

Severity Summary

Threat IDCategorySeverityLikelihoodReal-World Precedent
T1Smart ContractHighMedium (any ported algorithm with negative inputs)Solidity formal verification wrong semantics (#9802)
T2Smart ContractHighMedium (assembly-heavy DeFi code)Vyper CVE-2024-32481 (signed/unsigned confusion)
T3Smart ContractMediumMedium (same as MOD/DIV division-by-zero)—
T4Smart ContractHighMedium (any protocol using signed math for finance)Funding rate rounding in perpetuals protocols
T5Smart ContractMediumLow (requires specific int256.min input with companion SDIV)Notional SafeInt256 guard pattern
P1ProtocolMediumLow (rare but catastrophic: consensus split)LambdaClass Ethrex crash; revm i256_mod fix
P2ProtocolLowLowSolidity Signed Immutables Bug (0.6.5–0.8.8)
P3ProtocolLowN/A—
OpcodeRelationship
MOD (0x06)Unsigned counterpart. Same division-by-zero behavior (returns 0), but no sign ambiguity since both operands and result are unsigned. Using MOD on signed values or SMOD on unsigned values produces wrong results.
SDIV (0x05)Signed division, the quotient companion to SMOD. The identity a == (a / b) * b + (a % b) ties them together. SDIV’s int256.min / -1 overflow produces a wrong quotient that SMOD’s correct 0 remainder cannot compensate for.
SLT (0x12)Signed less-than comparison. Essential for checking the sign of SMOD results and converting negative remainders to positive (Euclidean mod). Using unsigned LT on SMOD results causes the Vyper-class bug.
SGT (0x13)Signed greater-than comparison. Paired with SLT for range-checking SMOD results in signed arithmetic guard patterns.
SIGNEXTEND (0x0B)Sign-extends smaller signed integers to 256 bits. Critical for correct SMOD behavior when operating on values narrower than int256. The Signed Immutables Bug was a failure of sign extension that corrupted SMOD inputs.
SAR (0x1D)Arithmetic shift right. Sometimes combined with SMOD in optimized signed division/remainder patterns. SAR preserves the sign bit, unlike SHR.

Graph View

Latest updates

Backlinks