Introduce RK87

RK87

RK87 is a symbolic platform for solidity smart contracts. User can add assertions and assumptions into existing solidity code base to let symbolic engine search for counterexamples or get verified.

RK87 is the only platform that allow user to do symbolic verifier using only solidity language and some small support directives.

How it works?

RK87 first compiles solidity source code into symbolic represents, and then z3 engine will be used to perform analysis. Additional directives can be added to support declarations and verifications.

Example

pragma solidity ^0.4.25;

library SafeMath {
    function mul(uint256 a, uint256 b) internal constant returns (uint256) {
        uint256 c = a * b;
        assert(a == 0 || c / a == b);
        return c;
    }

    function div(uint256 a, uint256 b) internal constant returns (uint256) {
        uint256 c = a / b;
        return c;
    }

    function sub(uint256 a, uint256 b) internal constant returns (uint256) {
        assert(b <= a);
        return a - b;
    }

    function add(uint256 a, uint256 b) internal constant returns (uint256) {
        uint256 c = a + b;
        assert(c >= a);
        return c;
    }
}

contract BEC{
    /**
    * BEC batchTransfer bug
    * https://etherscan.io/address/0xc5d105e63711398af9bbff092d4b6769c82f793d#code
    **/
    using SafeMath for uint256;

    mapping(address => uint256) balances;
    /**
    * %rk-check no_overflow
    **/
    function batchTransfer(address[] _receivers, uint256 _value) public returns (bool) {
        // %rk-for-all address a: balances[a] == 0
        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);
        }
        /**%rk-assert
        * [[Token should not appear from nowhere]]
        *    balances[address(0x1111111111111111111111111111111111111111)] == 0
        **/
        return true;
    }
}