Sigvex
EVMRemediation2 min read

Semantic Reentrancy Remediation

How to defend against reentrancy that exploits a temporarily invalid invariant rather than a stale balance.

evmreentrancy

Semantic Reentrancy Remediation

Overview

Related Detector: Semantic Reentrancy

Semantic reentrancy exploits a state that is internally consistent but semantically invalid during an external call. A lending protocol may track collateral and debt correctly, yet the ratio between them is momentarily wrong mid-operation — letting a re-entrant call borrow against collateral that is about to be removed. Simple checks-effects-interactions on a single variable is not enough; the fix is to hold every invariant valid across the call, or to lock re-entry entirely.

Before (Vulnerable)

function withdrawCollateral(uint256 amount) external {
    collateral[msg.sender] -= amount;
    // Invariant "collateral >= debt-backed value" is temporarily false here.
    _sendCollateral(msg.sender, amount);          // external call — re-entry possible
    require(_healthy(msg.sender), "Undercollateralized");   // checked too late
}

After (Fixed — validate the invariant before the call, and lock re-entry)

modifier nonReentrant() { /* standard guard */ _; }

function withdrawCollateral(uint256 amount) external nonReentrant {
    collateral[msg.sender] -= amount;
    require(_healthy(msg.sender), "Undercollateralized");   // invariant enforced BEFORE the call
    _sendCollateral(msg.sender, amount);                    // now safe to interact
}

Enforce cross-variable invariants (health factor, collateral ratio, total-supply equalities) before any external call, and add a reentrancy guard so no callback can observe a half-applied operation.

Common Mistakes

  • Applying CEI to one balance while a multi-variable invariant is still violated across the external call.
  • Checking the health factor after the interaction, when a re-entrant call already acted on the invalid state.
  • Trusting a reentrancy guard alone without also ordering the invariant check before the call.

References