Semantic Reentrancy

Overview

The semantic reentrancy detector identifies reentrancy vulnerabilities that exploit logical state inconsistencies rather than simple balance-draining patterns. In semantic reentrancy, the contract’s state is internally consistent from a bookkeeping perspective but semantically incorrect during the external call window. For example, a lending protocol may correctly track a user’s collateral and debt balances, but the ratio between them is temporarily invalid — allowing the user to borrow more than their collateral supports during the callback.

Why This Is an Issue

Standard reentrancy detectors focus on the classic pattern: external call before state update. Semantic reentrancy is subtler — the state variables may all be updated before the external call, but the relationship between them (invariants like collateral ratio, total supply consistency, or price oracle freshness) is temporarily violated. During the callback window, other functions that rely on these invariants produce incorrect results.

How to Resolve

// Before: Vulnerable — individual state updates correct, but invariant broken
function borrow(uint256 amount) external {
    userDebt[msg.sender] += amount;  // State updated
    // Collateral ratio is invalid here — debt increased but position not checked
    token.transfer(msg.sender, amount);  // External call during invalid state
    require(isHealthy(msg.sender), "Undercollateralized");
}

// After: Fixed — reentrancy guard protects invariant window
function borrow(uint256 amount) external nonReentrant {
    userDebt[msg.sender] += amount;
    token.transfer(msg.sender, amount);
    require(isHealthy(msg.sender), "Undercollateralized");
}

Detection Methodology

1. Multi-variable state tracking: Tracks all state variables modified within a function and identifies which invariants (ratios, sums, orderings) they participate in.
2. Invariant window detection: Identifies code regions where some but not all invariant-related variables have been updated — the “inconsistency window.”
3. External call in window: Flags external calls that occur during an invariant inconsistency window.
4. Cross-function analysis: Checks whether other public functions read the temporarily-inconsistent state, enabling exploitation via reentrant call.

Limitations

False positives: Functions with reentrancy guards that cover the entire invariant window are safe but may be flagged if the guard is in a modifier the detector does not trace. False negatives: Invariants that span multiple contracts (e.g., cross-contract collateral ratios) are beyond single-contract analysis.

Related Detectors

• Reentrancy — detects classic balance-draining reentrancy
• Cross-Function Reentrancy — detects reentrancy across function boundaries
• Read-Only Reentrancy — detects reentrancy via view functions

References

• SWC-107: Reentrancy
• OpenZeppelin ReentrancyGuard