Solidity’s SMTChecker can automatically find real bugs

In my previous post (https://medium.com/@leonardoalt/formal-verification-in-solidity-5cbff7b7ff8) I wrote about the SMTChecker, a formal verification module embedded in Solidity’s compiler that is under development. The goal of the SMTChecker is to be a compile-time automated prover and bug finder, where properties are specified using Solidity’s require/assert.

While developing the SMTChecker we often try examples from other more stable/established formal verification tools, which we use as benchmarks for what should be supported and proved. After reading https://medium.com/ethworks/formal-verification-for-n00bs-part-3-an-attempt-to-prevent-classic-hack-with-klab-8e8d13318086, we were curious to see how the SMTChecker would perform on that example after our recent work on supporting arrays and reporting fewer false positives when SafeMath is used.

The bug analyzed here is the batch overflow vulnerability. The following code snippet is a reduced version of the full contract which contains the original function:

pragma solidity ^0.5.0;
pragma experimental SMTChecker;
import "./SafeMath.sol";
contract Bug
{
using SafeMath for uint256;
bool paused = false;
mapping (address => uint) balances;
modifier whenNotPaused {
  require(!paused);
  _;
}
function batchTransfer(
  address[] memory _receivers,
  uint256 _value
) public whenNotPaused returns (bool) {
  uint cnt = _receivers.length;
  uint256 amount = uint256(cnt) * _value;
  require(cnt > 0 && cnt <= 20);
  require(_value > 0 && balances[msg.sender] >= amount);
  balances[msg.sender] = balances[msg.sender].sub(amount);
  for (uint i = 0; i < cnt; i++) {
    balances[_receivers[i]] = balances[_receivers[i]].add(_value);
    //Transfer(msg.sender, _receivers[i], _value);
  }
  return true;
}
}

Briefly, the bug is an overflow in the operation uint256(cnt) * _value . An attacker can choose specific _receivers and a huge _value such that cnt > 0 && cnt <= 20 is true and amount is small, such that they have enough funds. Notice that the gain is in balances[_receivers[i]].add(_value) , where _value might be much higher than it should be.

If we simply run the compiler on the example, the output (among some false positives) contains:

bug.sol:18:20: Warning: Overflow (resulting value larger than 2**256 - 1) happens here
  uint256 amount = uint256(cnt) * _value;
                   ^-------------------^
  for:
  <result> = 2**256
  _value = 0x80 * 2**248
  amount = 0
  balances[msg.sender] = 0
  cnt = 2
  msg.sender = 2997

The run took 10.24s with 2 backend SMT solvers on my laptop. It basically tells us how to exploit the bug: call batchTransfer(_receivers, 0x80 * 2**248) , where _receivers is an array with two addresses. After the overflow, amount = 0 which satisfies balances[msg.sender] >= amount . The addresses will then receive 0x80 * 2**248 tokens each.

This example shows that the SMTChecker can be used at compile-time to quickly find real bugs, even though it still lacks support to parts of Solidity. We are constantly increasing the power of the SMTChecker, hopefully eventually making it able to fully analyze complex smart contracts automatically.

If you have any questions/ideas please reach out! You can comment here, talk to us on our Gitter channel or start a thread in the Solidity repository.