Formal verification example

Question

I am currently taking a look at the slides from this presentation

I suppose the question is less with formal verification and more with solidity. Can some one help me understand what can possibly go wrong with this contract on transfer?

contract Token {
  mapping(address => uint) balances;
  function transfer(address from, address to, uint amount) {
    if (balances[from] >= amount) {
      balances[from] -= amount;
      balances[to] += amount
    }
  }
}

Question : Example: Is the sum of all balances unchanged by transfer()?

Coming from a c++ background , i honestly do not see the issue.

Answer 1

The transfer function can't handle the overflow and underflow of token while transferring to another account.For example, if your investor's balance exceeds the maximum value of (2^256) then, the token value becomes zero. This can be handled using the safeAdd and safeSub function. The sum of all balance won't be changed while transferring tokens to another account.

Answer 2

If this transfer function is used to send tokens to a contract address, then the sent token will be stuck in the contract since there is no private key controlling the smart contract (the contract will not recognize this transaction); One should only use the transfer function to send tokens to addresses which are externally owned i.e. there is a private key which controls it.

Therefore one should be super-cautious when using ERC20 tokens. The transfer function should be used to send tokens to an externally owned address, while sending tokens to a contract can only be done via calling approve+transferFrom.

Answer 3

I'm no expert on formal verification and @istvan's answer is helpful. Indeed, one can transfer the coins to an address one doesn't control (the usual idea), but there is no guarantee anyone or anything has sufficient control to ever spend them. Alice sent to Bob. Bob lost his key. Poor Bob.

Solidity has some new verbs to replace the old throw and help automated verification systems assess the correctness of the code: require, assert and 'revert'. In summary, use require to concentrate on inputs and assert to verify normal conditions (an assert should never be false). revert is still available as an approximate replacement for throw.

Details: Difference between require and assert and the difference between revert and throw

A quick reinterpretation of the example code might look something like:

contract Token {
  mapping(address => uint) balances;
  function transfer(address from, address to, uint amount) {
    require(balances[from] >= amount);

    uint initialSum = balances[from] + balances[to];
    balances[from] -= amount;

    // update, safeAdd idea
    require(balances[to] < balances[to] + amount);
    balances[to] += amount
    uint newSum = balances[from] + balances[to];

    assert(newSum == initialSum);
    }
  }
}

Now a verification suite can explore possibilities. It can try a range of inputs and cases that pass the require and see if there is ever any scenario in which that assert fails. If the assert can fail it would be treated as a discovered defect.

Hope it helps.

Update: @karthikeyan has a good point about safe math, so added a little overflow check.