Lending & Liquidation Logic Failures

Domain

Web3 & smart contracts

ROOTVIEL support

Partial — Core is built; parts are not yet wired end-to-end.

Analysis family

RootRaven

CWE

CWE-840, CWE-682, CWE-345

OWASP

SC03, SC02

A lending/liquidation logic failure is any defect in how a money market measures the health of a borrowing position or restores it when unhealthy. The protocol must, at all times, be able to assert that the value of a borrower’s collateral, discounted by a safety factor, exceeds their outstanding debt including accrued interest. When the accounting that produces that assertion is wrong — or when the mechanism meant to act on it is broken — the protocol can carry losses it believes do not exist.

The failure surfaces in three broad shapes: under-collateralization (a position is allowed to exist, or to persist, with debt exceeding discounted collateral value), mis-valuation (collateral or debt is priced wrongly, so a healthy-looking position is actually underwater or vice versa), and liquidation-mechanism faults (positions that cannot be liquidated at all, or that are liquidated far beyond what restoring health requires).

These failures live in the core of any over-collateralized lending or borrowing system and in the vaults, CDPs, and perpetuals that reuse the same health-factor pattern.

• ▸Collateralized debt positions / money markets: health = discounted collateral value / debt; the whole protocol rests on this ratio being right.
• ▸Interest accrual: per-second or per-block indexes that must grow the debt faithfully; a stale or mis-scaled index silently breaks the invariant.
• ▸Liquidation incentives: the bonus/penalty paid to liquidators, which must be enough to attract them but not so much it over-punishes borrowers.
• ▸Oracle-fed valuation: collateral priced from an external or on-chain source whose manipulation directly changes who is liquidatable.
• ▸Close-factor and partial-liquidation logic: how much of a position may be seized in one call, and whether repeated calls can seize too much.

Health is computed as discounted collateral value divided by debt, all in integer fixed-point. Three sub-systems feed it. Valuation converts collateral and debt amounts into a common unit using a price (the oracle leg — see oracle manipulation). Interest accrual grows debt over time using a compounding index, typically debt = principal * indexNow / indexAtBorrow, recomputed lazily whenever the market is touched. Liquidation reads health, and if it is below one, lets a liquidator repay some debt in exchange for seized collateral plus a bonus.

Every one of these is integer arithmetic subject to ordering and rounding (see precision loss), and every one depends on being called at the right time. A lazily-accrued index that is read before accrual under-states debt; a liquidation that rounds seized collateral up over-punishes the borrower; a health check that prices collateral from a spot source can be flipped by a flash-financed swap. The invariant is only as sound as the weakest of valuation, accrual, and seizure.

Health factor

Discounted collateral value ÷ debt (incl. accrued interest). Below 1 (or the protocol’s threshold) the position is liquidatable.

Collateral factor / LTV

The discount applied to collateral value; an 80% factor means $100 of collateral backs at most $80 of debt.

Liquidation bonus / penalty

The discount a liquidator receives on seized collateral, incentivising timely liquidation at the borrower’s expense.

Close factor

The maximum fraction of a position that may be liquidated in a single call; bounds over-liquidation.

Interest index

A monotonically growing accumulator used to scale principal into current debt; must be accrued before any health-dependent action.

The unifying root cause is a health invariant that is asserted from stale, mis-scaled, or manipulable inputs, or a liquidation path whose arithmetic does not actually restore that invariant. Concretely: pricing collateral from a manipulable source, reading debt before accruing interest, using a collateral factor that does not cover the asset’s real volatility, rounding seizure in the wrong direction, or a close-factor/ordering bug that lets a position be liquidated more than once past the point of health.

A second, structural root is incentive misalignment: if the liquidation bonus is too small relative to gas and price risk, no liquidator acts, and an underwater position becomes un-liquidatable bad debt even though the code "works"; if it is too large, liquidation becomes an extraction tool against borrowers. The code can be free of line bugs and still fail because the economic parameters make the mechanism inoperative or abusive.

One representative path: mis-valuation via a manipulable price lets an attacker borrow against collateral worth less than the loan, then walk away, leaving the protocol with bad debt. A second: stale accrual lets a position that is actually underwater escape liquidation.

