Abracadabra GMX V2 Cauldron Exploit - Phylax Credible Layer Documentation

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 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:

Setup: Attacker creates a failed GMX deposit, leaving tokens in the RouterOrder contract
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:

// 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:

Captures reported collateral from the buggy orderValueInCollateral() function
Calculates actual extractable value by checking real token balances
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.

​What Happened

​Assertion Pattern

​How the Assertion Would Have Prevented It

What Happened

Assertion Pattern

How the Assertion Would Have Prevented It