From f19dd5df91eb926b2f6f706cfd37c462f27949dc Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 13 Jun 2018 21:29:30 +0200 Subject: [PATCH 1/5] Make variable bitvec --- mythril/laser/ethereum/svm.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 27b096c8..7845879b 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -388,7 +388,8 @@ class LaserEVM: elif op == 'BYTE': s0, s1 = state.stack.pop(), state.stack.pop() - + if type(s1) is not ExprRef: + s1 = BitVecVal(s1, 256) try: n = helper.get_concrete_int(s0) oft = (31 - n) * 8 From 6410a0f538f0b2dc9c9cef9560758805a1e6bfb7 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sat, 16 Jun 2018 11:13:38 +0530 Subject: [PATCH 2/5] add native contracts --- mythril/laser/ethereum/helper.py | 30 ++++++ mythril/laser/ethereum/natives.py | 78 ++++++++++++++ mythril/laser/ethereum/svm.py | 59 +++++++---- tests/native_test.py | 117 +++++++++++++++++++++ tests/native_tests.sol | 166 ++++++++++++++++++++++++++++++ 5 files changed, 429 insertions(+), 21 deletions(-) create mode 100644 mythril/laser/ethereum/natives.py create mode 100644 tests/native_test.py create mode 100644 tests/native_tests.sol diff --git a/mythril/laser/ethereum/helper.py b/mythril/laser/ethereum/helper.py index dcbe17e3..32865fb8 100644 --- a/mythril/laser/ethereum/helper.py +++ b/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 + diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py new file mode 100644 index 00000000..98607165 --- /dev/null +++ b/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) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 27b096c8..ea03ef21 100644 --- a/mythril/laser/ethereum/svm.py +++ b/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 @@ -987,17 +987,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 - # Todo: Implement native contracts + 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 + + 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 +1066,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 +1178,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 diff --git a/tests/native_test.py b/tests/native_test.py new file mode 100644 index 00000000..b9239c30 --- /dev/null +++ b/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') + diff --git a/tests/native_tests.sol b/tests/native_tests.sol new file mode 100644 index 00000000..762d8443 --- /dev/null +++ b/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; + } + +} From 4c91fc2bcafdbdaf07023571e5f8032f5e11bb59 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sun, 17 Jun 2018 02:12:18 +0530 Subject: [PATCH 3/5] add type condition to jump --- mythril/laser/ethereum/svm.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index ea03ef21..d3a299d6 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -887,7 +887,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 +902,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 From e5a19c84df7d8160cac9437f3ba5ae3d604aca9b Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sun, 17 Jun 2018 14:48:45 +0200 Subject: [PATCH 4/5] Use isinstance --- mythril/laser/ethereum/svm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 7845879b..6e3da018 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -388,7 +388,7 @@ class LaserEVM: elif op == 'BYTE': s0, s1 = state.stack.pop(), state.stack.pop() - if type(s1) is not ExprRef: + if not isinstance(s1, ExprRef): s1 = BitVecVal(s1, 256) try: n = helper.get_concrete_int(s0) From fbfa16a1b56571fcf88a47820eaf3d6996c0214b Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Sun, 17 Jun 2018 21:04:44 +0700 Subject: [PATCH 5/5] Bump version number --- setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/setup.py b/setup.py index 523308fd..b4a0000d 100755 --- a/setup.py +++ b/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):