import json
import binascii
from datetime import datetime, timedelta
from typing import Dict, List, Any
from copy import deepcopy
from mythril.concolic.concrete_data import ConcreteData
from mythril.concolic.find_trace import concrete_execution
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.strategy.concolic import ConcolicStrategy
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.transaction.symbolic import execute_transaction
from mythril.laser.ethereum.transaction.transaction_models import tx_id_manager
from mythril.laser.smt import Expression, BitVec, symbol_factory
from mythril.laser.ethereum.time_handler import time_handler
from mythril.support.support_args import args
[docs]def flip_branches(
init_state: WorldState,
concrete_data: ConcreteData,
jump_addresses: List[str],
trace: List,
) -> List[Dict[str, Dict[str, Any]]]:
"""
Flips branches and prints the input required for branch flip
:param concrete_data: Concrete data
:param jump_addresses: Jump addresses to flip
:param trace: trace to follow
"""
tx_id_manager.restart_counter()
output_list = []
laser_evm = LaserEVM(
execution_timeout=600, use_reachability_check=False, transaction_count=10
)
laser_evm.open_states = [deepcopy(init_state)]
laser_evm.strategy = ConcolicStrategy(
work_list=laser_evm.work_list,
max_depth=100,
trace=trace,
flip_branch_addresses=jump_addresses,
)
time_handler.start_execution(laser_evm.execution_timeout)
laser_evm.time = datetime.now()
for transaction in concrete_data["steps"]:
execute_transaction(
laser_evm,
callee_address=transaction["address"],
caller_address=symbol_factory.BitVecVal(
int(transaction["origin"], 16), 256
),
data=transaction["input"][2:],
)
if laser_evm.strategy.results:
for addr in jump_addresses:
output_list.append(laser_evm.strategy.results[addr])
return output_list
[docs]def concolic_execution(
concrete_data: ConcreteData, jump_addresses: List, solver_timeout=100000
) -> List[Dict[str, Dict[str, Any]]]:
"""
Executes codes and prints input required to cover the branch flips
:param input_file: Input file
:param jump_addresses: Jump addresses to flip
:param solver_timeout: Solver timeout
"""
init_state, trace = concrete_execution(concrete_data)
args.solver_timeout = solver_timeout
output_list = flip_branches(
init_state=init_state,
concrete_data=concrete_data,
jump_addresses=jump_addresses,
trace=trace,
)
return output_list