diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index bddd1727..d6802f0e 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -25,7 +25,7 @@ from mythril.laser.smt import ( Bool, Not, LShR, - BitVecFunc + BitVecFunc, ) from mythril.laser.smt import symbol_factory @@ -1373,6 +1373,8 @@ class Instruction: index = state.stack.pop() state.stack.append(global_state.environment.active_account.storage[index]) + if global_state.get_current_instruction()["address"] == 1054: + print(index, simplify(state.stack[-1]), simplify(state.stack[-2])) return [global_state] @StateTransition() @@ -1440,7 +1442,6 @@ class Instruction: states = [] op0, condition = state.stack.pop(), state.stack.pop() - try: jump_addr = util.get_concrete_int(op0) except TypeError: diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 5ab770e8..47860449 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -18,7 +18,7 @@ from mythril.laser.smt import ( BaseArray, Concat, And, - If + If, ) from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory @@ -282,7 +282,7 @@ class Storage: key.potential_values = [] i = 0 for val1, val2 in zip(concrete_vals, vals2): - if val2 and val1: + if val2[0] and val1[0]: c_val = Concat(val1[0], val2[0]) condition = And( models[i][1], BitVec(key.raw) == c_val, val1[1], val2[1] diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 1f675ca5..68ab3ccb 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -35,6 +35,7 @@ class Constraints(list): """ :return: True/False based on the existence of solution of constraints """ + return True if self._is_possible is not None: return self._is_possible solver = Solver() diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index e6d9d02d..beeb02d6 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -25,7 +25,15 @@ from mythril.laser.ethereum.transaction import ( execute_contract_creation, execute_message_call, ) -from mythril.laser.smt import symbol_factory, And, BitVecFunc, BitVec, Extract, simplify, is_true +from mythril.laser.smt import ( + symbol_factory, + And, + BitVecFunc, + BitVec, + Extract, + simplify, + is_true, +) ACTOR_ADDRESSES = [ symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256), @@ -391,14 +399,14 @@ class LaserEVM: and isinstance(key.input_, BitVec) and key.input_.symbolic and key.input_.size() == 512 + and key.input_.get_extracted_input_cond(511, 256) is False ): - pseudo_input = random.randint(0, 2 ** 256 - 1) + pseudo_input = random.randint(0, 2 ** 160 - 1) hex_v = hex(pseudo_input)[2:] if len(hex_v) % 2 == 1: hex_v += "0" hash_val = symbol_factory.BitVecVal( - int(sha3.keccak_256(bytes.fromhex(hex_v)).hexdigest()[2:], 16), - 256, + int(sha3.keccak_256(bytes.fromhex(hex_v)).hexdigest(), 16), 256 ) pseudo_input = symbol_factory.BitVecVal(pseudo_input, 256) calldata_cond = And( @@ -406,11 +414,11 @@ class LaserEVM: Extract(511, 256, key.input_) == hash_val, Extract(511, 256, key.input_).potential_input == pseudo_input, ) - Extract(511, 256, key.input_).potential_input_cond = calldata_cond - if not is_true(simplify(Extract(511, 256, key.input_).potential_input_cond != calldata_cond)): - print(key.input_, Extract(511, 256, key.input_).concat_args) - assert Extract(511, 256, key.input_).potential_input_cond == calldata_cond - print(Extract(511, 256, key.input_), calldata_cond, "CONDED") + key.input_.set_extracted_input_cond(511, 256, calldata_cond) + assert ( + key.input_.get_extracted_input_cond(511, 256) == calldata_cond + ) + for actor in ACTOR_ADDRESSES: try: models_tuple.append( diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index ef1a1f5b..f85c6785 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -33,15 +33,21 @@ class BitVec(Expression[z3.BitVecRef]): """ self.concat_args = concat_args or [] self.potential_values = [] - from random import randint if pot_input: - self.potential_input = BitVec(z3.BitVec("rn{}_input_".format(randint(0, 1000000)), 256), pot_input=False) + self.potential_input = BitVec(z3.BitVec(str(hash(raw))+"_input", 160), pot_input=False) self.potential_input_cond = True else: self.potential_input = None self.potential_input_cond = False + self.potential_input_dict = {} super().__init__(raw, annotations) + def set_extracted_input_cond(self, high, low, cond): + self.potential_input_dict[str("{}:{}".format(high, low))] = cond + + def get_extracted_input_cond(self, high, low): + return self.potential_input_dict.get(str("{}:{}".format(high, low)), False) + def size(self) -> int: """TODO: documentation diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py index 4b4b6cb6..353b6625 100644 --- a/mythril/laser/smt/bitvec_helper.py +++ b/mythril/laser/smt/bitvec_helper.py @@ -138,14 +138,19 @@ def concat_helper(bvs: List[BitVec]) -> List[BitVec]: new_bvs.append(prev_bv) prev_bv = copy(bv) continue - prev_bv.raw = z3.Concat(prev_bv.raw, bv.raw) + prev_bv.raw = z3.simplify(z3.Concat(prev_bv.raw, bv.raw)) prev_bv.low = bv.low # type: ignore if check_extracted_var(prev_bv) and hash(z3.simplify(prev_bv.raw)) == hash( prev_bv.parent # type: ignore ): prev_bv = prev_bv.parent # type: ignore new_bvs.append(prev_bv) - if len(new_bvs) == 1 and check_extracted_var(new_bvs[0]) and hash(z3.simplify(new_bvs[0].raw)) == hash(z3.simplify(new_bvs[0].parent.raw)): + if ( + len(new_bvs) == 1 + and check_extracted_var(new_bvs[0]) + and hash(z3.simplify(new_bvs[0].raw)) + == hash(z3.simplify(new_bvs[0].parent.raw)) + ): return new_bvs[0].parent return new_bvs @@ -251,9 +256,6 @@ def Extract(high: int, low: int, bv: BitVec) -> BitVec: ): val = val.parent # type: ignore assert val.size() == high - low + 1 - if val.size() == 256 and isinstance(val, BitVecFunc): - pass - #print(val, val.input_) return val input_string = "" bv.simplify() diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index 3120c952..811b3124 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -67,6 +67,7 @@ def _comparison_helper( if operation == z3.ULT: operation = operator.lt return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union) + potential_cond = True if ( a.size() == 512 and b.size() == 512 @@ -75,29 +76,32 @@ def _comparison_helper( ) ): from mythril.laser.smt.bitvec_helper import Extract + a = Extract(511, 256, a) + potential_cond = b.get_extracted_input_cond(511, 256) b = Extract(511, 256, b) - if not isinstance(b, BitVecFunc): - paddded_cond = True + if ( + not isinstance(b, BitVecFunc) + and b.symbolic + and a.input_ is not None + and a.input_.size() == 160 + ): + padded_cond = True if b.potential_input and b.potential_input.size() >= a.input_.size(): if b.potential_input.size() > a.input_.size(): - padded_a = z3.Concat( - z3.BitVecVal(0, b.potential_input.size() - a.input_.size()), - a.input_.raw, - ) + extracted_b = z3.Extract(a.input_.size() - 1, 0, b.potential_input.raw) else: - padded_a = a.input_.raw - paddded_cond = And(operation(padded_a, b.potential_input.raw), b.potential_input_cond) + extracted_b = b.potential_input.raw + padded_cond = And(operation(a.input_.raw, extracted_b), potential_cond) if a.potential_values: condition = False for value, cond in a.potential_values: if value is not None: condition = Or(condition, And(operation(b.raw, value.value), cond)) - ret = And(condition, operation(a.raw, b.raw), paddded_cond) - return ret - - return And(operation(a.raw, b.raw), paddded_cond) + ret = And(condition, operation(a.raw, b.raw), padded_cond) + return False + return And(operation(a.raw, b.raw), padded_cond) if ( not isinstance(b, BitVecFunc) or not a.func_name @@ -146,7 +150,8 @@ def _comparison_helper( ) if a.potential_values: for i, val in enumerate(a.potential_values): - comparision = Or(comparision, And(operation(val[0].raw, b.raw), val[1])) + if val[0]: + comparision = Or(comparision, And(operation(val[0].raw, b.raw), val[1])) comparision.simplify() return comparision @@ -171,9 +176,6 @@ class BitVecFunc(BitVec): :param input: The input to the functions :param annotations: The annotations the BitVecFunc should start with """ - if str(z3.simplify(input_.raw)) == "" and str(z3.simplify(raw)) == "KECCAC[invhash(1443016052)]": - import traceback - print(traceback.extract_stack(), z3.simplify(raw), z3.simplify(input_.raw)) self.func_name = func_name self.input_ = input_ diff --git a/tests/laser/smt/concat_extract_tests/concat_extract_assignment.py b/tests/laser/smt/concat_extract_tests/concat_extract_assignment.py index 92e9a215..88250728 100644 --- a/tests/laser/smt/concat_extract_tests/concat_extract_assignment.py +++ b/tests/laser/smt/concat_extract_tests/concat_extract_assignment.py @@ -13,6 +13,7 @@ def test_concat_extract_assignment(): assert Extract(511, 256, output).potential_input_cond == cond + def test_concat_extract_input_assignment(): inp1 = symbol_factory.BitVecSym("input1", 256) inp2 = symbol_factory.BitVecSym("input2", 256) @@ -26,7 +27,6 @@ def test_concat_extract_input_assignment(): assert Extract(511, 256, inp3).potential_input_cond == cond - def test_concat_extract_assignment_nested(): inp1 = symbol_factory.BitVecSym("input1", 256) o1 = symbol_factory.BitVecFuncSym( @@ -42,11 +42,14 @@ def test_concat_extract_assignment_nested(): input_=Concat(o1, symbol_factory.BitVecVal(0, 256)), ) cond = And(output1 == o1, inp1 == inp1) - Extract(511, 256, Extract(511, 256, output1.input_).input_).potential_input_cond = cond - - assert Extract( + Extract( 511, 256, Extract(511, 256, output1.input_).input_ - ).potential_input_cond == cond + ).potential_input_cond = cond + + assert ( + Extract(511, 256, Extract(511, 256, output1.input_).input_).potential_input_cond + == cond + ) def test_concat_extract_same_instance():