Merge pull request #1 from ConsenSys/master

Update fork

mythril/laser/ethereum/helper.py

@@ -2,11 +2,33 @@ import re
 from z3 import *
 import logging
 
+import sha3 as _sha3
+import struct
+
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
 TT255 = 2 ** 255
 
 
+ALL_BYTES = tuple(
+            struct.pack('B', i)
+            for i in range(256)
+            )
+
+
+
+def zpad(x, l):
+    """ Left zero pad value `x` at least to length `l`.
+    >>> zpad('\xca\xfe', 4)
+    '\x00\x00\xca\xfe'
+    """
+    return b'\x00' * max(0, l - len(x)) + x
+
+
+def sha3(seed):
+    return _sha3.keccak_256(bytes(seed)).digest()
+
+
 def safe_decode(hex_encoded_string):
 
     if (hex_encoded_string.startswith("0x")):
@@ -90,3 +112,11 @@ def concrete_int_to_bytes(val):
         return val.to_bytes(32, byteorder='big')
 
     return (simplify(val).as_long()).to_bytes(32, byteorder='big')
+
+
+def bytearray_to_int(arr):
+    o = 0
+    for a in arr:
+        o = (o << 8) + a
+    return o
+

mythril/laser/ethereum/natives.py

@@ -0,0 +1,78 @@
+# -*- coding: utf8 -*-
+import copy
+import hashlib
+import coincurve
+
+from py_ecc.secp256k1 import N as secp256k1n
+
+from mythril.laser.ethereum.helper import ALL_BYTES, bytearray_to_int, concrete_int_to_bytes, sha3, zpad
+
+
+def int_to_32bytes(i):   #used because int can't fit as bytes function's input
+    o = [0] * 32
+    for x in range(32):
+        o[31 - x] = i & 0xff
+        i >>= 8
+    return bytes(o)
+
+
+def ecrecover_to_pub(rawhash, v, r, s):
+    try:
+        pk = coincurve.PublicKey.from_signature_and_message(
+            zpad(concrete_int_to_bytes(r), 32) + zpad(concrete_int_to_bytes(s), 32) +
+            ALL_BYTES[v - 27],
+            rawhash,
+            hasher=None,
+        )
+        pub = pk.format(compressed=False)[1:]
+    except BaseException:
+        pub = b"\x00" * 64
+
+    return pub
+
+
+def extract32(data, i):
+    if i >= len(data):
+        return 0
+    o = data[i: min(i + 32, len(data))]
+    o.extend(bytearray(32 - len(o)))
+    return bytearray_to_int(o)
+
+
+def ecrecover(data):
+    data = bytearray(data)
+    message = b''.join(map(lambda x: ALL_BYTES[x], data[0:32]))
+    v = extract32(data, 32)
+    r = extract32(data, 64)
+    s = extract32(data, 96)
+    if r >= secp256k1n or s >= secp256k1n or v < 27 or v > 28:
+        return []
+    try:
+        pub = ecrecover_to_pub(message, v, r, s)
+    except Exception as e:
+        return []
+    o = [0] * 12 + [x for x in sha3(pub)[-20:]]
+    return o
+
+
+def sha256(data):
+    data = bytes(data)
+    return hashlib.sha256(data).digest()
+
+
+def ripemd160(data):
+    data = bytes(data)
+    return 12*[0]+[i for i in hashlib.new('ripemd160', data).digest()]
+
+
+def identity(data):
+    return copy.copy(data)
+
+
+def native_contracts(address, data):
+    '''
+    takes integer address 1, 2, 3, 4
+    '''
+
+    functions = (ecrecover, sha256, ripemd160, identity)
+    return functions[address-1](data)

mythril/laser/ethereum/svm.py

@@ -1,4 +1,4 @@
-from mythril.laser.ethereum import helper
+from mythril.laser.ethereum import helper, natives
 from ethereum import utils
 from enum import Enum
 from flags import Flags
@@ -388,7 +388,8 @@ class LaserEVM:
 
             elif op == 'BYTE':
                 s0, s1 = state.stack.pop(), state.stack.pop()
-
+                if not isinstance(s1, ExprRef):
+                    s1 = BitVecVal(s1, 256)
                 try:
                     n = helper.get_concrete_int(s0)
                     oft = (31 - n) * 8
@@ -887,7 +888,7 @@ class LaserEVM:
                 # True case
                 condi = condition if type(condition) == BoolRef else condition != 0
                 if instr['opcode'] == "JUMPDEST":
