> ## Documentation Index
> Fetch the complete documentation index at: https://docs.phylax.systems/llms.txt
> Use this file to discover all available pages before exploring further.

# Abracadabra GMX V2 Cauldron Exploit

> Exploit that drained $13.4M from Abracadabra's GMX V2 Cauldron through accounting manipulation in the RouterOrder system

This case study explains how the Abracadabra GMX V2 Cauldron exploit worked and which assertion pattern could have constrained the invalid state transition.

## What Happened

This exploit drained \$13.4M from Abracadabra's GMX V2 Cauldron through an accounting bug that created "phantom collateral" - allowing the same tokens to be borrowed against multiple times.

**The Core Bug:**

The `GmxV2CauldronRouterOrder` contract had two critical functions:

* **`sendValueInCollateral()`** - Extracted real tokens during liquidations
* **`orderValueInCollateral()`** - Reported collateral value for borrowing calculations

Link to the two functions: [https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/dff69a19a219bbff90ab7b752c9f9c0ab5e8fe6f/src/periphery/GmxV2CauldronOrderAgent.sol#L241-L280](https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/dff69a19a219bbff90ab7b752c9f9c0ab5e8fe6f/src/periphery/GmxV2CauldronOrderAgent.sol#L241-L280)

When `sendValueInCollateral()` removed tokens, it failed to update internal accounting variables (`inputAmount`, `minOut`, `minOutLong`). This meant `orderValueInCollateral()` continued reporting the original collateral value even after tokens were extracted.

**Exploitation Steps:**

1. **Setup**: Attacker creates a failed GMX deposit, leaving tokens in the RouterOrder contract
2. **Exploit Loop**:
   * Borrow MIM against the reported collateral value
   * Self-liquidate to extract real tokens via `sendValueInCollateral()`
   * Internal accounting remains unchanged - same collateral value still reported
   * Borrow again against the "phantom" collateral
   * Repeat until all real tokens are drained

The attacker could extract real value multiple times while the system's solvency checks continued to pass using stale accounting data.

## Assertion Pattern

The core issue was a fundamental violation of a basic invariant: reported collateral values should never exceed actual extractable assets. A simple phantom collateral assertion could have prevented this exploit:

```solidity theme={null}
// SPDX-License-Identifier: MIT
pragma solidity 0.8.28;

import {Assertion} from "../../lib/credible-std/src/Assertion.sol";
import {AssertionSpec} from "../../lib/credible-std/src/SpecRecorder.sol";
import {PhEvm} from "../../lib/credible-std/src/PhEvm.sol";

interface IGmxV2CauldronRouterOrder {
    function orderValueInCollateral() external view returns (uint256);
    function shortToken() external view returns (address);
    function getExchangeRates() external view returns (uint256 shortExchangeRate, uint256 marketExchangeRate);
    function sendValueInCollateral(address to, uint256 amount) external;
}

interface IERC20 {
    function balanceOf(address account) external view returns (uint256);
}

contract AbracadabraGmxV2Assertion is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    uint256 constant oracleDecimalScale = 1e30;

    function triggers() public view override {
        // Trigger on any call to sendValueInCollateral
        registerFnCallTrigger(
            this.assertPhantomCollateral.selector,
            IGmxV2CauldronRouterOrder.sendValueInCollateral.selector
        );
    }

    function assertPhantomCollateral() external view {
        IGmxV2CauldronRouterOrder routerOrder = IGmxV2CauldronRouterOrder(ph.getAssertionAdopter());
        // Get the reported collateral value from the potentially buggy function
        uint256 reportedCollateral = routerOrder.orderValueInCollateral();
        
        // Calculate actual extractable value based on real token balance
        address shortTokenAddr = routerOrder.shortToken();
        IERC20 shortToken = IERC20(shortTokenAddr);
        uint256 actualBalance = shortToken.balanceOf(address(routerOrder));
        
        // Convert to collateral value using the same exchange rates as orderValueInCollateral()
        (uint256 shortExchangeRate, uint256 marketExchangeRate) = routerOrder.getExchangeRates();
        
        uint256 actualExtractable = (actualBalance * shortExchangeRate * marketExchangeRate) / oracleDecimalScale;
        
        // Core invariant: Reported collateral must never exceed actual extractable value
        require(
            reportedCollateral <= actualExtractable,
            "PHANTOM_COLLATERAL: Reported collateral exceeds actual extractable value"
        );
    }
}
```

### How the Assertion Would Have Prevented It

This assertion implements a fundamental economic sanity check that would have caught the accounting manipulation:

**What it does:**

1. **Captures reported collateral** from the buggy `orderValueInCollateral()` function
2. **Calculates actual extractable value** by checking real token balances
3. **Enforces the invariant** that reported values cannot exceed actual extractable amounts

**Why it catches the exploit:**

The exploit succeeded because of the growing gap between reported and actual values:

* **Before exploit**: RouterOrder has 1000 USDC, `orderValueInCollateral()` returns 1000 USDC equivalent, actual balance = 1000 USDC → **Assertion passes** ✅
* **During exploit**: `sendValueInCollateral()` extracts 500 USDC, but `orderValueInCollateral()` still returns 1000 USDC equivalent, actual balance = 500 USDC → **Assertion fails** ❌
* **After multiple extractions**: All tokens extracted, but `orderValueInCollateral()` still returns 1000 USDC equivalent, actual balance = 0 USDC → **Assertion fails** ❌

**Key insight**: This assertion doesn't need to understand the complex GMX V2 order mechanics or the specific accounting bug. It simply enforces the fundamental principle that "you cannot extract more value than actually exists" - a rule the exploit fundamentally violated.
