Requirement Violation
Detects functions where require/assert conditions can be violated through specific input combinations or state manipulation.
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)whenx == 0should 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 auint256is 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": "high",
"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
REVERTpaths in the CFG to reconstructrequireconditions. - 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
requiremay not be fully parsed.
Related Detectors
- Tautological Compare — comparisons that are always true or false
- Input Validation — missing input validation on function parameters
- Precision Errors — rounding errors in arithmetic conditions