-                    if not is_false(simplify(condi)):
+                    if (type(condi) == bool and condi) or (type(condi) == BoolRef and not is_false(simplify(condi))):
                         new_gblState = LaserEVM.copy_global_state(gblState)
                         new_gblState.mstate.pc = i
                         new_gblState.mstate.constraints.append(condi)
@@ -902,7 +903,7 @@ class LaserEVM:
                 # False case
                 negated = Not(condition) if type(condition) == BoolRef else condition == 0
 
-                if not is_false(simplify(negated)):
+                if (type(negated)==bool and negated) or (type(condi) == BoolRef and not is_false(simplify(negated))):
                     new_gblState = LaserEVM.copy_global_state(gblState)
                     new_gblState.mstate.constraints.append(negated)
                     new_gblState.mstate.depth += 1
@@ -987,17 +988,31 @@ class LaserEVM:
                             logging.debug("Unsupported memory symbolic index")
                         continue
 
-                if not re.match(r"^0x[0-9a-f]{40}", callee_address):
+                if (not re.match(r"^0x[0-9a-f]{40}", callee_address) and re.match(r"^0x[0-9a-f]{5,}",callee_address)):
                         logging.debug("Invalid address: " + str(callee_address))
                         ret = BitVec("retval_" + str(instr['address']), 256)
                         state.stack.append(ret)
                         continue
 
-                if (int(callee_address, 16) < 5):
+                if int(callee_address, 16) < 5 and int(callee_address, 16) > 0:
 
                     logging.info("Native contract called: " + callee_address)
+                    calldata, calldata_type = self._get_calldata(meminstart, meminsz, state, pad=False)
+                    if calldata == [] and calldata_type == CalldataType.SYMBOLIC:
+                        logging.debug("CALL with symbolic data not supported")
+                        continue
+
+                    data = natives.native_contracts(int(callee_address, 16 ), calldata)
+                    try:
+                        mem_out_start = helper.get_concrete_int(memoutstart)
+                        mem_out_sz = memoutsz.as_long()
+                    except AttributeError:
+                        logging.debug("CALL with symbolic start or offset not supported")
+                        continue
 
-                    # Todo: Implement native contracts
+                    state.mem_extend(mem_out_start, mem_out_sz)
+                    for i in range(min(len(data), mem_out_sz)):     # If more data is used then it's chopped off
+                        state.memory[mem_out_start+i] = data[i]
 
                     ret = BitVec("retval_" + str(instr['address']), 256)
                     state.stack.append(ret)
@@ -1052,24 +1067,8 @@ class LaserEVM:
                     state.stack.append(ret)
                     continue
 
-                try:
-                    # TODO: This only allows for either fully concrete or fully symbolic calldata.
-                    # Improve management of memory and callata to support a mix between both types.
-
-                    calldata = state.memory[helper.get_concrete_int(meminstart):helper.get_concrete_int(meminstart + meminsz)]
-
-                    if (len(calldata) < 32):
-                        calldata += [0] * (32 - len(calldata))
-
-                    calldata_type = CalldataType.CONCRETE
-                    logging.debug("Calldata: " + str(calldata))
-
-                except AttributeError:
-
-                    logging.info("Unsupported symbolic calldata offset")
-                    calldata_type = CalldataType.SYMBOLIC
-                    calldata = []
 
+                calldata, calldata_type = self._get_calldata(meminstart, meminsz, state)
                 self.call_stack.append(instr['address'])
                 self.pending_returns[instr['address']] = []
 
@@ -1180,3 +1179,22 @@ class LaserEVM:
 
         logging.debug("Returning from node " + str(node.uid))
         return node
+    def _get_calldata(self,meminstart, meminsz, state, pad = True):
+        try:
+            # TODO: This only allows for either fully concrete or fully symbolic calldata.
+            # Improve management of memory and callata to support a mix between both types.
+
+            calldata = state.memory[helper.get_concrete_int(meminstart):helper.get_concrete_int(meminstart + meminsz)]
+
+            if (len(calldata) < 32 and pad):
+                calldata += [0] * (32 - len(calldata))
+
+            calldata_type = CalldataType.CONCRETE
+            logging.debug("Calldata: " + str(calldata))
+
+        except AttributeError:
+
+            logging.info("Unsupported symbolic calldata offset")
+            calldata_type = CalldataType.SYMBOLIC
+            calldata = []
+        return calldata, calldata_type

setup.py

