Aave V4: Why Bad Debt Can Never Be Repaid

1. Background: WadRayMath

Aave uses a precision library called WadRayMath for handling decimal math in Solidity. Understanding this library is essential to understanding the bug.

Key Conversion Functions

// WadRayMath.sol

// WAD to RAY: multiply by 1e9
function toRay(uint256 a) returns (uint256) {
    return a * 1e9;  // 1e18 * 1e9 = 1e27
}

// RAY to WAD: divide by 1e9 (rounds up)
function fromRayUp(uint256 a) returns (uint256) {
    return (a + 1e9 - 1) / 1e9;
}

The critical insight: toRay() is designed for converting WAD (1e18) to RAY (1e27). It multiplies by 1e9.

2. The Vulnerability

When a position becomes underwater and gets liquidated, any remaining debt becomes "bad debt" (deficit). This deficit is tracked in deficitRay using RAY precision.

How Deficit Is Recorded

// When bad debt occurs (simplified)
uint256 drawnShares = position.debt;    // e.g., 1e6 (1 USDC worth of shares)
uint256 drawnIndex = reserve.index;     // e.g., 1e27 (RAY precision)

// Deficit stored as: shares * index = assets in RAY
deficitRay = drawnShares * drawnIndex;  // 1e6 * 1e27 = 1e33

The Broken Repayment Logic (Line 433)

// Hub.sol - eliminateDeficit()
function eliminateDeficit(address asset, uint256 amount) external {
    uint256 deficitRay = reserve.deficitRay;

    // THE BUG: toRay() multiplies by 1e9, but deficit is assets * 1e27
    uint256 deficitAmountRay = (amount < deficitRay.fromRayUp())
        ? amount.toRay()   // WRONG! Scales by 1e9 instead of 1e27
        : deficitRay;

    // This subtraction barely makes a dent
    reserve.deficitRay = deficitRay - deficitAmountRay;
}

3. The Math That Breaks Everything

How Much Would Actually Be Needed?

4. Impact: Permanent Insolvency

5. Proof of Concept

// Foundry test demonstrating the bug
function test_DeficitCanNeverBeRepaid() public {
    // Setup: Create 1 USDC of bad debt
    uint256 badDebtAmount = 1e6;  // 1 USDC
    uint256 deficitRay = badDebtAmount * 1e27;  // 1e33

    // User attempts to repay the full amount
    uint256 repayAmount = badDebtAmount;  // 1 USDC

    // Simulate eliminateDeficit logic
    uint256 deficitAmountRay = repayAmount.toRay();  // 1e6 * 1e9 = 1e15
    uint256 remaining = deficitRay - deficitAmountRay;

    // Assert that debt is essentially unchanged
    assertGt(remaining, deficitRay * 99 / 100);  // >99% remains

    // Calculate how many USDC would actually be needed
    uint256 requiredUsdc = deficitRay / 1e9;  // 1e24 USDC
    assertEq(requiredUsdc, 1e24);  // 1 quintillion USDC
}

6. The Fix

The fix is straightforward: scale by 1e27 (RAY) instead of 1e9 (WAD-to-RAY conversion).

// BEFORE (Broken)
uint256 deficitAmountRay = amount.toRay();  // 1e9 scaling

// AFTER (Fixed)
uint256 deficitAmountRay = amount * 1e27;   // Direct RAY scaling

// Or use a dedicated function:
function assetToDeficitRay(uint256 assets, uint256 index) returns (uint256) {
    return assets * index;  // Matches how deficit is recorded
}