External call does not change the storage of the callee contract.

[Just1ceP4rtn3r]

Description

When I tried to write a new analysis module to detect the problems with state variables in storage, I found some confusing situations with multiple smart contracts (e.g., external calls to the function of another contract).
If there is an external call in the contract Pool (see below), that will change the value of the state variable (i.e., balances) in another contract myToken, mythril failed to record (or execute) the change of the state variable in the storage of myToken.

How to Reproduce

For instance, when presented with the following two contracts (myToken and Pool), I utilize the analysis module 'Test' to print the value of state variable balances[Attacker] after invoking function myToken.deposit(), which will decrease the value to balances[Attacker]. However, the output shows that the value of this variable has not been altered.

• Contracts

pragma solidity ^0.5.12;


contract myToken {

  mapping(address => uint) public balances;

    constructor() public {
        balances[address(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF)] = 2;
    }

  function deposit() public {
    balances[address(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF)] = balances[address(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF)] - 1;
  }

    function getBalance() public view returns (uint) {
    return balances[address(0xDeaDbeefdEAdbeefdEadbEEFdeadbeEFdEaDbeeF)];
  }

}


contract Pool {

    myToken token_1 = new myToken();

  function test() public {
    token_1.deposit();
  }

}

• Analysis Module

class Test(DetectionModule):
    """This module search for cases where Ether can be withdrawn to a user-
    specified address."""

    name = "Test"
    swc_id = "Test"
    description = DESCRIPTION
    entry_point = EntryPoint.CALLBACK
    # pre_hooks = ["SSTORE",]
    post_hooks = ["CALL"]

    def reset_module(self):
        """
        Resets the module by clearing everything
        :return:
        """
        super().reset_module()

    def _execute(self, state: GlobalState) -> None:
        """
        :param state:
        :return:
        """
        potential_issues = self._analyze_state(state)

        annotation = get_potential_issues_annotation(state)
        annotation.potential_issues.extend(potential_issues)

    def _analyze_state(self, state):
        """
        :param state:
        :return:
        """
        instruction = state.get_current_instruction()


        pool_contract_account = None
        token_contract_account = None
       
       # To get account of the `Pool` and `token_1` 
        if(contractaddr.PoolAddr is not None and contractaddr.TokenAddr_1 is not None):
            pool_contract_account = state.world_state.accounts[contractaddr.PoolAddr]
            token_contract_account = state.world_state.accounts[contractaddr.TokenAddr_1]
        else:
            for account in state.world_state.accounts:
                if(account != ACTORS.creator.value and account != ACTORS.attacker.value and account != ACTORS.someguy.value):
                    if("Pool" in state.world_state.accounts[account].contract_name):
                        contractaddr.PoolAddr = account
                        pool_contract_account = state.world_state.accounts[account]
                        log.error("pool account: "+str(account))
                    else:
                        contractaddr.TokenAddr_1 = account
                        token_contract_account = state.world_state.accounts[account]
                        log.error("token account: "+str(account))



        token_slot_attacker = keccak_function_manager.create_keccak(symbol_factory.BitVecVal(0x000000000000000000000000deadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000000, 512))

        after_token = token_contract_account.storage[token_slot_attacker]

       # print the token after invoking `token_1.deposit();`
        log.error(after_token)

        constraints = state.world_state.constraints


        potential_issue = PotentialIssue(
            contract=state.environment.active_account.contract_name,
            function_name=state.environment.active_function_name,
            address=state.get_current_instruction()["address"],
            swc_id=self.swc_id,
            title=self.name,
            severity="Medium",
            bytecode=state.environment.code.bytecode,
            description_head=self.name,
            description_tail=self.name,
            detector=self,
            constraints=constraints,
        )
        return [potential_issue]

detector = Test()

• Mythril Output

The initial value of balances[Attacker] is 2. However, it remains unchanged at 2 even after the execution of the token_1.deposit() function.

$  myth  analyze pool.sol:Pool --execution-timeout 200 --parallel-solving -t 2 -m Test 


mythril.analysis.module.modules.Liveness_test [ERROR]: pool account: 51421440056055728346017419001665401074216449311
mythril.analysis.module.modules.Liveness_test [ERROR]: token account: 655251735853922694967911662580490717076041977877
mythril.analysis.module.modules.Liveness_test [ERROR]: 2
==== Test ====
SWC ID: Test
Severity: Medium
Contract: Pool
Function name: test()
PC address: 377
Estimated Gas Usage: 2519 - 37225
Test
Test
--------------------
In file: pool.sol:28

token_1.deposit()

--------------------
Initial State:

Account: [CREATOR], balance: 0x0, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}

Transaction Sequence:

Caller: [CREATOR], calldata: , decoded_data: , value: 0x0
Caller: [ATTACKER], function: test(), txdata: 0xf8a8fd6d, value: 0x0

Expected behavior

The value of balances[Attacker] should be 1 after calling function token_1.deposit().

Enviroment

• Mythril version: 0.23.25
• Solidity compiler and version: 0.5.12+commit.7709ece9.Linux.g++
• Python version: 3.10.12
• OS and Version: Ubuntu 22.04.2 LTS