Requirement Violation

Overview

Remediation Guide: How to Fix Requirement Violations

The requirement violation detector identifies require() and assert() statements that can be bypassed or violated through specific input sequences, state manipulation, or edge-case arithmetic. While require is intended to validate preconditions, flawed conditions or missing edge cases allow attackers to pass checks that should fail.

Why This Is an Issue

Requirements are the primary defense mechanism in Solidity. A violated requirement means an invariant the developer assumed would hold can be broken. Common causes:

Off-by-one in comparisons: require(x > 0) when x == 0 should pass (or vice versa).
Integer overflow in check expressions: The require condition itself overflows before the comparison.
State-dependent checks: Requirement depends on mutable state that an attacker can manipulate in the same transaction.
Tautological checks: require(x >= 0) on a uint256 is always true.

Failed invariants have led to catastrophic exploits. The bZx attack ($8M, 2020) bypassed a collateralization check through a specific combination of flash-loaned funds and price manipulation.

How to Resolve

// Before: Require condition is bypassable via overflow (pre-0.8.0)
function withdraw(uint256 amount) external {
    require(balances[msg.sender] - amount >= 0); // Always true for uint256!
    balances[msg.sender] -= amount;
    payable(msg.sender).transfer(amount);
}

// After: Proper comparison without arithmetic in the condition
function withdraw(uint256 amount) external {
    require(balances[msg.sender] >= amount, "Insufficient balance");
    balances[msg.sender] -= amount;
    payable(msg.sender).transfer(amount);
}

Examples

Vulnerable Code

contract VulnerableLending {
    function borrow(uint256 amount) external {
        uint256 collateralValue = getCollateralValue(msg.sender);
        uint256 debtValue = getDebtValue(msg.sender) + amount;
        // Vulnerable: collateral ratio can be manipulated via oracle in same tx
        require(collateralValue * 100 / debtValue >= 150, "Undercollateralized");
        _issueLoan(msg.sender, amount);
    }
}

Fixed Code

contract SafeLending {
    function borrow(uint256 amount) external {
        uint256 collateralValue = getCollateralValue(msg.sender);
        uint256 debtValue = getDebtValue(msg.sender) + amount;
        // Fixed: use TWAP oracle and check for manipulation
        require(debtValue > 0, "Zero debt");
        require(collateralValue * 100 >= debtValue * 150, "Undercollateralized");
        require(!_isPriceManipulated(), "Price anomaly detected");
        _issueLoan(msg.sender, amount);
    }
}

Sample Sigvex Output

{
  "detector_id": "requirement-violation",
  "severity": "medium",
  "confidence": 0.70,
  "description": "Require condition at offset 0x15c in borrow() depends on getCollateralValue() which reads manipulable oracle state. An attacker can inflate collateral value via flash loan to bypass the 150% collateralization check.",
  "location": { "function": "borrow(uint256)", "offset": 348 }
}

Detection Methodology

Condition extraction: Parses REVERT paths in the CFG to reconstruct require conditions.
Symbolic evaluation: Checks whether condition expressions contain tautologies, contradictions, or overflow-prone arithmetic.
State dependency tracking: Traces whether condition inputs depend on mutable storage that can be influenced in the same transaction.
Edge-case analysis: Tests boundary values (0, 1, max) against the condition using symbolic constraints.

Limitations

Deep symbolic analysis is bounded; complex multi-step state manipulation paths may not be explored.
Conditions depending on off-chain oracle values cannot be fully evaluated statically.
Custom error types (Solidity 0.8.4+) used instead of require may not be fully parsed.

Tautological Compare – comparisons that are always true or false
Input Validation – missing input validation on function parameters
Precision Errors – rounding errors in arithmetic conditions