analysis.py

#!/usr/bin/env python

from mythril.ether.util import compile_solidity
from mythril.ether.ethcontract import ETHContract
from mythril.analysis.symbolic import StateSpace
from mythril.analysis import solver
from mythril.exceptions import UnsatError
from z3 import *


name, bytecode = compile_solidity(sys.argv[1])

contract = ETHContract(bytecode, name)
statespace = StateSpace([contract])


for node_id, node in statespace.nodes.items():

    for instr in node.instruction_list:

        # Find all states where Ib[μpc] == SSTORE

        if (instr['opcode'] == 'SSTORE'):

            # Obtain the top value from the stack. This may return a concrete or symbolic value

            sstore_target = node.states[instr['address']].stack[-1]

            '''
            Mythril symbolic variable naming conventions:

            - "caller" = msg.sender
            - "storage_0" = storage slot 0
            '''

            caller = BitVec("caller", 256)
            storage_0 = BitVec("storage_0", 256)

            # Construct the logical formula: P(σ) ^ σs[0] == 0 ^ Is  != σ[Ia]s[0]

            constr = node.constraints

            constr.append(sstore_target == 0)
            constr.append((UDiv(storage_0, 256)) & 0xffffffffffffffffffffffffffffffffffffffff != caller & 0xffffffffffffffffffffffffffffffffffffffff)

            try:
                model = solver.get_model(constr)

                print("Violation found! Function: " + node.function_name +", address: "  + str(instr['address']))

                for d in model.decls():
                    print("%s = 0x%x" % (d.name(), model[d].as_long()))

            except UnsatError:
                pass

print("Analysis completed.")