1. 1Probe: the attacker identifies that collateral is valued from a manipulable source, or that debt is read before interest is accrued, so the health factor can be made to lie.
2. 2Distort: they move the price (often flash-financed) or exploit the accrual gap so their position reads as over-collateralized when it is not.
3. 3Extract: they borrow the maximum the inflated health allows, or avoid a liquidation that should have fired, taking value out of the protocol.
4. 4Reverse: they let the price revert (or the index catch up); the position is now plainly underwater, but the funds are already withdrawn.
5. 5Bad debt crystallises: the protocol is left with debt exceeding collateral; if liquidation incentives are too weak, no one repays it, and honest depositors absorb the shortfall.

A synthetic money market whose health check reads debt WITHOUT accruing interest first and prices collateral from a spot source. Both make the health factor over-state safety, so a position can borrow more than its collateral truly supports and escape liquidation.

synthetic — do not use; stale debt + manipulable valuation
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

interface ISpotOracle { function price(address token) external view returns (uint256); }

contract LooseMarket {
    ISpotOracle public oracle;
    uint256 public collateralFactor = 0.9e18;   // 90% LTV, very high

    mapping(address => uint256) public collateralAmt;  // units of collateral
    mapping(address => uint256) public principal;      // borrow principal
    uint256 public interestIndex = 1e18;               // grows over time
    mapping(address => uint256) public indexAtBorrow;

    address public collateralToken;

    // UNSAFE: uses the CURRENT stored index without accruing first,
    // so if accrual is lazy and hasn't run, debt is understated.
    function debtOf(address u) public view returns (uint256) {
        return principal[u] * interestIndex / indexAtBorrow[u];
    }

    // UNSAFE: collateral priced from a manipulable SPOT oracle,
    // and collateralFactor is aggressively high.
    function healthFactor(address u) public view returns (uint256) {
        uint256 collValue = collateralAmt[u] * oracle.price(collateralToken) / 1e18;
        uint256 discounted = collValue * collateralFactor / 1e18;
        uint256 d = debtOf(u);
        if (d == 0) return type(uint256).max;
        return discounted * 1e18 / d;            // >= 1e18 means "healthy"
    }

    // UNSAFE: no accrual before the check -> position can dodge liquidation.
    function liquidatable(address u) public view returns (bool) {
        return healthFactor(u) < 1e18;
    }
}

• ▸Protocol insolvency / bad debt: positions that cannot be liquidated, or that were under-collateralized from the start, leave debt the protocol cannot recover.
• ▸Depositor loss: the shortfall is ultimately borne by suppliers, who may be unable to withdraw in full.
• ▸Borrower harm (over-liquidation): wrong seizure math or an abusive bonus can take far more collateral than restoring health requires.
• ▸Cascading liquidations: a mis-valuation during volatility can trigger mass liquidations that further move the price, deepening losses.

Detection combines spotting the structural weaknesses (stale reads, spot-priced collateral, missing close factor) with executing scenarios that drive a position across the health threshold and checking the mechanism responds correctly.

Static analysis

Flags health checks that read debt before accrual, collateral priced from a spot source, missing/oversized close factors, and seizure rounding that favours the liquidator. SIGNALS of an unsound invariant, not proof of loss.

Dynamic (local-fork) testing

Set up a borrow, then drive price/time to the liquidation boundary and execute the liquidation; measure whether solvency is restored, whether seizure matches the formula, and whether bad debt remains. A reproduced over/under-liquidation is concrete evidence.

Symbolic execution

Can search for inputs where the health factor crosses 1 but liquidation reverts or restores the wrong amount; a model is a counterexample. The oracle/accrual composition often forces UNKNOWN on timeout.

Fuzzing

Invariant fuzzing asserts protocol-level solvency (total collateral value ≥ total debt, or "no account is both underwater and un-liquidatable") across random borrow/accrue/liquidate sequences; a break is reproducible.

Formal verification

