Add transaction sequence support

mythril/analysis/symbolic.py

@@ -2,6 +2,8 @@
 purposes."""
 
 import copy
+
+from ast import literal_eval
 from mythril.analysis.security import get_detection_module_hooks, get_detection_modules
 from mythril.laser.ethereum import svm
 from mythril.laser.ethereum.state.account import Account
@@ -38,6 +40,7 @@ class SymExecWrapper:
         modules=(),
         compulsory_statespace=True,
         enable_iprof=False,
+        transaction_sequences=None,
     ):
         """
 
@@ -73,6 +76,8 @@ class SymExecWrapper:
         )
         self.accounts = {address: account}
 
+        if transaction_sequences:
+            transaction_sequences = literal_eval(str(transaction_sequences))
         self.laser = svm.LaserEVM(
             self.accounts,
             dynamic_loader=dynloader,
@@ -83,6 +88,7 @@ class SymExecWrapper:
             transaction_count=transaction_count,
             requires_statespace=requires_statespace,
             enable_iprof=enable_iprof,
+            transaction_sequences=transaction_sequences,
         )
         mutation_plugin = MutationPruner()
 

mythril/interfaces/cli.py

@@ -213,6 +213,15 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
         default=2,
         help="Maximum number of transactions issued by laser",
     )
+    options.add_argument(
+        "--transaction-sequences",
+        type=str,
+        default=None,
+        help="The possible transaction sequences to be executed. "
+        "Like [[func_hash1, func_hash2], [func_hash2, func_hash3]] where for the first transaction is constrained "
+        "with func_hash1 and func_hash2, and the second tx is constrained with func_hash2 and func_hash3",
+    )
+
     options.add_argument(
         "--execution-timeout",
         type=int,
@@ -412,6 +421,7 @@ def execute_command(
         create_timeout=args.create_timeout,
         enable_iprof=args.enable_iprof,
         onchain_storage_access=not args.no_onchain_storage_access,
+        transaction_sequences=args.transaction_sequences,
     )
 
     if args.disassemble:

mythril/laser/ethereum/svm.py

@@ -55,6 +55,7 @@ class LaserEVM:
         transaction_count=2,
         requires_statespace=True,
         enable_iprof=False,
+        transaction_sequences=None,
     ) -> None:
         """
 
@@ -99,7 +100,7 @@ class LaserEVM:
         self._execute_state_hooks = []  # type: List[Callable]
         self._start_sym_exec_hooks = []  # type: List[Callable]
         self._stop_sym_exec_hooks = []  # type: List[Callable]
-
+        self.transaction_sequences = transaction_sequences
         self.iprof = InstructionProfiler() if enable_iprof else None
 
         log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
@@ -186,8 +187,14 @@ class LaserEVM:
                     i, len(self.open_states)
                 )
             )
-
-            execute_message_call(self, address)
+            func_hashes = (
+                self.transaction_sequences[i] if self.transaction_sequences else None
+            )
+            if func_hashes:
+                func_hashes = [
+                    bytes.fromhex(hex(func_hash)[2:]) for func_hash in func_hashes
+                ]
+            execute_message_call(self, address, function_hashes=func_hashes)
 
             end_coverage = self._get_covered_instructions()
 

mythril/laser/ethereum/transaction/symbolic.py

@@ -1,9 +1,9 @@
 """This module contains functions setting up and executing transactions with
 symbolic values."""
 import logging
+from typing import List
 
-
-from mythril.laser.smt import symbol_factory
+from mythril.laser.smt import symbol_factory, Or, Bool
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
@@ -20,7 +20,19 @@ CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
 ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 
 
-def execute_message_call(laser_evm, callee_address: str) -> None:
+def generate_function_constraints(calldata: SymbolicCalldata, func_hashes: List[int]):
+    constraints = []
+    for i in range(4):
+        constraint = Bool(False)
+        for func_hash in func_hashes:
+            constraint = Or(
+                constraint, calldata[i] == symbol_factory.BitVecVal(func_hash[i], 8)
+            )
+        constraints.append(constraint)
+    return constraints
+
+
+def execute_message_call(laser_evm, callee_address: str, function_hashes=None) -> None:
     """Executes a message call transaction from all open states.
 
     :param laser_evm:
@@ -36,6 +48,7 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
             continue
 
         next_transaction_id = get_next_transaction_id()
+        calldata = SymbolicCalldata(next_transaction_id)
         transaction = MessageCallTransaction(
             world_state=open_world_state,
             identifier=next_transaction_id,
@@ -48,12 +61,17 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
             ),
             caller=symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256),
             callee_account=open_world_state[callee_address],
-            call_data=SymbolicCalldata(next_transaction_id),
+            call_data=calldata,
             call_value=symbol_factory.BitVecSym(
                 "call_value{}".format(next_transaction_id), 256
             ),
         )
-        _setup_global_state_for_execution(laser_evm, transaction)
+        constraints = (
+            generate_function_constraints(calldata, function_hashes)
+            if function_hashes
+            else None
+        )
+        _setup_global_state_for_execution(laser_evm, transaction, constraints)
 
     laser_evm.exec()
 
@@ -104,7 +122,9 @@ def execute_contract_creation(
     return new_account
 
 
-def _setup_global_state_for_execution(laser_evm, transaction) -> None:
+def _setup_global_state_for_execution(
+    laser_evm, transaction, initial_constraints=None
+) -> None:
     """Sets up global state and cfg for a transactions execution.
 
     :param laser_evm:
@@ -113,7 +133,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
     # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
     global_state = transaction.initial_global_state()
     global_state.transaction_stack.append((transaction, None))
-
+    global_state.mstate.constraints += initial_constraints or []
     new_node = Node(
         global_state.environment.active_account.contract_name,
         function_name=global_state.environment.active_function_name,

mythril/mythril/mythril_analyzer.py

@@ -37,6 +37,7 @@ class MythrilAnalyzer:
         execution_timeout: Optional[int] = None,
         create_timeout: Optional[int] = None,
         enable_iprof: bool = False,
+        transaction_sequences=None,
     ):
         """
 
@@ -55,6 +56,7 @@ class MythrilAnalyzer:
         self.execution_timeout = execution_timeout
         self.create_timeout = create_timeout
         self.enable_iprof = enable_iprof
+        self.transaction_sequences = transaction_sequences
 
     def dump_statespace(self, contract: EVMContract = None) -> str:
         """
@@ -145,6 +147,7 @@ class MythrilAnalyzer:
                     modules=modules,
                     compulsory_statespace=False,
                     enable_iprof=self.enable_iprof,
+                    transaction_sequences=self.transaction_sequences,
                 )
                 issues = fire_lasers(sym, modules)
             except KeyboardInterrupt: