Merge branch 'master' into features/invalidjumpexception

6 years ago · 0e6b2d6d22
parent c950b30835 7b4fe769c8
commit 0e6b2d6d22
11 changed files with 150 additions and 95 deletions
--- a/6
+++ b/6
@ -5,6 +5,7 @@ COPY . /opt/mythril
 RUN apt-get update \
  && apt-get install -y \
     build-essential \
+     locales \
     python-pip-whl=9.0.1-2 \
     python3-pip=9.0.1-2 \
     python3-setuptools \
@ -22,4 +23,9 @@ RUN apt-get update \
  && pip3 install -r requirements.txt \
  && python setup.py install

+RUN locale-gen en_US.UTF-8
+ENV LANG en_US.UTF-8
+ENV LANGUAGE en_US.en
+ENV LC_ALL en_US.UTF-8
+
 ENTRYPOINT ["/usr/local/bin/myth"]
--- a/README.md
+++ b/README.md
@ -1,5 +1,5 @@
 # Mythril OSS [![Tweet](https://img.shields.io/twitter/url/http/shields.io.svg?style=social)](https://twitter.com/intent/tweet?text=Mythril%20-%20Security%20Analyzer%20for%20Ethereum%20Smart%20Contracts&url=https://www.github.com/ConsenSys/mythril)
-[![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/vwX58mr)
+[![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/E3YrVtG)
 [![PyPI](https://badge.fury.io/py/mythril.svg)](https://pypi.python.org/pypi/mythril)
 ![Master Build Status](https://img.shields.io/circleci/project/github/ConsenSys/mythril/master.svg)
 [![Waffle.io - Columns and their card count](https://badge.waffle.io/ConsenSys/mythril.svg?columns=all)](https://waffle.io/ConsenSys/mythril)
@ -9,7 +9,7 @@

 Mythril OSS is the classic security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. 

-Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/dFHQGrE) will serve your needs!
+Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs!

 Oh and by the way, we're now building a whole security tools ecosystem with [Mythril Platform API](https://mythril.ai). You should definitely check that out as well.

@ -33,7 +33,7 @@ See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup)

 Instructions for using the 'myth' tool are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). 

-For support or general discussions please join the Mythril community on [Discord](https://discord.gg/dFHQGrE).
+For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).

 ## Presentations, papers and videos

--- a/mythril/analysis/modules/multiple_sends.py
+++ b/mythril/analysis/modules/multiple_sends.py
@ -1,4 +1,5 @@
 from mythril.analysis.report import Issue
+from mythril.laser.ethereum.cfg import JumpType
 """
 MODULE DESCRIPTION:

@ -21,7 +22,7 @@ def execute(statespace):
            instruction = call.state.get_current_instruction()
            issue = Issue(node.contract_name, node.function_name, instruction['address'],
                          "Multiple Calls",
-                          "Information")
+                          "Informational")

            issue.description = \
                "Multiple sends exist in one transaction, try to isolate each external call into its own transaction." \
@ -50,7 +51,8 @@ def _explore_states(call, statespace):

 def _child_nodes(statespace, node):
    result = []
-    children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid]
+    children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid
+                and edge.type != JumpType.Transaction]

    for child in children:
        result.append(child)
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@ -22,16 +22,37 @@ TT256M1 = 2 ** 256 - 1
 keccak_function_manager = KeccakFunctionManager()


-def instruction(func):
-    """ Wrapper that handles copy and original return """
+class StateTransition(object):
+    """Decorator that handles global state copy and original return.

-    def wrapper(self, global_state):
-        global_state_copy = copy(global_state)
-        new_global_states = func(self, global_state_copy)
-        for state in new_global_states:
-            state.mstate.pc += 1
-        return new_global_states
-    return wrapper
+    This decorator calls the decorated instruction mutator function on a copy of the state that
+    is passed to it. After the call, the resulting new states' program counter is automatically
+    incremented if `increment_pc=True`.
+    """
+
+    def __init__(self, increment_pc=True):
+        self.increment_pc = increment_pc
+
+    @staticmethod
+    def call_on_state_copy(func, func_obj, state):
+        global_state_copy = copy(state)
+        return func(func_obj, global_state_copy)
+
+    def increment_states_pc(self, states):
+        if self.increment_pc:
+            for state in states:
+                state.mstate.pc += 1
+        return states
+
+    def __call__(self, func):
+        def wrapper(func_obj, global_state):
+            new_global_states = self.call_on_state_copy(
+                func,
+                func_obj,
+                global_state
+            )
+            return self.increment_states_pc(new_global_states)
+        return wrapper


 class Instruction:
@ -64,11 +85,11 @@ class Instruction:

        return instruction_mutator(global_state)

-    @instruction
+    @StateTransition()
    def jumpdest_(self, global_state):
        return [global_state]

-    @instruction
+    @StateTransition()
    def push_(self, global_state):
        push_instruction = global_state.get_current_instruction()
        push_value = push_instruction['argument'][2:]
@ -82,7 +103,7 @@ class Instruction:
        global_state.mstate.stack.append(BitVecVal(int(push_value, 16), 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def dup_(self, global_state):
        value = int(global_state.get_current_instruction()['opcode'][3:], 10)
        try:
@ -91,7 +112,7 @@ class Instruction:
            raise VmException('Trying to duplicate out of bounds stack elements')
        return [global_state]

-    @instruction
+    @StateTransition()
    def swap_(self, global_state):
        depth = int(self.op_code[4:])
        try:
@ -101,7 +122,7 @@ class Instruction:
            raise StackUnderflowException
        return [global_state]

-    @instruction
+    @StateTransition()
    def pop_(self, global_state):
        try:
            global_state.mstate.stack.pop()
@ -109,7 +130,7 @@ class Instruction:
            raise StackUnderflowException
        return [global_state]

-    @instruction
+    @StateTransition()
    def and_(self, global_state):
        try:
            stack = global_state.mstate.stack
@ -124,7 +145,7 @@ class Instruction:
            raise StackUnderflowException
        return [global_state]

-    @instruction
+    @StateTransition()
    def or_(self, global_state):
        stack = global_state.mstate.stack
        try:
@ -141,19 +162,19 @@ class Instruction:
            raise StackUnderflowException
        return [global_state]

-    @instruction
+    @StateTransition()
    def xor_(self, global_state):
        mstate = global_state.mstate
        mstate.stack.append(mstate.stack.pop() ^ mstate.stack.pop())
        return [global_state]

-    @instruction
+    @StateTransition()
    def not_(self, global_state: GlobalState):
        mstate = global_state.mstate
        mstate.stack.append(TT256M1 - mstate.stack.pop())
        return [global_state]

-    @instruction
+    @StateTransition()
    def byte_(self, global_state):
        mstate = global_state.mstate
        op0, op1 = mstate.stack.pop(), mstate.stack.pop()
@ -174,25 +195,25 @@ class Instruction:
        return [global_state]

    # Arithmetic
-    @instruction
+    @StateTransition()
    def add_(self, global_state):
        global_state.mstate.stack.append(
            (helper.pop_bitvec(global_state.mstate) + helper.pop_bitvec(global_state.mstate)))
        return [global_state]

-    @instruction
+    @StateTransition()
    def sub_(self, global_state):
        global_state.mstate.stack.append(
            (helper.pop_bitvec(global_state.mstate) - helper.pop_bitvec(global_state.mstate)))
        return [global_state]

-    @instruction
+    @StateTransition()
    def mul_(self, global_state):
        global_state.mstate.stack.append(
            (helper.pop_bitvec(global_state.mstate) * helper.pop_bitvec(global_state.mstate)))
        return [global_state]

-    @instruction
+    @StateTransition()
    def div_(self, global_state):
        op0, op1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
        if op1 == 0:
@ -201,7 +222,7 @@ class Instruction:
            global_state.mstate.stack.append(UDiv(op0, op1))
        return [global_state]

-    @instruction
+    @StateTransition()
    def sdiv_(self, global_state):
        s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
        if s1 == 0:
@ -210,33 +231,33 @@ class Instruction:
            global_state.mstate.stack.append(s0 / s1)
        return [global_state]

-    @instruction
+    @StateTransition()
    def mod_(self, global_state):
        s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
        global_state.mstate.stack.append(0 if s1 == 0 else URem(s0, s1))
        return [global_state]

-    @instruction
+    @StateTransition()
    def smod_(self, global_state):
        s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
        global_state.mstate.stack.append(0 if s1 == 0 else SRem(s0, s1))
        return [global_state]

-    @instruction
+    @StateTransition()
    def addmod_(self, global_state):
        s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec(
            global_state.mstate)
        global_state.mstate.stack.append(URem(URem(s0, s2) + URem(s1, s2), s2))
        return [global_state]

-    @instruction
+    @StateTransition()
    def mulmod_(self, global_state):
        s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec(
            global_state.mstate)
        global_state.mstate.stack.append(URem(URem(s0, s2) * URem(s1, s2), s2))
        return [global_state]

-    @instruction
+    @StateTransition()
    def exp_(self, global_state):
        state = global_state.mstate

@ -248,7 +269,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def signextend_(self, global_state):
        state = global_state.mstate
        s0, s1 = state.stack.pop(), state.stack.pop()
@ -272,28 +293,28 @@ class Instruction:
        return [global_state]

    # Comparisons
-    @instruction
+    @StateTransition()
    def lt_(self, global_state):
        state = global_state.mstate
        exp = ULT(util.pop_bitvec(state), util.pop_bitvec(state))
        state.stack.append(exp)
        return [global_state]

-    @instruction
+    @StateTransition()
    def gt_(self, global_state):
        state = global_state.mstate
        exp = UGT(util.pop_bitvec(state), util.pop_bitvec(state))
        state.stack.append(exp)
        return [global_state]

-    @instruction
+    @StateTransition()
    def slt_(self, global_state):
        state = global_state.mstate
        exp = util.pop_bitvec(state) < util.pop_bitvec(state)
        state.stack.append(exp)
        return [global_state]

-    @instruction
+    @StateTransition()
    def sgt_(self, global_state):
        state = global_state.mstate

@ -301,7 +322,7 @@ class Instruction:
        state.stack.append(exp)
        return [global_state]

-    @instruction
+    @StateTransition()
    def eq_(self, global_state):
        state = global_state.mstate

@ -319,7 +340,7 @@ class Instruction:
        state.stack.append(exp)
        return [global_state]

-    @instruction
+    @StateTransition()
    def iszero_(self, global_state):
        state = global_state.mstate

@ -330,7 +351,7 @@ class Instruction:
        return [global_state]

    # Call data
-    @instruction
+    @StateTransition()
    def callvalue_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
@ -338,7 +359,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def calldataload_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
@ -378,7 +399,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def calldatasize_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
@ -388,7 +409,7 @@ class Instruction:
            state.stack.append(BitVecVal(len(environment.calldata), 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def calldatacopy_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
@ -453,35 +474,35 @@ class Instruction:
        return [global_state]

    # Environment
-    @instruction
+    @StateTransition()
    def address_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
        state.stack.append(environment.address)
        return [global_state]

-    @instruction
+    @StateTransition()
    def balance_(self, global_state):
        state = global_state.mstate
        address = state.stack.pop()
        state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def origin_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
        state.stack.append(environment.origin)
        return [global_state]

-    @instruction
+    @StateTransition()
    def caller_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
        state.stack.append(environment.sender)
        return [global_state]

-    @instruction
+    @StateTransition()
    def codesize_(self, global_state):
        state = global_state.mstate
        environment = global_state.environment
@ -489,7 +510,7 @@ class Instruction:
        state.stack.append(len(disassembly.bytecode) // 2)
        return [global_state]

-    @instruction
+    @StateTransition()
    def sha3_(self, global_state):
        global keccak_function_manager

@ -526,12 +547,12 @@ class Instruction:
        state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccak, 0), 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def gasprice_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def codecopy_(self, global_state):
        memory_offset, code_offset, size = global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), global_state.mstate.stack.pop()

@ -580,7 +601,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def extcodesize_(self, global_state):
        state = global_state.mstate
        addr = state.stack.pop()
@ -606,7 +627,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def extcodecopy_(self, global_state):
        # FIXME: not implemented
        state = global_state.mstate
@ -614,45 +635,45 @@ class Instruction:
        start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop()
        return [global_state]

-    @instruction
+    @StateTransition()
    def returndatasize_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def blockhash_(self, global_state):
        state = global_state.mstate
        blocknumber = state.stack.pop()
        state.stack.append(global_state.new_bitvec("blockhash_block_" + str(blocknumber), 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def coinbase_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def timestamp_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def number_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def difficulty_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("block_difficulty", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def gaslimit_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("block_gaslimit", 256))
        return [global_state]

    # Memory operations
-    @instruction
+    @StateTransition()
    def mload_(self, global_state):
        state = global_state.mstate
        op0 = state.stack.pop()
@ -679,7 +700,7 @@ class Instruction:
        state.stack.append(data)
        return [global_state]

-    @instruction
+    @StateTransition()
    def mstore_(self, global_state):
        state = global_state.mstate
        try:
@ -717,7 +738,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def mstore8_(self, global_state):
        state = global_state.mstate
        op0, value = state.stack.pop(), state.stack.pop()
@ -733,7 +754,7 @@ class Instruction:
        state.memory[offset] = value % 256
        return [global_state]

-    @instruction
+    @StateTransition()
    def sload_(self, global_state):
        global keccak_function_manager
        
@ -786,6 +807,7 @@ class Instruction:
        global_state.mstate.stack.append(data)
        return [global_state]

+
    def _get_constraints(self, keccak_keys, this_key, argument):
        global keccak_function_manager
        for keccak_key in keccak_keys:
@ -794,7 +816,7 @@ class Instruction:
            keccak_argument = keccak_function_manager.get_argument(keccak_key)
            yield keccak_argument != argument

-    @instruction
+    @StateTransition()
    def sstore_(self, global_state):
        global keccak_function_manager
        state = global_state.mstate
@ -852,7 +874,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition(increment_pc=False)
    def jump_(self, global_state):
        state = global_state.mstate
        disassembly = global_state.environment.code
@ -878,7 +900,7 @@ class Instruction:

        return [new_state]

-    @instruction
+    @StateTransition(increment_pc=False)
    def jumpi_(self, global_state):
        state = global_state.mstate
        disassembly = global_state.environment.code
@ -891,6 +913,7 @@ class Instruction:
            # FIXME: to broad exception handler
        except:
            logging.debug("Skipping JUMPI to invalid destination.")
+            global_state.mstate.pc += 1
            return [global_state]

        # False case
@ -899,6 +922,7 @@ class Instruction:
        if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(negated)):
            new_state = copy(global_state)
            new_state.mstate.depth += 1
+            new_state.mstate.pc += 1
            new_state.mstate.constraints.append(negated)
            states.append(new_state)
        else:
@ -921,29 +945,27 @@ class Instruction:
                new_state.mstate.pc = index
                new_state.mstate.depth += 1
                new_state.mstate.constraints.append(condi)
-
                states.append(new_state)
            else:
                logging.debug("Pruned unreachable states.")
-
        return states

-    @instruction
+    @StateTransition()
    def pc_(self, global_state):
        global_state.mstate.stack.append(global_state.mstate.pc - 1)
        return [global_state]

-    @instruction
+    @StateTransition()
    def msize_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("msize", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def gas_(self, global_state):
        global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
        return [global_state]

-    @instruction
+    @StateTransition()
    def log_(self, global_state):
        # TODO: implement me
        state = global_state.mstate
@ -953,7 +975,7 @@ class Instruction:
        # Not supported
        return [global_state]

-    @instruction
+    @StateTransition()
    def create_(self, global_state):
        # TODO: implement me
        state = global_state.mstate
@ -962,7 +984,7 @@ class Instruction:
        state.stack.append(0)
        return [global_state]

-    @instruction
+    @StateTransition()
    def return_(self, global_state):
        state = global_state.mstate
        offset, length = state.stack.pop(), state.stack.pop()
@ -973,27 +995,42 @@ class Instruction:
            logging.debug("Return with symbolic length or offset. Not supported")
        global_state.current_transaction.end(global_state, return_data)

-    @instruction
+    @StateTransition()
    def suicide_(self, global_state):
-        return []
+        target = global_state.mstate.stack.pop()
+
+        # Often the target of the suicide instruction will be symbolic
+        # If it isn't then well transfer the balance to the indicated contract
+        if isinstance(target, BitVecNumRef):
+            target = '0x' + hex(target.as_long())[-40:]
+        if isinstance(target, str):
+            try:
+                global_state.world_state[target].balance += global_state.environment.active_account.balance
+            except KeyError:
+                global_state.world_state.create_account(address=target, balance=global_state.environment.active_account.balance)
+
+        global_state.environment.active_account.balance = 0
+        global_state.environment.active_account.deleted = True
+
+        global_state.current_transaction.end(global_state)

-    @instruction
+    @StateTransition()
    def revert_(self, global_state):
        return []

-    @instruction
+    @StateTransition()
    def assert_fail_(self, global_state):
        return []

-    @instruction
+    @StateTransition()
    def invalid_(self, global_state):
        return []

-    @instruction
+    @StateTransition()
    def stop_(self, global_state):
        global_state.current_transaction.end(global_state)

-    @instruction
+    @StateTransition()
    def call_(self, global_state):

        instr = global_state.get_current_instruction()
@ -1052,7 +1089,7 @@ class Instruction:
                                             call_data_type=call_data_type)
        raise TransactionStartSignal(transaction, self.op_code)

-    @instruction
+    @StateTransition()
    def call_post(self, global_state):
        instr = global_state.get_current_instruction()

@ -1093,7 +1130,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def callcode_(self, global_state):
        instr = global_state.get_current_instruction()
        environment = global_state.environment
@ -1120,7 +1157,7 @@ class Instruction:
                                             )
        raise TransactionStartSignal(transaction, self.op_code)

-    @instruction
+    @StateTransition()
    def callcode_post(self, global_state):
        instr = global_state.get_current_instruction()

@ -1162,7 +1199,7 @@ class Instruction:
        return [global_state]


-    @instruction
+    @StateTransition()
    def delegatecall_(self, global_state):
        instr = global_state.get_current_instruction()
        environment = global_state.environment
@ -1190,7 +1227,7 @@ class Instruction:
        raise TransactionStartSignal(transaction, self.op_code)


-    @instruction
+    @StateTransition()
    def delegatecall_post(self, global_state):
        instr = global_state.get_current_instruction()

@ -1234,7 +1271,7 @@ class Instruction:

        return [global_state]

-    @instruction
+    @StateTransition()
    def staticcall_(self, global_state):
        # TODO: implement me
        instr = global_state.get_current_instruction()
--- a/mythril/laser/ethereum/state.py
+++ b/mythril/laser/ethereum/state.py
@ -1,4 +1,5 @@
 from z3 import BitVec, BitVecVal, Solver, ExprRef, sat
+from mythril.disassembler.disassembly import Disassembly
 from copy import copy, deepcopy
 from enum import Enum
 from random import randint
@ -59,7 +60,7 @@ class Account:
        :param concrete_storage: Interpret storage as concrete
        """
        self.nonce = 0
-        self.code = code
+        self.code = code or Disassembly("")
        self.balance = balance if balance else BitVec("balance", 256)
        self.storage = Storage(concrete_storage, address=address, dynamic_loader=dynamic_loader)

@ -67,6 +68,8 @@ class Account:
        self.address = address
        self.contract_name = contract_name

+        self.deleted = False
+
    def __str__(self):
        return str(self.as_dict)

--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@ -223,7 +223,7 @@ class LaserEVM:
                    new_node.flags |= NodeFlags.FUNC_ENTRY
            except IndexError:
                new_node.flags |= NodeFlags.FUNC_ENTRY
-        address = state.environment.code.instruction_list[state.mstate.pc - 1]['address']
+        address = state.environment.code.instruction_list[state.mstate.pc]['address']

        environment = state.environment
        disassembly = environment.code
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@ -1,4 +1,5 @@
 from z3 import BitVec, Extract, Not
+from logging import debug

 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
@ -6,13 +7,16 @@ from mythril.laser.ethereum.state import CalldataType
 from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction,\
    get_next_transaction_id

-
 def execute_message_call(laser_evm, callee_address):
    """ Executes a message call transaction from all open states """
    open_states = laser_evm.open_states[:]
    del laser_evm.open_states[:]

    for open_world_state in open_states:
+        if open_world_state[callee_address].deleted:
+            debug("Can not execute dead contract, skipping.")
+            continue
+
        next_transaction_id = get_next_transaction_id()
        transaction = MessageCallTransaction(
            world_state=open_world_state,
--- a/requirements.txt
+++ b/requirements.txt
@ -8,6 +8,7 @@ eth-keyfile>=0.5.1
 eth-keys>=0.2.0b3
 eth-rlp>=0.1.0
 eth-tester>=0.1.0b21
+eth-typing<2.0.0,>=1.3.0
 eth-utils>=1.0.1
 jinja2>=2.9
 mock
--- a/setup.py
+++ b/setup.py
@ -95,6 +95,7 @@ setup(
        'eth-keys>=0.2.0b3',
        'eth-rlp>=0.1.0',
        'eth-tester>=0.1.0b21',
+        'eth-typing>=1.3.0,<2.0.0',
        'coverage',
        'jinja2>=2.9',
        'rlp>=1.0.1',
--- a/tests/laser/evm_testsuite/evm_test.py
+++ b/tests/laser/evm_testsuite/evm_test.py
@ -65,6 +65,7 @@ def test_vmtest(test_name: str, pre_condition: dict, action: dict, post_conditio
    )

    # Assert
+
    if 'Suicide' not in test_name and post_condition != {}:
        assert len(laser_evm.open_states) == 1
    else:
--- a/tests/laser/transaction/symbolic_test.py
+++ b/tests/laser/transaction/symbolic_test.py
@ -1,7 +1,7 @@
 from mythril.laser.ethereum.transaction.symbolic import execute_message_call, execute_contract_creation
 from mythril.laser.ethereum.transaction import MessageCallTransaction, ContractCreationTransaction
 from mythril.laser.ethereum.svm import LaserEVM
-from mythril.laser.ethereum.state import WorldState
+from mythril.laser.ethereum.state import WorldState, Account
 import unittest.mock as mock
 from unittest.mock import MagicMock

@ -20,7 +20,7 @@ def test_execute_message_call(mocked_setup: MagicMock):
    laser_evm = LaserEVM({})

    world_state = WorldState()
-    world_state.accounts["address"] = "something"
+    world_state.accounts["address"] = Account("address")

    laser_evm.open_states = [world_state]
    laser_evm.exec = MagicMock()