Prove a liquidation monotonicity/solvency property — e.g. a successful liquidation never decreases global solvency — under a modelled oracle and accrual. Holds only within those assumptions.

An autonomous investigator models the full lifecycle — borrow, accrue, price-move, liquidate — and seeks a concrete sequence that leaves the protocol insolvent or a borrower over-seized, proven by execution.

1. 1Observe: map the valuation, accrual, and liquidation legs; flag stale reads, spot pricing, aggressive LTV, and close-factor gaps as candidates.
2. 2Hypothesise: state a lifecycle claim ("borrow at max LTV, let the manipulable price revert / skip accrual, and the position becomes underwater yet liquidatable only at a loss, leaving bad debt B").
3. 3Experiment: on a local fork, open the position, advance time and/or move the price, then attempt liquidation; record collateral seized, debt repaid, and residual bad debt.
4. 4Collect evidence: the measured solvency gap, the seizure-vs-formula discrepancy, and whether any liquidation path reverts — all from execution.
5. 5Decide: promote to a finding only when a real sequence produced insolvency, over-liquidation, or an un-liquidatable underwater position; otherwise UNKNOWN with the reason.

RootRaven proves a lending/liquidation finding only by executing the full borrow→accrue→move→liquidate lifecycle on a disposable LOCAL blockchain or a LOCAL fork of real state — never on a live network — and confirming the solvency outcome with a deterministic, AI-free verifier. The model composes the candidate lifecycle and parameters; the verifier measures whether solvency was actually broken, a borrower over-seized, or an underwater position left un-liquidatable.

Observation

Stale debt reads, spot-priced collateral, aggressive LTV, and close-factor gaps are marked as candidate invariant weaknesses — SIGNALS only.

Hypothesis

A quantified lifecycle claim: positions, time/price moves, and the expected residual bad debt or over-seizure.

Experiment

On a local fork/chain, open the borrow, advance time, move the (manipulable) price, and run liquidation; capture collateral, debt, and residuals at each step. No live-network attack mode.

Evidence

Measured solvency gap, seizure-vs-formula delta, and any revert in the liquidation path — raw numbers from execution.

Verification

A deterministic checker confirms global solvency fell, or seizure exceeded what health restoration required, or an underwater account could not be liquidated — no model judgement.

Finding

Promoted only on a reproduced insolvency / over-liquidation / un-liquidatable outcome; non-reproduced weaknesses stay UNKNOWN.

• ▸Accrue interest before every health-dependent read and action, so debt is never understated at the moment it matters.
• ▸Price collateral from manipulation-resistant sources (TWAP / aggregated oracles with deviation bounds), not a spot ratio an attacker can move.
• ▸Set collateral factors conservatively for the asset’s real volatility and liquidity; leave a buffer so a healthy position does not flip underwater on normal moves.
• ▸Bound liquidation with a close factor and round seizure in the protocol/borrower-protective direction, so a position cannot be repeatedly over-seized.
• ▸Calibrate the liquidation bonus so liquidators are reliably incentivised to act before bad debt forms, but not so much that liquidation becomes extractive.
• ▸Add a bad-debt backstop (reserves / insurance fund) and socialise-loss logic explicitly, rather than assuming liquidation always clears positions.
• ▸State and continuously test a global solvency invariant (total discounted collateral ≥ total debt) as a first-class property.

The corrected market accrues interest before reading debt, prices collateral from a TWAP oracle, uses a conservative LTV, and applies a close factor so no single liquidation can seize more than restoring health requires.

synthetic — accrue-first + TWAP + close factor
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

interface ITwapOracle { function consult(address token, uint256 amt) external view returns (uint256); }

contract TighterMarket {
    ITwapOracle public oracle;
    uint256 public collateralFactor = 0.75e18;   // conservative 75% LTV
    uint256 public closeFactor = 0.5e18;          // at most 50% liquidated per call
    uint256 public liquidationBonus = 1.08e18;    // 8% bonus

    mapping(address => uint256) public collateralAmt;
    mapping(address => uint256) public principal;
    uint256 public interestIndex = 1e18;
    uint256 public lastAccrual;
    address public collateralToken;

    // WHY: bring the index up to date BEFORE any health read.
    function accrue() public {
        uint256 dt = block.timestamp - lastAccrual;
        if (dt > 0) {
            interestIndex += interestIndex * ratePerSecond() * dt / 1e18;
            lastAccrual = block.timestamp;
        }
    }

    function ratePerSecond() internal pure returns (uint256) { return 3170979198; } // ~10%/yr, illustrative

    function debtOf(address u, uint256 idxAtBorrow) public view returns (uint256) {
        return principal[u] * interestIndex / idxAtBorrow;
    }

    // WHY: collateral priced from a TWAP (not a flash-manipulable spot),
    // conservative LTV, and accrual enforced by the caller first.
    function healthFactor(address u, uint256 idxAtBorrow) public view returns (uint256) {
        uint256 collValue = oracle.consult(collateralToken, collateralAmt[u]);
        uint256 discounted = collValue * collateralFactor / 1e18;
        uint256 d = debtOf(u, idxAtBorrow);
        if (d == 0) return type(uint256).max;
        return discounted * 1e18 / d;
    }

    // WHY: bound seizure by the close factor so a borrower cannot be
    // over-liquidated in a single call; accrue first so health is current.
    function liquidate(address u, uint256 repay, uint256 idxAtBorrow) external {
        accrue();
        require(healthFactor(u, idxAtBorrow) < 1e18, "healthy");
        uint256 maxRepay = debtOf(u, idxAtBorrow) * closeFactor / 1e18;
        require(repay <= maxRepay, "exceeds close factor");
        // ... seize repay * liquidationBonus worth of collateral (rounding
        //     toward the protocol), update principal, transfer. (omitted)
    }
}

Verify by driving positions across the liquidation boundary under adversarial price and time, and asserting that liquidation restores solvency, respects the close factor, and leaves no un-liquidatable underwater account. Conceptual Foundry/Echidna-style tests follow.

conceptual — Foundry: liquidation restores solvency, respects close factor
function test_liquidationBoundedAndSolvent() public {
    _open(borrower, collat, debt);
    _advanceTimeAndPriceToUnderwater();        // accrual + TWAP move
    market.accrue();
    assertLt(market.healthFactor(borrower, idx), 1e18);

    uint256 maxRepay = market.debtOf(borrower, idx) * market.closeFactor() / 1e18;
    vm.expectRevert();                          // over-close-factor must fail
    market.liquidate(borrower, maxRepay + 1, idx);

    market.liquidate(borrower, maxRepay, idx);  // allowed amount succeeds
    assertGe(_globalCollateralValue(), _globalDebt());  // solvency not worsened
}

conceptual — Echidna: no un-liquidatable underwater account
function echidna_no_unliquidatable_underwater() public view returns (bool) {
    address u = _probe();
    // if underwater, a liquidation at the close factor must be callable
    return market.healthFactor(u, _idx(u)) >= 1e18 || _liquidationWouldSucceed(u);
}

• ▸Composite surface: the failure can live in valuation, accrual, or seizure; a clean result for one leg says nothing about the others.
• ▸Economic dependence: incentive adequacy (the liquidation bonus) is a parameter question execution can probe but not prove correct for all markets.
• ▸Oracle reliance: valuation safety inherits the oracle’s safety; a manipulable price undermines every downstream guarantee.
• ▸Fork-scoped: reproduced insolvency is scoped to the forked state, block, and parameters; other conditions may differ.
• ▸Volatility outruns mechanism: no fix guarantees solvency against an arbitrarily fast price move; it only narrows the window.
• ▸Maturity caveat: "partial" — RootRaven reproduces some lifecycle exploits but reports non-reproduced weaknesses as UNKNOWN, never safe.

Liquidation failures sit at the confluence of several classes: oracle manipulation is the most direct way to mis-value collateral and force or dodge a liquidation; flash-loan-assisted attacks supply the capital to move that price within a transaction; precision loss and rounding decide who absorbs dust in seizure math; and MEV/back-running shapes who captures liquidation profit. Accounting and share-inflation attacks share the same valuation-and-rounding surface in vault contexts.