Merge branch 'master' of github.com:ConsenSys/mythril

Dockerfile

@@ -1,7 +1,5 @@
 FROM ubuntu:bionic
 
-COPY . /opt/mythril
-
 RUN apt-get update \
   && apt-get install -y \
      build-essential \
@@ -18,8 +16,11 @@ RUN apt-get update \
      python3-dev \
      pandoc \
      git \
-  && ln -s /usr/bin/python3 /usr/local/bin/python \
-  && cd /opt/mythril \
+  && ln -s /usr/bin/python3 /usr/local/bin/python
+
+COPY . /opt/mythril
+
+RUN cd /opt/mythril \
   && pip3 install -r requirements.txt \
   && python setup.py install
 

mythril/analysis/modules/transaction_order_dependence.py

@@ -112,7 +112,7 @@ def _get_influencing_sstores(statespace, interesting_storages):
         index, value = sstore_state.mstate.stack[-1], sstore_state.mstate.stack[-2]
         try:
             index = util.get_concrete_int(index)
-        except AttributeError:
+        except TypeError:
             index = str(index)
         if "storage_{}".format(index) not in interesting_storages:
             continue

mythril/analysis/ops.py

@@ -21,7 +21,7 @@ class Variable:
 def get_variable(i):
     try:
         return Variable(util.get_concrete_int(i), VarType.CONCRETE)
-    except AttributeError:
+    except TypeError:
         return Variable(simplify(i), VarType.SYMBOLIC)
 
 

mythril/analysis/symbolic.py

@@ -14,7 +14,7 @@ class SymExecWrapper:
     """
 
     def __init__(self, contract, address, strategy, dynloader=None, max_depth=22,
-                 execution_timeout=None, create_timeout=None):
+                 execution_timeout=None, create_timeout=None, max_transaction_count=3):
 
         s_strategy = None
         if strategy == 'dfs':
@@ -30,7 +30,8 @@ class SymExecWrapper:
 
         self.laser = svm.LaserEVM(self.accounts, dynamic_loader=dynloader, max_depth=max_depth,
                                   execution_timeout=execution_timeout, strategy=s_strategy,
-                                  create_timeout=create_timeout)
+                                  create_timeout=create_timeout,
+                                  max_transaction_count=max_transaction_count)
 
         if isinstance(contract, SolidityContract):
             self.laser.sym_exec(creation_code=contract.creation_code, contract_name=contract.name)

mythril/disassembler/disassembly.py

@@ -20,10 +20,16 @@ class Disassembly(object):
 
         # Parse jump table & resolve function names
 
-        jmptable_indices = asm.find_opcode_sequence(["PUSH4", "EQ"], self.instruction_list)
+        # Need to take from PUSH1 to PUSH4 because solc seems to remove excess 0s at the beginning for optimizing
+        jmptable_indices = asm.find_opcode_sequence([("PUSH1", "PUSH2", "PUSH3", "PUSH4"), ("EQ",)],
+                                                    self.instruction_list)
 
         for i in jmptable_indices:
             func_hash = self.instruction_list[i]['argument']
+
+            # Append with missing 0s at the beginning
+            func_hash = "0x" + func_hash[2:].rjust(8, "0")
+
             self.func_hashes.append(func_hash)
             try:
                 # tries local cache, file and optional online lookup

mythril/ether/asm.py

@@ -70,13 +70,13 @@ def find_opcode_sequence(pattern, instruction_list):
 
     for i in range(0, len(instruction_list) - pattern_length + 1):
 
-        if instruction_list[i]['opcode'] == pattern[0]:
+        if instruction_list[i]['opcode'] in pattern[0]:
 
             matched = True
 
             for j in range(1, len(pattern)):
 
-                if not (instruction_list[i + j]['opcode'] == pattern[j]):
+                if not (instruction_list[i + j]['opcode'] in pattern[j]):
                     matched = False
                     break
 

mythril/interfaces/cli.py

@@ -69,6 +69,7 @@ def main():
     options = parser.add_argument_group('options')
     options.add_argument('-m', '--modules', help='Comma-separated list of security analysis modules', metavar='MODULES')
     options.add_argument('--max-depth', type=int, default=22, help='Maximum recursion depth for symbolic execution')
+    options.add_argument('--max-transaction-count', type=int, default=3, help='Maximum number of transactions issued by laser')
     options.add_argument('--strategy', choices=['dfs', 'bfs'], default='dfs', help='Symbolic execution strategy')
     options.add_argument('--execution-timeout', type=int, default=600, help="The amount of seconds to spend on symbolic execution")
     options.add_argument('--create-timeout', type=int, default=10, help="The amount of seconds to spend on "
@@ -218,7 +219,8 @@ def main():
                                              modules=[m.strip() for m in args.modules.strip().split(",")] if args.modules else [],
                                              verbose_report=args.verbose_report,
                                              max_depth=args.max_depth, execution_timeout=args.execution_timeout,
-                                             create_timeout=args.create_timeout)
+                                             create_timeout=args.create_timeout,
+                                             max_transaction_count=args.max_transaction_count)
                 outputs = {
                     'json': report.as_json(),
                     'text': report.as_text(),

mythril/laser/ethereum/call.py

@@ -48,7 +48,7 @@ def get_callee_address(global_state:GlobalState, dynamic_loader: DynLoader, symb
 
     try:
         callee_address = hex(util.get_concrete_int(symbolic_to_address))
-    except AttributeError:
+    except TypeError:
         logging.debug("Symbolic call encountered")
 
         match = re.search(r'storage_(\d+)', str(simplify(symbolic_to_address)))
@@ -63,6 +63,7 @@ def get_callee_address(global_state:GlobalState, dynamic_loader: DynLoader, symb
         # attempt to read the contract address from instance storage
         try:
             callee_address = dynamic_loader.read_storage(environment.active_account.address, index)
+        # TODO: verify whether this happens or not
         except:
             logging.debug("Error accessing contract storage.")
             raise ValueError
@@ -112,7 +113,6 @@ def get_callee_account(global_state, callee_address, dynamic_loader):
     return callee_account
 
 
-
 def get_call_data(global_state, memory_start, memory_size, pad=True):
     """
     Gets call_data from the global_state
@@ -130,7 +130,7 @@ def get_call_data(global_state, memory_start, memory_size, pad=True):
             call_data += [0] * (32 - len(call_data))
         call_data_type = CalldataType.CONCRETE
         logging.debug("Calldata: " + str(call_data))
-    except AttributeError:
+    except TypeError:
         logging.info("Unsupported symbolic calldata offset")
         call_data_type = CalldataType.SYMBOLIC
         call_data = []

mythril/laser/ethereum/instructions.py

@@ -175,7 +175,7 @@ class Instruction:
                 result = simplify(Concat(BitVecVal(0, 248), Extract(offset + 7, offset, op1)))
             else:
                 result = 0
-        except AttributeError:
+        except TypeError:
             logging.debug("BYTE: Unsupported symbolic byte offset")
             result = global_state.new_bitvec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
 
@@ -265,18 +265,17 @@ class Instruction:
         try:
             s0 = util.get_concrete_int(s0)
             s1 = util.get_concrete_int(s1)
+        except TypeError:
+            return []
 
-            if s0 <= 31:
-                testbit = s0 * 8 + 7
-                if s1 & (1 << testbit):
-                    state.stack.append(s1 | (TT256 - (1 << testbit)))
-                else:
-                    state.stack.append(s1 & ((1 << testbit) - 1))
+        if s0 <= 31:
+            testbit = s0 * 8 + 7
+            if s1 & (1 << testbit):
+                state.stack.append(s1 | (TT256 - (1 << testbit)))
             else:
-                state.stack.append(s1)
-            # TODO: broad exception handler
-        except:
-            return []
+                state.stack.append(s1 & ((1 << testbit) - 1))
+        else:
+            state.stack.append(s1)
 
         return [global_state]
 
@@ -356,7 +355,7 @@ class Instruction:
         try:
             offset = util.get_concrete_int(simplify(op0))
             b = environment.calldata[offset]
-        except AttributeError:
+        except TypeError:
             logging.debug("CALLDATALOAD: Unsupported symbolic index")
             state.stack.append(global_state.new_bitvec(
                 "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
@@ -368,16 +367,15 @@ class Instruction:
             return [global_state]
 
         if type(b) == int:
-            val = b''
 
             try:
-                for i in range(offset, offset + 32):
-                    val += environment.calldata[i].to_bytes(1, byteorder='big')
+                val = b''.join([calldata.to_bytes(1, byteorder='big') for calldata in
+                                environment.calldata[offset:offset+32]])
 
                 logging.debug("Final value: " + str(int.from_bytes(val, byteorder='big')))
                 state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256))
-            # FIXME: broad exception catch
-            except:
+
+            except (TypeError, AttributeError):
                 state.stack.append(global_state.new_bitvec(
                     "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
         else:
@@ -405,16 +403,14 @@ class Instruction:
 
         try:
             mstart = util.get_concrete_int(op0)
-            # FIXME: broad exception catch
-        except:
+        except TypeError:
             logging.debug("Unsupported symbolic memory offset in CALLDATACOPY")
             return [global_state]
 
         dstart_sym = False
         try:
             dstart = util.get_concrete_int(op1)
-            # FIXME: broad exception catch
-        except:
+        except TypeError:
             logging.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
             dstart = simplify(op1)
             dstart_sym = True
@@ -422,8 +418,7 @@ class Instruction:
         size_sym = False
         try:
             size = util.get_concrete_int(op2)
-            # FIXME: broad exception catch
-        except:
+        except TypeError:
             logging.debug("Unsupported symbolic size in CALLDATACOPY")
             size = simplify(op2)
             size_sym = True
@@ -438,8 +433,7 @@ class Instruction:
         if size > 0:
             try:
                 state.mem_extend(mstart, size)
-            # FIXME: broad exception catch
-            except:
+            except TypeError:
                 logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size))
                 state.mem_extend(mstart, 1)
                 state.memory[mstart] = global_state.new_bitvec(
@@ -453,7 +447,7 @@ class Instruction:
                 for i in range(mstart, mstart + size):
                     state.memory[i] = environment.calldata[i_data]
                     i_data += 1
-            except:
+            except IndexError:
                 logging.debug("Exception copying calldata to memory")
 
                 state.memory[mstart] = global_state.new_bitvec(
@@ -508,8 +502,7 @@ class Instruction:
 
         try:
             index, length = util.get_concrete_int(op0), util.get_concrete_int(op1)
-        # FIXME: broad exception catch
-        except:
+        except TypeError:
             # Can't access symbolic memory offsets
             if is_expr(op0):
                 op0 = simplify(op0)
@@ -521,7 +514,7 @@ class Instruction:
             data = b''.join([util.get_concrete_int(i).to_bytes(1, byteorder='big')
                              for i in state.memory[index: index + length]])
 
-        except AttributeError:
+        except TypeError:
             argument = str(state.memory[index]).replace(" ", "_")
 
             result = BitVec("KECCAC[{}]".format(argument), 256)
@@ -546,14 +539,14 @@ class Instruction:
 
         try:
             concrete_memory_offset = helper.get_concrete_int(memory_offset)
-        except AttributeError:
+        except TypeError:
             logging.debug("Unsupported symbolic memory offset in CODECOPY")
             return [global_state]
 
         try:
             concrete_size = helper.get_concrete_int(size)
             global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
-        except:
+        except TypeError:
             # except both attribute error and Exception
             global_state.mstate.mem_extend(concrete_memory_offset, 1)
             global_state.mstate.memory[concrete_memory_offset] = \
@@ -562,7 +555,7 @@ class Instruction:
 
         try:
             concrete_code_offset = helper.get_concrete_int(code_offset)
-        except AttributeError:
+        except TypeError:
             logging.debug("Unsupported symbolic code offset in CODECOPY")
             global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
             for i in range(concrete_size):
@@ -596,7 +589,7 @@ class Instruction:
         environment = global_state.environment
         try:
             addr = hex(helper.get_concrete_int(addr))
-        except AttributeError:
+        except TypeError:
             logging.info("unsupported symbolic address for EXTCODESIZE")
             state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
             return [global_state]
@@ -670,7 +663,7 @@ class Instruction:
 
         try:
             offset = util.get_concrete_int(op0)
-        except AttributeError:
+        except TypeError:
             logging.debug("Can't MLOAD from symbolic index")
             data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256)
             state.stack.append(data)
@@ -695,7 +688,7 @@ class Instruction:
 
         try:
             mstart = util.get_concrete_int(op0)
-        except AttributeError:
+        except TypeError:
             logging.debug("MSTORE to symbolic index. Not supported")
             return [global_state]
 
@@ -708,17 +701,15 @@ class Instruction:
 
         try:
             # Attempt to concretize value
+
             _bytes = util.concrete_int_to_bytes(value)
 
-            i = 0
+            state.memory[mstart:mstart+len(_bytes)] = _bytes
 
-            for b in _bytes:
-                state.memory[mstart + i] = _bytes[i]
-                i += 1
-        except:
+        except (AttributeError, TypeError):
             try:
                 state.memory[mstart] = value
-            except:
+            except TypeError:
                 logging.debug("Invalid memory access")
 
         return [global_state]
@@ -730,7 +721,7 @@ class Instruction:
 
         try:
             offset = util.get_concrete_int(op0)
-        except AttributeError:
+        except TypeError:
             logging.debug("MSTORE to symbolic index. Not supported")
             return [global_state]
 
@@ -751,7 +742,7 @@ class Instruction:
             index = util.get_concrete_int(index)
             return self._sload_helper(global_state, index)
 
-        except AttributeError:
+        except TypeError:
             if not keccak_function_manager.is_keccak(index):
                 return self._sload_helper(global_state, str(index))
 
@@ -813,7 +804,7 @@ class Instruction:
         try:
             index = util.get_concrete_int(index)
             return self._sstore_helper(global_state, index, value)
-        except AttributeError:
+        except TypeError:
             is_keccak = keccak_function_manager.is_keccak(index)
             if not is_keccak:
                 return self._sstore_helper(global_state, str(index), value)
@@ -867,7 +858,7 @@ class Instruction:
         disassembly = global_state.environment.code
         try:
             jump_addr = util.get_concrete_int(state.stack.pop())
-        except AttributeError:
+        except TypeError:
             raise InvalidJumpDestination("Invalid jump argument (symbolic address)")
         except IndexError:
             raise StackUnderflowException()
@@ -897,8 +888,7 @@ class Instruction:
 
         try:
             jump_addr = util.get_concrete_int(op0)
-            # FIXME: to broad exception handler
-        except:
+        except TypeError:
             logging.debug("Skipping JUMPI to invalid destination.")
             global_state.mstate.pc += 1
             return [global_state]
@@ -978,7 +968,7 @@ class Instruction:
         return_data = [global_state.new_bitvec("return_data", 256)]
         try:
             return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)]
-        except AttributeError:
+        except TypeError:
             logging.debug("Return with symbolic length or offset. Not supported")
         global_state.current_transaction.end(global_state, return_data)
 
@@ -1008,7 +998,7 @@ class Instruction:
         return_data = [global_state.new_bitvec("return_data", 256)]
         try:
             return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)]
-        except AttributeError:
+        except TypeError:
             logging.debug("Return with symbolic length or offset. Not supported")
         global_state.current_transaction.end(global_state, return_data=return_data, revert=True)
 
@@ -1052,7 +1042,7 @@ class Instruction:
             try:
                 mem_out_start = helper.get_concrete_int(memory_out_offset)
                 mem_out_sz = memory_out_size.as_long()
-            except AttributeError:
+            except TypeError:
                 logging.debug("CALL with symbolic start or offset not supported")
                 return [global_state]
 
@@ -1109,7 +1099,7 @@ class Instruction:
         try:
             memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset
             memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size
-        except AttributeError:
+        except TypeError:
             global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
@@ -1177,7 +1167,7 @@ class Instruction:
         try:
             memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset
             memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size
-        except AttributeError:
+        except TypeError:
             global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 
@@ -1249,7 +1239,7 @@ class Instruction:
                                                                                        ExprRef) else memory_out_offset
             memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size,
                                                                                    ExprRef) else memory_out_size
-        except AttributeError:
+        except TypeError:
             global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
             return [global_state]
 

mythril/laser/ethereum/svm.py

