Solidity’s SMTChecker can automatically find real bugs

Leonardo Alt
Feb 26 · 2 min read
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;
}
}
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

Leonardo Alt

Written by

Building Solidity and Formal Verification tools.

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade