Check the integrity of balances

[luongnt95]

This PR checks if the amount of balance transfered by the sender and the amount of balance received by the receiver are the same. The below is the contract being used to test the PR. This contract contains a bug in the line balances[msg.sender] -= 2; so it is expected to display "ERC20 bug" in the result.

contract ERC20 {
  // Balances for each account
  mapping(address => uint256) balances;
  bytes32 public diff;

  function transfer(address _to, uint256 _amount){
    uint256 prev_sender = balances[msg.sender];
    uint256 prev_to = balances[_to];
    if (balances[msg.sender] >= _amount && _amount > 0 && balances[_to] + _amount > balances[_to]) {
      balances[msg.sender] -= (_amount + 2);
      balances[_to] += (_amount + 3);
      if (sha3(msg.data) < diff) {
        balances[msg.sender] -= 2;
        balances[_to] -= 3;
        assert(prev_sender - _amount == balances[msg.sender] && prev_to + _amount == balances[_to]);
      }
    }
  }
}

The method that I used to detect the bug is that I use assertion to detect if the condition of the assertion satisfies just by checking if the program would jump into INVALID or not. Because our program uses symbolic values, there's no way for our program to understand that these two lines

balances[msg.sender] -= (_amount + 2);
balances[msg.sender] -= 2;

use the same variable which share a key in the storage. Based on the layout of mapping variables in storage, I tried to simulate the process of storing and loading a mapping variable like balances. The pattern to load or store the key of a mapping variable in storage is something like: MSTORE -> SHA3 -> SLOAD

[inian]

s0 and s1 may be symbolic - that case should be handled here right?

[luongnt95]

Yeah. This PR is not complete. This SHA3 works with my tests when it's used to find a key in the storage. Other SHA3 should be handled differently as s0 and s1 could be symbolic

[loiluu]

Do consider the overlapping with this PR #144 !