Bitallx · Non-repair
Checks only when something was funded
Applies the bound only when the funded total is above zero. The incident funded nothing.
The historical exploit still succeeds against the frozen state.
What ran, and what it said.
Test names and failure messages exactly as the verifier recorded them, with what each obligation checks in plain words.
Exploit
1 replay · profit over 2,000 USDT- ✗The DeFiHackLabs reproduction of the attack: landsIt still clears the case’s profit threshold (2,000 USDT).test/poc.t.sol:Bitallx_PoC:testExploit()
Security obligations
1 / 3 pass- ✗A batch whose total exceeds what was funded pays nothing[0, treasury] with nothing funded: the shape a first-element-only fix lets through.test/hidden/security.t.sol:Bitallx_Security:test_multi_element_over_request_pays_nothing()unfunded multi-element payout drained the contract's own USDT treasury: 0 < 2029473999999999986000
- ✗The incident’s own shape pays nothingA one-element over-request from a payer who funded nothing, kept as a standing obligation.test/hidden/security.t.sol:Bitallx_Security:test_single_element_over_request_from_fresh_payer_pays_nothing()unfunded single-element payout drained the contract's own USDT treasury: 0 < 2029473999999999986000
- ✓The sum is bounded, not just each element[total, total] funded once must not be paid twice.test/hidden/security.t.sol:Bitallx_Security:test_sum_over_funded_total_rejected_even_when_each_element_fits()
Legitimate use · behaviour
5 / 5 pass- ✓A funded batch payout pays everyone correctlyThe contract’s actual purpose.test/hidden/regression.t.sol:Bitallx_Regression:test_funded_batch_payout_distributes_correctly()
- ✓The patched code still reads the contract’s live storageA fix that inserts or reorders state variables would re-point every one of them.test/hidden/regression.t.sol:Bitallx_Regression:test_live_storage_still_readable()
- ✓The owner’s treasury sweep works, and only for the ownertest/hidden/regression.t.sol:Bitallx_Regression:test_owner_treasury_path_still_works()
- ✓An unfunded payer is refusedtest/hidden/regression.t.sol:Bitallx_Regression:test_payout_rejects_an_unfunded_payer()
- ✓The publisher can still pay a reward, within its limitstest/hidden/regression.t.sol:Bitallx_Regression:test_publisher_can_still_pay_a_reward()
Legitimate use · interface
5 / 5 pass- ✓Original functions still answerCalls the original functions and requires an answer other than “no such function”.test/hidden/invariants_auto.t.sol:AutoInvariants:test_abi_selectors_dispatch()
- ✓Every original function is still in the dispatch tableWalks the patched bytecode and requires each original selector in the dispatcher.test/hidden/invariants_auto.t.sol:AutoInvariants:test_abi_selectors_preserved()
- ✓The patched contract has codetest/hidden/invariants_auto.t.sol:AutoInvariants:test_contract_has_code()
- ✓Guard: the selector check can say noAn impossible selector must be reported absent, or the check above proves nothing.test/hidden/invariants_auto.t.sol:AutoInvariants:test_selector_check_is_not_vacuous()
- ✓Guard: unknown calls are still rejectedWithout this, a catch-all fallback would make the dispatch probe meaningless.test/hidden/invariants_auto.t.sol:AutoInvariants:test_unknown_selector_is_rejected()
The patch
against the original source@@ -91,7 +91,21 @@9191 uint256 totalSendAmount9292 ) external {9393 require(wallet.length == amount.length, "The length of 2 arrays should be the same");94− 94+95+ // PATCH: bound the payout by what was actually funded. Every check below -- the96+ // allowance, the sender's balance, and the transferFrom that pulls money IN -- is97+ // against `totalSendAmount`, while the loop below paid out the caller-supplied98+ // `amount[]` with nothing tying the two together. Calling this with99+ // totalSendAmount = 0 and amount[0] = the contract's own balance therefore passed100+ // every check and paid the caller the contract's treasury.101+ uint256 requested = 0;102+ for (uint256 i = 0; i < amount.length; i++) {103+ requested += amount[i];104+ }105+ if (totalSendAmount > 0) {106+ require(requested == totalSendAmount, "Payout total does not match the funded amount"); // VARIANT: never fires for the attack107+ }108+95109 uint256 allowance = IBEP20(tokencontract).allowance(msg.sender, address(this));96110 require(allowance >= totalSendAmount, "Insufficient token allowance");97111
Re-run this grade
offline · same inputsNeeds Foundry 1.7.1 with solc 0.8.30, 0.8.26 and 0.8.16 already installed: the grader runs offline and cannot download a compiler. Python 3.12 or later. Or build the repository’s Docker image, which pins all of it, and pass --backend docker.
$ git clone https://github.com/FarseenSh/evmpatch-env.git && cd evmpatch-env
$ git checkout 165c0ed
$ python -m evmpatch_env.sandbox tasks/bitallx_2025_05 \
--patch worked_example/bitallx_2025_05/controls/non_repair__bound_only_when_funded/Token.sol \
--backend local --sha256Expected output: core 5b70aa193f447f737698ba3cec3fe99822198e9a532c5cde17a9b77319350e37 and strict 84a93e6988ed7d6ea241ab76476d4541676ca420d67e73fd9e10a00bae9ac728.
To check a downloaded grade file instead: shasum -a 256 grade.strict.json prints the strict hash.
Control note
from the repositoryThe reference bound applied only when totalSendAmount > 0. The whole incident is totalSendAmount = 0, so the shipped PoC catches it with no help from the security suite.