@@ -6,7 +6,7 @@ import os
 # Package version (vX.Y.Z). It must match git tag being used for CircleCI
 # deployment; otherwise the build will failed.
 
-VERSION = "v0.18.4"
+VERSION = "v0.18.5"
 
 
 class VerifyVersionCommand(install):

tests/native_test.py

@@ -0,0 +1,117 @@
+import json
+from mythril.ether.soliditycontract import SolidityContract
+
+from mythril.laser.ethereum.svm import GlobalState, MachineState
+from mythril.laser.ethereum import svm
+from tests import *
+
+
+SHA256_TEST = [ (0,False) for i in range(6)]
+
+RIPEMD160_TEST = [ (0,False) for i in range(6)]
+
+ECRECOVER_TEST = [ (0,False) for i in range(9)]
+
+IDENTITY_TEST = [ (0, False) for i in range(4)]
+
+SHA256_TEST[0] = (5555555555555555, True)     #These are Random numbers to check whether the 'if condition' is entered or not(True means entered)
+SHA256_TEST[1] = (323232325445454546, True)
+SHA256_TEST[2] = (34756834765834658, False)
+SHA256_TEST[3] = (8756476956956795876987, True)
+SHA256_TEST[4] = (5763467587689578369, True)
+SHA256_TEST[5] = (948365957658767467857, False)
+
+RIPEMD160_TEST[0] = (1242435356364, True)
+RIPEMD160_TEST[1] = (6732648654386435, True)
+RIPEMD160_TEST[2] = (97457657536546465, False)
+RIPEMD160_TEST[3] = (56436346436456546, True)
+RIPEMD160_TEST[4] = (999999999999999999993, True)
+RIPEMD160_TEST[5] = (1111111111112, False)
+
+
+ECRECOVER_TEST[0] = (786428768768632537676, True)
+ECRECOVER_TEST[1] = (4897983476979346779638, False)
+ECRECOVER_TEST[2] = (674837568743979857398564869, True)
+ECRECOVER_TEST[3] = (3487683476979311, False)
+ECRECOVER_TEST[4] = (853729594875984769847369, True)
+ECRECOVER_TEST[5] = (83579382475972439587, False)
+ECRECOVER_TEST[6] = (8437589437695876985769, True)
+ECRECOVER_TEST[7] = (9486794873598347697596, False)
+ECRECOVER_TEST[8] = (346934876983476, True)
+
+IDENTITY_TEST[0] = (87426857369875698, True)
+IDENTITY_TEST[1] = (476934798798347, False)
+
+IDENTITY_TEST[2] = (7346948379483769, True)
+IDENTITY_TEST[3] = (83269476937987, False)
+
+def _all_info(laser):
+    accounts = {}
+    for address, _account in laser.accounts.items():
+        account = _account.as_dict()
+        account["code"] = account["code"].instruction_list
+        account['balance'] = str(account['balance'])
+        accounts[address] = account
+
+    nodes = {}
+    for uid, node in laser.nodes.items():
+        states = []
+        for state in node.states:
+            if isinstance(state, MachineState):
+                states.append(state.as_dict())
+            elif isinstance(state, GlobalState):
+                environment = state.environment.as_dict()
+                environment["active_account"] = environment["active_account"].address
+                states.append({
+                    'accounts': state.accounts.keys(),
+                    'environment': environment,
+                    'mstate': state.mstate.as_dict()
+                })
+
+        nodes[uid] = {
+            'uid': node.uid,
+            'contract_name': node.contract_name,
+            'start_addr': node.start_addr,
+            'states': states,
+            'constraints': node.constraints,
+            'function_name': node.function_name,
+            'flags': str(node.flags)
+        }
+
+    edges = [edge.as_dict() for edge in laser.edges]
+
+    return {
+        'accounts': accounts,
+        'nodes': nodes,
+        'edges': edges,
+        'total_states': laser.total_states,
+        'max_depth': laser.max_depth
+    }
+
+def _test_natives(laser_info, test_list, test_name):
+    success = 0
+    for i,j in test_list:
+        if (str(i) in laser_info) == j:
+            success+=1
+        else:
+            print ("Failed: "+str(i)+" "+str(j))
+    assert(success == len(test_list))
+
+
+
+class NativeTests(BaseTestCase):
+    def runTest(self):
+        disassembly = SolidityContract('./tests/native_tests.sol').disassembly
+        account = svm.Account("0x0000000000000000000000000000000000000000", disassembly)
+        accounts = {account.address: account}
+
+        laser = svm.LaserEVM(accounts, max_depth = 100)
+        laser.sym_exec(account.address)
+        laser_info = str(_all_info(laser))
+        print('\n')
+
+        _test_natives(laser_info, SHA256_TEST, 'SHA256')
+        _test_natives(laser_info, RIPEMD160_TEST, 'RIPEMD160')
+        _test_natives(laser_info, ECRECOVER_TEST, 'ECRECOVER')
+        _test_natives(laser_info, IDENTITY_TEST, 'IDENTITY')
+