@@ -28,7 +28,7 @@ class LaserEVM:
     """
 
     def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, create_timeout=10,
-                 strategy=DepthFirstSearchStrategy):
+                 strategy=DepthFirstSearchStrategy, max_transaction_count=3):
         world_state = WorldState()
         world_state.accounts = accounts
         # this sets the initial world state
@@ -45,6 +45,7 @@ class LaserEVM:
         self.work_list = []
         self.strategy = strategy(self.work_list, max_depth)
         self.max_depth = max_depth
+        self.max_transaction_count = max_transaction_count
 
         self.execution_timeout = execution_timeout
         self.create_timeout = create_timeout
@@ -60,7 +61,7 @@ class LaserEVM:
     def accounts(self):
         return self.world_state.accounts
 
-    def sym_exec(self, main_address=None, creation_code=None, contract_name=None, max_transactions=3):
+    def sym_exec(self, main_address=None, creation_code=None, contract_name=None):
         logging.debug("Starting LASER execution")
         self.time = datetime.now()
 
@@ -77,7 +78,7 @@ class LaserEVM:
 
             # Reset code coverage
             self.coverage = {}
-            for i in range(max_transactions):
+            for i in range(self.max_transaction_count):
                 initial_coverage = self._get_covered_instructions()
 
                 self.time = datetime.now()

mythril/laser/ethereum/taint_analysis.py

@@ -213,7 +213,7 @@ class TaintRunner:
         _ = record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)
-        except AttributeError:
+        except TypeError:
             logging.debug("Can't MLOAD taint track symbolically")
             record.stack.append(False)
             return
@@ -225,7 +225,7 @@ class TaintRunner:
         _, value_taint = record.stack.pop(), record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)
-        except AttributeError:
+        except TypeError:
             logging.debug("Can't mstore taint track symbolically")
             return
 
@@ -236,7 +236,7 @@ class TaintRunner:
         _ = record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)
-        except AttributeError:
+        except TypeError:
             logging.debug("Can't MLOAD taint track symbolically")
             record.stack.append(False)
             return
@@ -248,7 +248,7 @@ class TaintRunner:
         _, value_taint = record.stack.pop(), record.stack.pop()
         try:
             index = helper.get_concrete_int(op0)
-        except AttributeError:
+        except TypeError:
             logging.debug("Can't mstore taint track symbolically")
             return
 

mythril/laser/ethereum/util.py

@@ -10,6 +10,8 @@ TT256M1 = 2 ** 256 - 1
 TT255 = 2 ** 255
 
 
+
+
 def sha3(seed):
     return _sha3.keccak_256(bytes(seed)).digest()
 
@@ -80,9 +82,12 @@ def get_concrete_int(item):
         elif is_true(simplified):
             return 1
         else:
-            raise ValueError("Symbolic boolref encountered")
+            raise TypeError("Symbolic boolref encountered")
 
-    return simplify(item).as_long()
+    try:
+        return simplify(item).as_long()
+    except AttributeError:
+        raise TypeError("Got a symbolic BitVecRef")
 
 
 def concrete_int_from_bytes(_bytes, start_index):

mythril/mythril.py

@@ -360,14 +360,16 @@ class Mythril(object):
         return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
 
     def fire_lasers(self, strategy, contracts=None, address=None,
-                    modules=None, verbose_report=False, max_depth=None, execution_timeout=None, create_timeout=None):
+                    modules=None, verbose_report=False, max_depth=None, execution_timeout=None, create_timeout=None,
+                    max_transaction_count=None):
 
         all_issues = []
         for contract in (contracts or self.contracts):
             sym = SymExecWrapper(contract, address, strategy,
                                  dynloader=DynLoader(self.eth) if self.dynld else None,
                                  max_depth=max_depth, execution_timeout=execution_timeout,
-                                 create_timeout=create_timeout)
+                                 create_timeout=create_timeout,
+                                 max_transaction_count=max_transaction_count)
 
             issues = fire_lasers(sym, modules)
 

mythril/support/truffle.py

@@ -40,7 +40,7 @@ def analyze_truffle_project(sigs, args):
             if len(bytecode) < 4:
                 continue
 
-            sigs.import_from_solidity_source(contractdata['sourcePath'])
+            sigs.import_from_solidity_source(contractdata['sourcePath'], solc_args=args.solc_args)
             sigs.write()
 
             ethcontract = ETHContract(bytecode, name=name)