Bitallx · Complete repair
Alternative repair: sum bounded
Requires the sum to be at most the funded total: a bound, not an equality.
The exploit is blocked for a declared reason, and all 3 security and 10 legitimate-use obligations pass.
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: blockedIt fails in the attack or profit step, for a reason the task declares.test/poc.t.sol:Bitallx_PoC:testExploit()Payout total does not match the funded amount
Security obligations
3 / 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()
- ✓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 / 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,6 +91,11 @@9191 uint256 totalSendAmount9292 ) external {9393 require(wallet.length == amount.length, "The length of 2 arrays should be the same");94+ uint256 payoutTotal;95+ for (uint256 i = 0; i < amount.length; i++) {96+ payoutTotal += amount[i];97+ }98+ require(payoutTotal <= totalSendAmount, "Payout total does not match the funded amount");9499 95100 uint256 allowance = IBEP20(tokencontract).allowance(msg.sender, address(this));96101 require(allowance >= totalSendAmount, "Insufficient token allowance");
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/alt_complete_fix__sum_bounded/Token.sol \
--backend local --sha256Expected output: core 6ab3606f6d0fc6d017bbef39da2bbcfcd52537bef89758c46518aca84418ba55 and strict 0164491d777793056c490d3b59b18ef370c9bd996886082bc0574925ae83fc92.
To check a downloaded grade file instead: shasum -a 256 grade.strict.json prints the strict hash.
Control note
from the repositoryAn independent complete repair written against the shipped source: the sum must be <= the funded total (a bound, not an equality). Proves the security obligations credit a different implementation of the same property.