tests/native_tests.sol

@@ -0,0 +1,166 @@
+pragma solidity ^0.4.17;
+
+
+contract Caller {
+
+    address public fixed_address;  //Just some useless variables
+    address public stored_address;  
+
+    uint256 statevar;        //useless( but good for testing as they contribute as decoys)
+    bytes32 far;
+
+    function Caller(address addr) { 
+        fixed_address = addr;
+    }
+
+    function thisisfine() public {      //some typical function as a decoy
+        fixed_address.call();
+    }
+    function sha256_test1() public {
+        uint256 i;
+        if(sha256('ab','c') == 0xba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad){    //True
+            i = 5555555555555555;
+        }
+
+        if(sha256('abc') == 0xba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad){      //True
+            i = 323232325445454546;
+        }
+    }
+    function sha256_test2() public {
+        uint256 i;
+        if(sha256('abd') == 0xba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad) {     //False
+            i = 34756834765834658;
+        }
+        if(sha256('ab','d') == 0xa52d159f262b2c6ddb724a61840befc36eb30c88877a4030b65cbe86298449c9) {  //True
+            i = 8756476956956795876987;
+        }
+    }
+    function sha256_test3() public {
+        uint256 i;
+        if(sha256('') == 0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855) {         //True
+            i = 5763467587689578369;
+        }
+        if(sha256('hhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhfdhhfdhhhhhh') == 0xe4ebd771f821e3277b77dcc39e94fe7172a5c9c8c12f8885c2d5513385a0a8b8) {  //False
+            i = 948365957658767467857;
+        }
+    }
+
+    function ripemd_test1() public {
+        uint256 i;
+        if(ripemd160('ab','c') == 0x8eb208f7e05d987a9b044a8e98c6b087f15a0bfc){    //True
+            i = 1242435356364;
+        }
+        if(ripemd160('abc') == 0x8eb208f7e05d987a9b044a8e98c6b087f15a0bfc){      //True
+            i = 6732648654386435;
+        }
+    }
+    function ripemd_test2() public {
+        uint256 i;
+        if(ripemd160('abd') == 0x8eb208f7e05d987a9b044a8e98c6b087f15a0bfc) {     //False
+            i = 97457657536546465;
+        }
+        if(ripemd160('ab','d') == 0xb0a79cc77e333ea11974e105cd051d33836928b0) {  //True
+            i = 56436346436456546;
+        }
+    }
+    function ripemd_test3() public {
+        uint256 i;
+        if(ripemd160('') == 0x9c1185a5c5e9fc54612808977ee8f548b2258d31) {         //True
+            i = 999999999999999999993;
+        }
+        if(ripemd160('hhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhhh') == 0x2d1b88a5daa5d138eb7bb14ee320010937f0ebe7) {  //False
+            i = 1111111111112;
+        }
+    }
+
+    function ecrecover_test1() public {
+        bytes32 foobar = 0x1c8aff950685c2ed4bc3174f3472287b56d9517b9c948127319a09a7a36deac8;
+        bytes memory prefix = "\x19Ethereum Signed Message:\n32";
+        bytes32 prefixedHash = keccak256(prefix, foobar);
+        uint8 v = 28;
+        bytes32 r = 0x9242685bf161793cc25603c231bc2f568eb630ea16aa137d2664ac8038825608;
+        bytes32 s = 0x4f8ae3bd7535248d0bd448298cc2e2071e56992d0774dc340c368ae950852ada;
+        if( ecrecover(prefixedHash, v, r, s) == 0x7156526fbd7a3c72969b54f64e42c10fbb768c8a)   {  //True
+            uint256 bignum = 786428768768632537676;
+        }
+        if( ecrecover(prefixedHash, v, r, s) == 0x7156526fbd7a3c72969b54f64e42c10fbb768c8b) {   //False
+            uint256 small = 4897983476979346779638;
+        }
+        foobar = 0x38d18acb67d25c8bb9942764b62f18e17054f66a817bd4295423adf9ed98873e;
+        if( ecrecover( keccak256(foobar), v, r, s) == 0x0faf91ea0aaaa5377dfdf188b21409007f0b4019) {    //True
+            uint256 dk = 674837568743979857398564869;
+        }
+        foobar = 0x38d18acb67d25c7bb9942764b62f18e17054f66a817bd4295423adf9ed98873e; //not same as above, minor change(7bb instead of 8bb)
+        if( ecrecover( keccak256(foobar), v, r, s) == 0x0faf91ea0aaaa5377dfdf188b21409007f0b4019) {    //False
+            uint256 pk = 3487683476979311;
+        }
+
+    }
+
+    function ecrecover_test2() public {
+        bytes32 foobar = 0x1c8aff950685c2ed4bc3174f3472287b56d9517b9c948127319a09a7a36deac8;
+        bytes memory prefix = "\x19Ethereum Signed Message:\n32";
+        bytes32 prefixedHash = keccak256(prefix, foobar);
+        uint8 v = 26;
+        bytes32 r = 0x9242685bf161793cc25603c231bc2f568eb630ea16aa137d2664ac8038825608;
+        bytes32 s = 0x4f8ae3bd7535248d0bd448298cc2e2071e56992d0774dc340c368ae950852ada;
+        if( ecrecover(prefixedHash, v, r, s) == 0x0000000000000000000000000000000000000000)   {   //True
+            uint256 bignum = 853729594875984769847369;
+        }
+        if( ecrecover(prefixedHash, v, r, s) == 0x7156526fbd7a3c72969b54f64e42c10fbb768c8b) {     //False
+            uint256 small = 83579382475972439587;
+        }
+    }
+    function ecrecover_test3() public {
+        bytes32 foobar = 0x1c8aff950685c2ed4bc3174f3472287b56d9517b9c948127319a09a7a36deac8;
+        bytes memory prefix = "\x19Ethereum Signed Message:\n32";
+        bytes32 prefixedHash = keccak256(prefix, foobar);
+        uint8 v = 29;
+        bytes32 r = 0x9242685bf161793cc25603c231bc2f568eb630ea16aa137d2664ac8038825608;
+        bytes32 s = 0x4f8ae3bd7535248d0bd448298cc2e2071e56992d0774dc340c368ae950852ada;
+        if( ecrecover(prefixedHash, v, r, s) == 0x0000000000000000000000000000000000000000)   {   //True
+            uint256 bignum = 8437589437695876985769;
+        }
+        if( ecrecover(prefixedHash, v, r, s) == 0x7156526fbd7a3c72969b54f64e42c10fbb768c8b) {     //False
+            uint256 small = 9486794873598347697596;
+        }
+    }
+    function ecrecover_test4() public {
+        bytes32 foobar = 0x1c8aff950685c2ed4bc3174f3472287b56d9517b9c948127319a09a7a36deac8;
+        bytes memory prefix = "\x19Ethereum Signed Message:\n32";
+        bytes32 prefixedHash = keccak256(prefix, foobar);
+        uint8 v = 27;
+        bytes32 r = 0xfffffffffffffffffffffffffffffffffaaedce6af48a03bbfd25e8cd0364141;  //greater than the max limit
+        bytes32 s = 0x4f8ae3bd7535248d0bd448298cc2e2071e56992d0774dc340c368ae950852ada;
+
+        if( ecrecover(prefixedHash, v, r, s) == 0x0000000000000000000000000000000000000000)   {   //True
+            uint256 bignum = 346934876983476;
+        }
+    }
+    function need_identity_invoke(uint sea) returns (uint) {
+        return sea;                                     //identity is invoked here in compiler and not below
+    }
+    function identity_function(int input) public returns(int out) {
+        assembly{
+            let x := mload(0x40)
+            mstore(x, input)
+
+            let success := call(500000000, 0x4, 100000, x, 0x20, x, 0x20)
+            out := mload(x)
+            mstore(0x40, x)
+        }
+    }
+    function identity_test1() public{
+        if(identity_function(100)==100)         //True
+            uint256 smallnum = 87426857369875698;
+        if(identity_function(200)==100)         //False
+            uint256 bignum = 476934798798347;
+    }
+    function identity_test2() public{
+        if(identity_function(12345678)==12345678)         //True
+            uint256 smallnum = 7346948379483769;
+        if(identity_function(74648796976)==4685987)         //False
+            uint256 bignum = 83269476937987;
+    }
+
+}