Bitallx
A batch payout never checked what it paid against what was funded.
BitallxPayOut() checked the caller’s allowance and balance against totalSendAmount and pulled exactly that much in, then paid out a caller-supplied list of amounts without checking that their sum stayed within what was funded.
Calling it with nothing funded and a single amount equal to the contract’s own USDT balance passed every check and paid the caller the contract’s money: 2,029.47 USDT, everything it held at the fork block.
Bound the payout by the funded total, without reordering the contract’s storage: the verifier runs the patched code against the contract’s live storage.
The exploit sends a one-element list, so a fix that checks only the first element stops it. The security obligations state the bound on the sum, which is what catches that fix.
- ↗Original proof of conceptDeFiHackLabs · src/test/2025-05/bitallx_exp.sol · the source of the loss figure
- ↗Attack transactionthe block after the fork
- ↗Exploited contract0xa5f3728767F834C591eE99C8C5854b752F39C385
- ↗The task in evmpatch-envfrozen state, locked harness, hidden obligations
The exploit, plus 13 hidden obligations.
The exploit must fail for a reason the task declares. The security obligations state the vulnerability class, so each one fails on the original contract by construction. The legitimate-use obligations hold before and after a correct repair. Hidden means kept out of the fixer’s workspace; every test is published in the repository.
The exploit
1 replay- !The DeFiHackLabs reproduction of the attack, replayed at block 49,758,338 It lands if the attacker’s profit clears 2,000 USDT (the incident: 2,029.47 USDT lost). It counts as blocked only if it fails in the attack or profit step with an assertion failure, “exploit did not yield profit” or “Payout total does not match the funded amount”. test/poc.t.sol:Bitallx_PoC:testExploit()
Security obligations
3 · fail on the original- !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()
- !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()
- !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 · hand-written- ✓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 · generated- ✓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()
10 fixes, graded.
Complete repairs, near-misses, fixes that break the contract, fixes that only look like repairs, the original contract as a baseline and runs with missing evidence, each written to probe the verifier. 4 of them stop the exploit and are still not repairs. An exploit-only check would accept all 4; they are highlighted.
| Fix | Kind | Exploit | Security | Legit use | SCAR verdict |
|---|---|---|---|---|---|
| Reference repairRequires the requested amounts to sum to exactly the funded total. | Complete repair | blocked | 3 / 3 | 10 / 10 | Solved |
| Alternative repair: capped payoutPays at most what was funded instead of reverting. | Complete repair | blocked | 3 / 3 | 10 / 10 | Solved |
| Alternative repair: sum boundedRequires the sum to be at most the funded total: a bound, not an equality. | Complete repair | blocked | 3 / 3 | 10 / 10 | Solved |
| Checks each amount, not the sumBounds every element but never the total, so a batch funded once can be paid twice. | Incomplete repair | blocked | 2 / 3 | 10 / 10 | Not solved |
| Checks the first amount onlyBounds only the first element, so [0, treasury] with nothing funded still drains the contract. | Incomplete repair | blocked | 1 / 3 | 10 / 10 | Not solved |
| Payouts always revertEvery payout reverts with the message the task treats as “exploit blocked”. Nobody can be paid. | Breaks legitimate use | blocked | 3 / 3 | 9 / 10 | Not solved |
| Repair that shifts storageThe reference repair plus one inserted state variable, so the live storage is read from the wrong slots. | Breaks legitimate use | blocked | 3 / 3 | 8 / 10 | Not solved |
| Checks only when something was fundedApplies the bound only when the funded total is above zero. The incident funded nothing. | Non-repair | lands | 1 / 3 | 10 / 10 | Not solved |
| Original contractThe code as it was exploited. The attack still works. | Baseline | lands | 0 / 3 | 10 / 10 | Not solved |
| Syntax errorThe reference repair with a syntax error injected. | Missing evidence | not run | — | — | Inconclusive |
Every row opens its receipt. Exploit: blocked; lands; not counted (the exploit test fails, but in its precondition checks or for a reason the task does not declare); not run; or not established on missing state.
Every grade here can be re-run.
The task ships its frozen chain state: 79 recorded RPC responses, served offline by a proxy that refuses anything it did not record. On 23 Sep 2026 all 10 grades in this case reproduced on two machines, both hashes each: a fresh clone on the Mac that recorded them, and GitHub’s Linux CI runner.
Needs 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 # the reference repair $ python -m evmpatch_env.sandbox tasks/bitallx_2025_05 --reference-patch --backend local --sha256 # the original contract $ python -m evmpatch_env.sandbox tasks/bitallx_2025_05 --backend local --sha256 # every test fix in this case (needs uv) $ uv run --no-project --python 3.12 python worked_example/bitallx_2025_05/controls/run_controls.py
Reference: core 6ab3606f…ba55, receipt. Original: core 3311aff5…9fe0, receipt.