diff --git a/.circleci/config.yml b/.circleci/config.yml index ae1a05d1..8926f5e6 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -108,6 +108,7 @@ jobs: -e CIRCLE_BUILD_NUM=$CIRCLE_BUILD_NUM \ -e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \ -e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \ + -e MONGO_URL=$MONGO_URL \ --rm edelweiss-mythril:latest \ --timeout 90 \ --output-dir /opt/edelweiss \ diff --git a/myth b/myth index 283f6bbb..0f6189c7 100755 --- a/myth +++ b/myth @@ -3,29 +3,11 @@ """mythril.py: Bug hunting on the Ethereum blockchain http://www.github.com/b-mueller/mythril """ -from sys import argv, exit -from mythril.interfaces.cli import COMMAND_LIST +from sys import exit import mythril.interfaces.cli -import mythril.interfaces.old_cli -import warnings -def format_Warning(message, category, filename, lineno, line=""): - return "Deprecation warning: {}\n\n".format(str(message)) - - -warnings.formatwarning = format_Warning - if __name__ == "__main__": - for arg in argv: - if arg in COMMAND_LIST: - mythril.interfaces.cli.main() - exit() - if "--help" in argv or "-h" in argv: - mythril.interfaces.cli.main() - exit() - - warnings.warn("The old cli arguments are deprecated, Please use 'myth -h' to view the new command line interface") - mythril.interfaces.old_cli.main() - + mythril.interfaces.cli.main() + exit() diff --git a/mythril/__version__.py b/mythril/__version__.py index 9085271a..feb9e24e 100644 --- a/mythril/__version__.py +++ b/mythril/__version__.py @@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well as for importing into Python. """ -__version__ = "v0.21.17" +__version__ = "v0.21.19" diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index e9229468..fa001b90 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -7,7 +7,7 @@ from mythril.analysis.potential_issues import ( PotentialIssue, ) from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT -from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) @@ -54,7 +54,7 @@ class DelegateCallModule(DetectionModule): to = state.mstate.stack[-2] constraints = [ - to == ATTACKER_ADDRESS, + to == ACTORS.attacker, UGT(gas, symbol_factory.BitVecVal(2300, 256)), state.new_bitvec( "retval_{}".format(state.get_current_instruction()["address"]), 256 @@ -64,7 +64,7 @@ class DelegateCallModule(DetectionModule): for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): - constraints.append(tx.caller == ATTACKER_ADDRESS) + constraints.append(tx.caller == ACTORS.attacker) try: address = state.get_current_instruction()["address"] diff --git a/mythril/analysis/modules/deprecated_ops.py b/mythril/analysis/modules/deprecated_ops.py index 85766537..0510dd8e 100644 --- a/mythril/analysis/modules/deprecated_ops.py +++ b/mythril/analysis/modules/deprecated_ops.py @@ -58,9 +58,7 @@ class DeprecatedOperationsModule(DetectionModule): "The smart contract retrieves the transaction origin (tx.origin) using msg.origin. " "Use of msg.origin is deprecated and the instruction may be removed in the future. " "Use msg.sender instead.\nSee also: " - "https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin".format( - state.environment.active_function_name - ) + "https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin" ) swc_id = DEPRECATED_FUNCTIONS_USAGE diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index 13066795..6a1e30cc 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -8,15 +8,12 @@ from mythril.analysis.potential_issues import ( get_potential_issues_annotation, PotentialIssue, ) -from mythril.laser.ethereum.transaction.symbolic import ( - ATTACKER_ADDRESS, - CREATOR_ADDRESS, -) +from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction import ContractCreationTransaction -from mythril.laser.smt import UGT, symbol_factory, UGE +from mythril.laser.smt import UGT, UGE log = logging.getLogger(__name__) @@ -93,9 +90,9 @@ class EtherThief(DetectionModule): This prevents false positives where the owner willingly transfers ownership to another address. """ if not isinstance(tx, ContractCreationTransaction): - constraints += [tx.caller != CREATOR_ADDRESS] + constraints += [tx.caller != ACTORS.creator] - attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256) + attacker_address_bitvec = ACTORS.attacker constraints += [ UGE( @@ -111,8 +108,8 @@ class EtherThief(DetectionModule): state.world_state.balances[attacker_address_bitvec], state.world_state.starting_balances[attacker_address_bitvec], ), - target == ATTACKER_ADDRESS, - state.current_transaction.caller == ATTACKER_ADDRESS, + target == ACTORS.attacker, + state.current_transaction.caller == ACTORS.attacker, ] potential_issue = PotentialIssue( diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index 804df576..1ac639eb 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -31,6 +31,8 @@ class ReachableExceptionsModule(DetectionModule): :param state: :return: """ + if state.get_current_instruction()["address"] in self.cache: + return issues = self._analyze_state(state) for issue in issues: self.cache.add(issue.address) @@ -55,11 +57,9 @@ class ReachableExceptionsModule(DetectionModule): "Note that explicit `assert()` should only be used to check invariants. " "Use `require()` for regular input checking." ) - transaction_sequence = solver.get_transaction_sequence( state, state.mstate.constraints ) - issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index 8a249a74..f227f7b2 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -8,7 +8,7 @@ from mythril.analysis.potential_issues import ( ) from mythril.analysis.swc_data import REENTRANCY from mythril.laser.ethereum.state.constraints import Constraints -from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) @@ -87,20 +87,20 @@ class ExternalCalls(DetectionModule): try: constraints = Constraints([UGT(gas, symbol_factory.BitVecVal(2300, 256))]) - transaction_sequence = solver.get_transaction_sequence( + solver.get_transaction_sequence( state, constraints + state.mstate.constraints ) # Check whether we can also set the callee address try: - constraints += [to == ATTACKER_ADDRESS] + constraints += [to == ACTORS.attacker] for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): - constraints.append(tx.caller == ATTACKER_ADDRESS) + constraints.append(tx.caller == ACTORS.attacker) - transaction_sequence = solver.get_transaction_sequence( + solver.get_transaction_sequence( state, constraints + state.mstate.constraints ) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 78d93f31..2879a331 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -343,7 +343,7 @@ def _get_address_from_state(state): def _get_overflowunderflow_state_annotation( - state: GlobalState + state: GlobalState, ) -> OverUnderflowStateAnnotation: state_annotations = cast( List[OverUnderflowStateAnnotation], diff --git a/mythril/analysis/modules/state_change_external_calls.py b/mythril/analysis/modules/state_change_external_calls.py index a05f4ffd..55b1d488 100644 --- a/mythril/analysis/modules/state_change_external_calls.py +++ b/mythril/analysis/modules/state_change_external_calls.py @@ -55,7 +55,7 @@ class StateChangeCallsAnnotation(StateAnnotation): constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF] try: - transaction_sequence = solver.get_transaction_sequence( + solver.get_transaction_sequence( global_state, constraints + global_state.mstate.constraints ) except UnsatError: diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index b55fcd3f..e3e77360 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -4,12 +4,12 @@ from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT from mythril.exceptions import UnsatError from mythril.analysis.modules.base import DetectionModule from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) import logging -import json + log = logging.getLogger(__name__) @@ -68,13 +68,12 @@ class SuicideModule(DetectionModule): for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): - constraints.append(tx.caller == ATTACKER_ADDRESS) - + constraints.append(tx.caller == ACTORS.attacker) try: try: transaction_sequence = solver.get_transaction_sequence( state, - state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS], + state.mstate.constraints + constraints + [to == ACTORS.attacker], ) description_tail = ( "Anyone can kill this contract and withdraw its balance to an arbitrary " @@ -85,7 +84,6 @@ class SuicideModule(DetectionModule): state, state.mstate.constraints + constraints ) description_tail = "Arbitrary senders can kill this contract." - issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 00de6bd4..1ac586e1 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -1,12 +1,16 @@ """This module contains analysis module helpers to solve path constraints.""" from functools import lru_cache -from typing import Dict, Tuple, Union +from typing import Dict, List, Tuple, Union from z3 import sat, unknown, FuncInterp import z3 from mythril.analysis.analysis_args import analysis_args from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints +from mythril.laser.ethereum.keccak_function_manager import ( + keccak_function_manager, + hash_matcher, +) from mythril.laser.ethereum.transaction import BaseTransaction from mythril.laser.smt import UGE, Optimize, symbol_factory from mythril.laser.ethereum.time_handler import time_handler @@ -18,6 +22,7 @@ import logging log = logging.getLogger(__name__) + # LRU cache works great when used in powers of 2 @lru_cache(maxsize=2 ** 23) def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True): @@ -48,7 +53,6 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True s.minimize(e) for e in maximize: s.maximize(e) - result = s.check() if result == sat: return s.model() @@ -97,7 +101,6 @@ def get_transaction_sequence( tx_constraints, minimize = _set_minimisation_constraints( transaction_sequence, constraints.copy(), [], 5000, global_state.world_state ) - try: model = get_model(tx_constraints, minimize=minimize) except UnsatError: @@ -122,12 +125,52 @@ def get_transaction_sequence( ).as_long() concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict) - + if isinstance(transaction_sequence[0], ContractCreationTransaction): + code = transaction_sequence[0].code + _replace_with_actual_sha(concrete_transactions, model, code) + else: + _replace_with_actual_sha(concrete_transactions, model) steps = {"initialState": concrete_initial_state, "steps": concrete_transactions} return steps +def _replace_with_actual_sha( + concrete_transactions: List[Dict[str, str]], model: z3.Model, code=None +): + concrete_hashes = keccak_function_manager.get_concrete_hash_data(model) + for tx in concrete_transactions: + if hash_matcher not in tx["input"]: + continue + if code is not None and code.bytecode in tx["input"]: + s_index = len(code.bytecode) + 2 + else: + s_index = 10 + for i in range(s_index, len(tx["input"])): + data_slice = tx["input"][i : i + 64] + if hash_matcher not in data_slice or len(data_slice) != 64: + continue + find_input = symbol_factory.BitVecVal(int(data_slice, 16), 256) + input_ = None + for size in concrete_hashes: + _, inverse = keccak_function_manager.store_function[size] + if find_input.value not in concrete_hashes[size]: + continue + input_ = symbol_factory.BitVecVal( + model.eval(inverse(find_input).raw).as_long(), size + ) + + if input_ is None: + continue + keccak = keccak_function_manager.find_concrete_keccak(input_) + hex_keccak = hex(keccak.value)[2:] + if len(hex_keccak) != 64: + hex_keccak = "0" * (64 - len(hex_keccak)) + hex_keccak + tx["input"] = tx["input"][:s_index] + tx["input"][s_index:].replace( + tx["input"][i : 64 + i], hex_keccak + ) + + def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): """ Gets a concrete state """ accounts = {} diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index d72578a5..ddded1b0 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -4,6 +4,7 @@ purposes.""" from mythril.analysis.security import get_detection_module_hooks, get_detection_modules from mythril.laser.ethereum import svm +from mythril.laser.ethereum.iprof import InstructionProfiler from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import ( @@ -15,10 +16,7 @@ from mythril.laser.ethereum.strategy.basic import ( ) from mythril.laser.ethereum.natives import PRECOMPILE_COUNT -from mythril.laser.ethereum.transaction.symbolic import ( - ATTACKER_ADDRESS, - CREATOR_ADDRESS, -) +from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory @@ -28,7 +26,7 @@ from mythril.laser.ethereum.strategy.extensions.bounded_loops import ( BoundedLoopsStrategy, ) from mythril.laser.smt import symbol_factory, BitVec -from typing import Union, List, Type +from typing import Union, List, Type, Optional from mythril.solidity.soliditycontract import EVMContract, SolidityContract from .ops import Call, VarType, get_variable @@ -44,32 +42,38 @@ class SymExecWrapper: self, contract, address: Union[int, str, BitVec], - strategy, + strategy: str, dynloader=None, - max_depth=22, - execution_timeout=None, - loop_bound=3, - create_timeout=None, - transaction_count=2, + max_depth: int = 22, + execution_timeout: Optional[int] = None, + loop_bound: int = 3, + create_timeout: Optional[int] = None, + transaction_count: int = 2, modules=(), - compulsory_statespace=True, - enable_iprof=False, - disable_dependency_pruning=False, - run_analysis_modules=True, - enable_coverage_strategy=False, - custom_modules_directory="", + compulsory_statespace: bool = True, + iprof: Optional[InstructionProfiler] = None, + disable_dependency_pruning: bool = False, + run_analysis_modules: bool = True, + enable_coverage_strategy: bool = False, + custom_modules_directory: str = "", ): """ - :param contract: - :param address: - :param strategy: - :param dynloader: - :param max_depth: - :param execution_timeout: - :param create_timeout: - :param transaction_count: - :param modules: + :param contract: Contract to symbolically execute + :param address: Address of the contract to symbolically execute + :param strategy: Execution strategy to use (bfs, dfs, etc) + :param dynloader: Dynamic Loader + :param max_depth: Max analysis depth + :param execution_timeout: Timeout for the entire analysis + :param create_timeout: Timeout for the creation transaction + :param transaction_count: Number of transactions to symbolically execute + :param modules: Analysis modules to run during analysis + :param compulsory_statespace: Boolean indicating whether or not the statespace should be saved + :param iprof: Instruction Profiler + :param disable_dependency_pruning: Boolean indicating whether dependency pruning should be disabled + :param run_analysis_modules: Boolean indicating whether analysis modules should be executed + :param enable_coverage_strategy: Boolean indicating whether the coverage strategy should be enabled + :param custom_modules_directory: The directory to read custom analysis modules from """ if isinstance(address, str): address = symbol_factory.BitVecVal(int(address, 16), 256) @@ -88,10 +92,10 @@ class SymExecWrapper: raise ValueError("Invalid strategy argument supplied") creator_account = Account( - hex(CREATOR_ADDRESS), "", dynamic_loader=dynloader, contract_name=None + hex(ACTORS.creator.value), "", dynamic_loader=dynloader, contract_name=None ) attacker_account = Account( - hex(ATTACKER_ADDRESS), "", dynamic_loader=dynloader, contract_name=None + hex(ACTORS.attacker.value), "", dynamic_loader=dynloader, contract_name=None ) requires_statespace = ( @@ -99,11 +103,11 @@ class SymExecWrapper: or len(get_detection_modules("post", modules, custom_modules_directory)) > 0 ) if not contract.creation_code: - self.accounts = {hex(ATTACKER_ADDRESS): attacker_account} + self.accounts = {hex(ACTORS.attacker.value): attacker_account} else: self.accounts = { - hex(CREATOR_ADDRESS): creator_account, - hex(ATTACKER_ADDRESS): attacker_account, + hex(ACTORS.creator.value): creator_account, + hex(ACTORS.attacker.value): attacker_account, } instruction_laser_plugin = PluginFactory.build_instruction_coverage_plugin() @@ -116,7 +120,7 @@ class SymExecWrapper: create_timeout=create_timeout, transaction_count=transaction_count, requires_statespace=requires_statespace, - enable_iprof=enable_iprof, + iprof=iprof, enable_coverage_strategy=enable_coverage_strategy, instruction_laser_plugin=instruction_laser_plugin, ) diff --git a/mythril/analysis/templates/report_as_markdown.jinja2 b/mythril/analysis/templates/report_as_markdown.jinja2 index 360648ea..59187b66 100644 --- a/mythril/analysis/templates/report_as_markdown.jinja2 +++ b/mythril/analysis/templates/report_as_markdown.jinja2 @@ -42,7 +42,7 @@ Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% {% for step in issue.tx_sequence.steps %} {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %} -Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }} +Caller: [CREATOR], data: [CONTRACT_CREATION], value: {{ step.value }} {% else %} Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }} {% endif %} diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2 index 1488807c..3ec34c69 100644 --- a/mythril/analysis/templates/report_as_text.jinja2 +++ b/mythril/analysis/templates/report_as_text.jinja2 @@ -33,7 +33,7 @@ Transaction Sequence: {% for step in issue.tx_sequence.steps %} {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %} -Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }} +Caller: [CREATOR], data: [CONTRACT_CREATION], value: {{ step.value }} {% else %} Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }} {% endif %} diff --git a/mythril/ethereum/interface/leveldb/client.py b/mythril/ethereum/interface/leveldb/client.py index 3373d3f1..c6289d1d 100644 --- a/mythril/ethereum/interface/leveldb/client.py +++ b/mythril/ethereum/interface/leveldb/client.py @@ -23,8 +23,8 @@ body_prefix = b"b" # body_prefix + num (uint64 big endian) + hash -> block body num_suffix = b"n" # header_prefix + num (uint64 big endian) + num_suffix -> hash block_hash_prefix = b"H" # block_hash_prefix + hash -> num (uint64 big endian) block_receipts_prefix = ( - b"r" -) # block_receipts_prefix + num (uint64 big endian) + hash -> block receipts + b"r" # block_receipts_prefix + num (uint64 big endian) + hash -> block receipts +) # known geth keys head_header_key = b"LastBlock" # head (latest) header hash # custom prefixes diff --git a/mythril/ethereum/util.py b/mythril/ethereum/util.py index 0fd72dcb..0ec4e645 100644 --- a/mythril/ethereum/util.py +++ b/mythril/ethereum/util.py @@ -2,8 +2,8 @@ solc integration.""" import binascii import json +import sys import os -import solcx from pathlib import Path from subprocess import PIPE, Popen @@ -12,6 +12,9 @@ from ethereum.utils import zpad from mythril.exceptions import CompilerError +if sys.version_info[1] >= 6: + import solcx + def safe_decode(hex_encoded_string): """ @@ -33,7 +36,7 @@ def get_solc_json(file, solc_binary="solc", solc_settings_json=None): :param solc_settings_json: :return: """ - cmd = [solc_binary, "--standard-json", "--allow-paths", "."] + cmd = [solc_binary, "--optimize", "--standard-json", "--allow-paths", "."] settings = json.loads(solc_settings_json) if solc_settings_json else {} settings.update( @@ -128,10 +131,9 @@ def solc_exists(version): "bin/solc", ) # py-solc setup ] - else: + elif sys.version_info[1] >= 6: # we are using solc-x for the the 0.5 and higher solc_binaries = [os.path.join(solcx.__path__[0], "bin", "solc-v" + version)] - for solc_path in solc_binaries: if os.path.exists(solc_path): return solc_path diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 1501120f..96731a10 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -18,6 +18,7 @@ import mythril.support.signatures as sigs from argparse import ArgumentParser, Namespace, RawTextHelpFormatter from mythril import mythx from mythril.exceptions import AddressNotFoundError, CriticalError +from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.mythril import ( MythrilAnalyzer, MythrilDisassembler, @@ -468,6 +469,16 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): help="designates a separate directory to search for custom analysis modules", metavar="CUSTOM_MODULES_DIRECTORY", ) + options.add_argument( + "--attacker-address", + help="Designates a specific attacker address to use during analysis", + metavar="ATTACKER_ADDRESS", + ) + options.add_argument( + "--creator-address", + help="Designates a specific creator address to use during analysis", + metavar="CREATOR_ADDRESS", + ) def validate_args(args: Namespace): @@ -662,6 +673,18 @@ def execute_command( args.outform, "input files do not contain any valid contracts" ) + if args.attacker_address: + try: + ACTORS["ATTACKER"] = args.attacker_address + except ValueError: + exit_with_error(args.outform, "Attacker address is invalid") + + if args.creator_address: + try: + ACTORS["CREATOR"] = args.creator_address + except ValueError: + exit_with_error(args.outform, "Creator address is invalid") + if args.graph: html = analyzer.graph_html( contract=analyzer.contracts[0], @@ -769,15 +792,6 @@ def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None: solc_settings_json=solc_json, enable_online_lookup=query_signature, ) - if args.command == "truffle": - try: - disassembler.analyze_truffle_project(args) - except FileNotFoundError: - print( - "Build directory not found. Make sure that you start the analysis from the project root, " - "and that 'truffle compile' has executed successfully." - ) - sys.exit() address = load_code(disassembler, args) execute_command( diff --git a/mythril/interfaces/old_cli.py b/mythril/interfaces/old_cli.py deleted file mode 100644 index 27bde387..00000000 --- a/mythril/interfaces/old_cli.py +++ /dev/null @@ -1,551 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- -"""mythril.py: Bug hunting on the Ethereum blockchain - - http://www.github.com/ConsenSys/mythril -""" - -import argparse -import json -import logging -import os -import sys - -import coloredlogs -import traceback - -import mythril.support.signatures as sigs -from mythril.exceptions import AddressNotFoundError, CriticalError -from mythril.mythril import ( - MythrilAnalyzer, - MythrilDisassembler, - MythrilConfig, - MythrilLevelDB, -) -from mythril.__version__ import __version__ as VERSION - -log = logging.getLogger(__name__) - - -def exit_with_error(format_, message): - """ - :param format_: - :param message: - """ - if format_ == "text" or format_ == "markdown": - log.error(message) - elif format_ == "json": - result = {"success": False, "error": str(message), "issues": []} - print(json.dumps(result)) - else: - result = [ - { - "issues": [], - "sourceType": "", - "sourceFormat": "", - "sourceList": [], - "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]}, - } - ] - print(json.dumps(result)) - sys.exit() - - -def main() -> None: - """The main CLI interface entry point.""" - parser = argparse.ArgumentParser( - description="Security analysis of Ethereum smart contracts" - ) - create_parser(parser) - - # Get config values - - args = parser.parse_args() - parse_args(parser=parser, args=args) - - -def create_parser(parser: argparse.ArgumentParser) -> None: - """ - Creates the parser by setting all the possible arguments - :param parser: The parser - """ - parser.add_argument("solidity_file", nargs="*") - - commands = parser.add_argument_group("commands") - commands.add_argument("-g", "--graph", help="generate a control flow graph") - commands.add_argument( - "-V", - "--version", - action="store_true", - help="print the Mythril version number and exit", - ) - commands.add_argument( - "-x", - "--fire-lasers", - action="store_true", - help="detect vulnerabilities, use with -c, -a or solidity file(s)", - ) - commands.add_argument( - "--truffle", - action="store_true", - help="analyze a truffle project (run from project dir)", - ) - commands.add_argument( - "-d", "--disassemble", action="store_true", help="print disassembly" - ) - commands.add_argument( - "-j", - "--statespace-json", - help="dumps the statespace json", - metavar="OUTPUT_FILE", - ) - - inputs = parser.add_argument_group("input arguments") - inputs.add_argument( - "-c", - "--code", - help='hex-encoded bytecode string ("6060604052...")', - metavar="BYTECODE", - ) - inputs.add_argument( - "-f", - "--codefile", - help="file containing hex-encoded bytecode string", - metavar="BYTECODEFILE", - type=argparse.FileType("r"), - ) - inputs.add_argument( - "-a", - "--address", - help="pull contract from the blockchain", - metavar="CONTRACT_ADDRESS", - ) - inputs.add_argument( - "-l", - "--dynld", - action="store_true", - help="auto-load dependencies from the blockchain", - ) - inputs.add_argument( - "--no-onchain-storage-access", - action="store_true", - help="turns off getting the data from onchain contracts", - ) - inputs.add_argument( - "--bin-runtime", - action="store_true", - help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.", - ) - - outputs = parser.add_argument_group("output formats") - outputs.add_argument( - "-o", - "--outform", - choices=["text", "markdown", "json", "jsonv2"], - default="text", - help="report output format", - metavar="", - ) - - database = parser.add_argument_group("local contracts database") - database.add_argument( - "-s", "--search", help="search the contract database", metavar="EXPRESSION" - ) - database.add_argument( - "--leveldb-dir", - help="specify leveldb directory for search or direct access operations", - metavar="LEVELDB_PATH", - ) - - utilities = parser.add_argument_group("utilities") - utilities.add_argument( - "--hash", help="calculate function signature hash", metavar="SIGNATURE" - ) - utilities.add_argument( - "--storage", - help="read state variables from storage index, use with -a", - metavar="INDEX,NUM_SLOTS,[array] / mapping,INDEX,[KEY1, KEY2...]", - ) - utilities.add_argument( - "--solv", - help="specify solidity compiler version. If not present, will try to install it (Experimental)", - metavar="SOLV", - ) - utilities.add_argument( - "--contract-hash-to-address", - help="returns corresponding address for a contract address hash", - metavar="SHA3_TO_LOOK_FOR", - ) - - 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=50, - help="Maximum recursion depth for symbolic execution", - ) - options.add_argument( - "--strategy", - choices=["dfs", "bfs", "naive-random", "weighted-random"], - default="bfs", - help="Symbolic execution strategy", - ) - options.add_argument( - "-b", - "--loop-bound", - type=int, - default=4, - help="Bound loops at n iterations", - metavar="N", - ) - options.add_argument( - "-t", - "--transaction-count", - type=int, - default=2, - help="Maximum number of transactions issued by laser", - ) - options.add_argument( - "--solver-timeout", - type=int, - default=10000, - help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules", - ) - options.add_argument( - "--execution-timeout", - type=int, - default=86400, - 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 " "the initial contract creation", - ) - options.add_argument( - "--solc-json", - help="Json for the optional 'settings' parameter of solc's standard-json input", - ) - options.add_argument( - "--phrack", action="store_true", help="Phrack-style call graph" - ) - options.add_argument( - "--enable-physics", action="store_true", help="enable graph physics simulation" - ) - options.add_argument( - "-v", type=int, help="log level (0-5)", metavar="LOG_LEVEL", default=2 - ) - options.add_argument( - "-q", - "--query-signature", - action="store_true", - help="Lookup function signatures through www.4byte.directory", - ) - options.add_argument( - "--enable-iprof", action="store_true", help="enable the instruction profiler" - ) - options.add_argument( - "--disable-dependency-pruning", - action="store_true", - help="Deactivate dependency-based pruning", - ) - - rpc = parser.add_argument_group("RPC options") - - rpc.add_argument( - "--rpc", - help="custom RPC settings", - metavar="HOST:PORT / ganache / infura-[network_name]", - default="infura-mainnet", - ) - rpc.add_argument( - "--rpctls", type=bool, default=False, help="RPC connection over TLS" - ) - parser.add_argument("--epic", action="store_true", help=argparse.SUPPRESS) - - -def validate_args(parser: argparse.ArgumentParser, args: argparse.Namespace): - if not ( - args.search - or args.hash - or args.disassemble - or args.graph - or args.fire_lasers - or args.storage - or args.truffle - or args.statespace_json - or args.contract_hash_to_address - ): - parser.print_help() - sys.exit() - - if args.v: - if 0 <= args.v < 6: - log_levels = [ - logging.NOTSET, - logging.CRITICAL, - logging.ERROR, - logging.WARNING, - logging.INFO, - logging.DEBUG, - ] - coloredlogs.install( - fmt="%(name)s [%(levelname)s]: %(message)s", level=log_levels[args.v] - ) - logging.getLogger("mythril").setLevel(log_levels[args.v]) - else: - exit_with_error( - args.outform, "Invalid -v value, you can find valid values in usage" - ) - - if args.query_signature: - if sigs.ethereum_input_decoder is None: - exit_with_error( - args.outform, - "The --query-signature function requires the python package ethereum-input-decoder", - ) - - if args.enable_iprof: - if args.v < 4: - exit_with_error( - args.outform, - "--enable-iprof must be used with -v LOG_LEVEL where LOG_LEVEL >= 4", - ) - elif not (args.graph or args.fire_lasers or args.statespace_json): - exit_with_error( - args.outform, - "--enable-iprof must be used with one of -g, --graph, -x, --fire-lasers, -j and --statespace-json", - ) - - -def quick_commands(args: argparse.Namespace): - if args.hash: - print(MythrilDisassembler.hash_for_function_signature(args.hash)) - sys.exit() - - -def set_config(args: argparse.Namespace): - config = MythrilConfig() - if args.dynld or not args.no_onchain_storage_access and not (args.rpc or args.i): - config.set_api_from_config_path() - - if args.address: - # Establish RPC connection if necessary - config.set_api_rpc(rpc=args.rpc, rpctls=args.rpctls) - elif args.search or args.contract_hash_to_address: - # Open LevelDB if necessary - config.set_api_leveldb( - config.leveldb_dir if not args.leveldb_dir else args.leveldb_dir - ) - return config - - -def leveldb_search(config: MythrilConfig, args: argparse.Namespace): - if args.search or args.contract_hash_to_address: - leveldb_searcher = MythrilLevelDB(config.eth_db) - if args.search: - # Database search ops - leveldb_searcher.search_db(args.search) - - else: - # search corresponding address - try: - leveldb_searcher.contract_hash_to_address(args.contract_hash_to_address) - except AddressNotFoundError: - print("Address not found.") - - sys.exit() - - -def get_code(disassembler: MythrilDisassembler, args: argparse.Namespace): - address = None - if args.code: - # Load from bytecode - code = args.code[2:] if args.code.startswith("0x") else args.code - address, _ = disassembler.load_from_bytecode(code, args.bin_runtime) - elif args.codefile: - bytecode = "".join([l.strip() for l in args.codefile if len(l.strip()) > 0]) - bytecode = bytecode[2:] if bytecode.startswith("0x") else bytecode - address, _ = disassembler.load_from_bytecode(bytecode, args.bin_runtime) - elif args.address: - # Get bytecode from a contract address - address, _ = disassembler.load_from_address(args.address) - elif args.solidity_file: - # Compile Solidity source file(s) - if args.graph and len(args.solidity_file) > 1: - exit_with_error( - args.outform, - "Cannot generate call graphs from multiple input files. Please do it one at a time.", - ) - address, _ = disassembler.load_from_solidity( - args.solidity_file - ) # list of files - else: - exit_with_error( - args.outform, - "No input bytecode. Please provide EVM code via -c BYTECODE, -a ADDRESS, or -i SOLIDITY_FILES", - ) - return address - - -def execute_command( - disassembler: MythrilDisassembler, - address: str, - parser: argparse.ArgumentParser, - args: argparse.Namespace, -): - - if args.storage: - if not args.address: - exit_with_error( - args.outform, - "To read storage, provide the address of a deployed contract with the -a option.", - ) - - storage = disassembler.get_state_variable_from_storage( - address=address, params=[a.strip() for a in args.storage.strip().split(",")] - ) - print(storage) - return - - analyzer = MythrilAnalyzer( - strategy=args.strategy, - disassembler=disassembler, - address=address, - max_depth=args.max_depth, - execution_timeout=args.execution_timeout, - loop_bound=args.loop_bound, - create_timeout=args.create_timeout, - enable_iprof=args.enable_iprof, - disable_dependency_pruning=args.disable_dependency_pruning, - onchain_storage_access=not args.no_onchain_storage_access, - solver_timeout=args.solver_timeout, - ) - - if args.disassemble: - # or mythril.disassemble(mythril.contracts[0]) - - if disassembler.contracts[0].code: - print("Runtime Disassembly: \n" + disassembler.contracts[0].get_easm()) - if disassembler.contracts[0].creation_code: - print("Disassembly: \n" + disassembler.contracts[0].get_creation_easm()) - - elif args.graph or args.fire_lasers: - if not disassembler.contracts: - exit_with_error( - args.outform, "input files do not contain any valid contracts" - ) - - if args.graph: - html = analyzer.graph_html( - contract=analyzer.contracts[0], - enable_physics=args.enable_physics, - phrackify=args.phrack, - transaction_count=args.transaction_count, - ) - - try: - with open(args.graph, "w") as f: - f.write(html) - except Exception as e: - exit_with_error(args.outform, "Error saving graph: " + str(e)) - - else: - try: - report = analyzer.fire_lasers( - modules=[m.strip() for m in args.modules.strip().split(",")] - if args.modules - else [], - transaction_count=args.transaction_count, - ) - outputs = { - "json": report.as_json(), - "jsonv2": report.as_swc_standard_format(), - "text": report.as_text(), - "markdown": report.as_markdown(), - } - print(outputs[args.outform]) - except ModuleNotFoundError as e: - exit_with_error( - args.outform, "Error loading analyis modules: " + format(e) - ) - - elif args.statespace_json: - - if not analyzer.contracts: - exit_with_error( - args.outform, "input files do not contain any valid contracts" - ) - - statespace = analyzer.dump_statespace(contract=analyzer.contracts[0]) - - try: - with open(args.statespace_json, "w") as f: - json.dump(statespace, f) - except Exception as e: - exit_with_error(args.outform, "Error saving json: " + str(e)) - - else: - parser.print_help() - - -def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> None: - """ - Parses the arguments - :param parser: The parser - :param args: The args - """ - - if args.epic: - path = os.path.dirname(os.path.realpath(__file__)) - sys.argv.remove("--epic") - os.system(" ".join(sys.argv) + " | python3 " + path + "/epic.py") - sys.exit() - - if args.version: - if args.outform == "json": - print(json.dumps({"version_str": VERSION})) - else: - print("Mythril version {}".format(VERSION)) - sys.exit() - - # Parse cmdline args - validate_args(parser, args) - try: - quick_commands(args) - config = set_config(args) - leveldb_search(config, args) - disassembler = MythrilDisassembler( - eth=config.eth, - solc_version=args.solv, - solc_settings_json=args.solc_json, - enable_online_lookup=args.query_signature, - ) - if args.truffle: - try: - disassembler.analyze_truffle_project(args) - except FileNotFoundError: - print( - "Build directory not found. Make sure that you start the analysis from the project root, and that 'truffle compile' has executed successfully." - ) - sys.exit() - - address = get_code(disassembler, args) - execute_command( - disassembler=disassembler, address=address, parser=parser, args=args - ) - except CriticalError as ce: - exit_with_error(args.outform, str(ce)) - except Exception: - exit_with_error(args.outform, traceback.format_exc()) - - -if __name__ == "__main__": - main() diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 24a8e2f3..5d0672c9 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -8,7 +8,7 @@ from typing import Union, List, cast, Callable, Optional import mythril.laser.ethereum.util as util from mythril.laser.ethereum import natives -from mythril.laser.ethereum.gas import OPCODE_GAS +from mythril.laser.ethereum.instruction_data import calculate_native_gas from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.natives import PRECOMPILE_COUNT from mythril.laser.ethereum.state.calldata import ( @@ -42,9 +42,12 @@ def get_call_parameters( """ gas, to = global_state.mstate.pop(2) value = global_state.mstate.pop() if with_value else 0 - memory_input_offset, memory_input_size, memory_out_offset, memory_out_size = global_state.mstate.pop( - 4 - ) + ( + memory_input_offset, + memory_input_size, + memory_out_offset, + memory_out_size, + ) = global_state.mstate.pop(4) callee_address = get_callee_address(global_state, dynamic_loader, to) @@ -213,7 +216,7 @@ def get_call_data( return ConcreteCalldata(transaction_id, calldata_from_mem) except TypeError: log.debug( - "Unsupported symbolic calldata offset %s size %s", memory_start, memory_size + "Unsupported symbolic memory offset %s size %s", memory_start, memory_size ) return SymbolicCalldata(transaction_id) @@ -242,7 +245,7 @@ def native_call( contract_list = ["ecrecover", "sha256", "ripemd160", "identity"] call_address_int = int(callee_address, 16) - native_gas_min, native_gas_max = cast(Callable, OPCODE_GAS["NATIVE_COST"])( + native_gas_min, native_gas_max = calculate_native_gas( global_state.mstate.calculate_extension_size(mem_out_start, mem_out_sz), contract_list[call_address_int - 1], ) diff --git a/mythril/laser/ethereum/cfg.py b/mythril/laser/ethereum/cfg.py index ddf181cc..c62f8857 100644 --- a/mythril/laser/ethereum/cfg.py +++ b/mythril/laser/ethereum/cfg.py @@ -3,7 +3,6 @@ from enum import Enum from typing import Dict, List, TYPE_CHECKING from mythril.laser.ethereum.state.constraints import Constraints - from flags import Flags if TYPE_CHECKING: diff --git a/mythril/laser/ethereum/evm_exceptions.py b/mythril/laser/ethereum/evm_exceptions.py index 7e2a7b8f..647c52e4 100644 --- a/mythril/laser/ethereum/evm_exceptions.py +++ b/mythril/laser/ethereum/evm_exceptions.py @@ -41,9 +41,3 @@ class WriteProtection(VmException): """A VM exception denoting that a write operation is executed on a write protected environment""" pass - - -class ProgramCounterException(VmException): - """A VM exception denoting an invalid PC value (No stop instruction is reached).""" - - pass diff --git a/mythril/laser/ethereum/gas.py b/mythril/laser/ethereum/gas.py deleted file mode 100644 index 0a0c0a38..00000000 --- a/mythril/laser/ethereum/gas.py +++ /dev/null @@ -1,194 +0,0 @@ -"""This module contains functions for dynamic gas calculation and a gas cost -table.""" -from ethereum import opcodes -from ethereum.utils import ceil32 -from typing import Callable, Dict, Tuple, Union - - -def calculate_native_gas(size: int, contract: str): - """ - - :param size: - :param contract: - :return: - """ - gas_value = None - word_num = ceil32(size) // 32 - if contract == "ecrecover": - gas_value = opcodes.GECRECOVER - elif contract == "sha256": - gas_value = opcodes.GSHA256BASE + word_num * opcodes.GSHA256WORD - elif contract == "ripemd160": - gas_value = opcodes.GRIPEMD160BASE + word_num * opcodes.GRIPEMD160WORD - elif contract == "identity": - gas_value = opcodes.GIDENTITYBASE + word_num * opcodes.GIDENTITYWORD - else: - raise ValueError("Unknown contract type {}".format(contract)) - return gas_value, gas_value - - -def calculate_sha3_gas(length: int): - """ - - :param length: - :return: - """ - gas_val = 30 + opcodes.GSHA3WORD * (ceil32(length) // 32) - return gas_val, gas_val - - -# opcode -> (min_gas, max_gas) -OPCODE_GAS = { - "STOP": (0, 0), - "ADD": (3, 3), - "MUL": (5, 5), - "SUB": (3, 3), - "DIV": (5, 5), - "SDIV": (5, 5), - "MOD": (5, 5), - "SMOD": (5, 5), - "ADDMOD": (8, 8), - "MULMOD": (8, 8), - "EXP": (10, 340), # exponent max 2^32 - "SIGNEXTEND": (5, 5), - "LT": (3, 3), - "GT": (3, 3), - "SLT": (3, 3), - "SGT": (3, 3), - "EQ": (3, 3), - "ISZERO": (3, 3), - "AND": (3, 3), - "OR": (3, 3), - "XOR": (3, 3), - "NOT": (3, 3), - "BYTE": (3, 3), - "SHL": (3, 3), - "SHR": (3, 3), - "SAR": (3, 3), - "SHA3": ( - 30, - 30 + 6 * 8, - ), # max can be larger, but usually storage location with 8 words - "SHA3_FUNC": calculate_sha3_gas, - "ADDRESS": (2, 2), - "BALANCE": (400, 400), - "ORIGIN": (2, 2), - "CALLER": (2, 2), - "CALLVALUE": (2, 2), - "CALLDATALOAD": (3, 3), - "CALLDATASIZE": (2, 2), - "CALLDATACOPY": (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556 - "CODESIZE": (2, 2), - "CODECOPY": (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556, - "GASPRICE": (2, 2), - "EXTCODESIZE": (700, 700), - "EXTCODECOPY": (700, 700 + 3 * 768), # https://ethereum.stackexchange.com/a/47556 - "EXTCODEHASH": (400, 400), - "RETURNDATASIZE": (2, 2), - "RETURNDATACOPY": (3, 3), - "BLOCKHASH": (20, 20), - "COINBASE": (2, 2), - "TIMESTAMP": (2, 2), - "NUMBER": (2, 2), - "DIFFICULTY": (2, 2), - "GASLIMIT": (2, 2), - "POP": (2, 2), - # assume 1KB memory r/w cost as upper bound - "MLOAD": (3, 96), - "MSTORE": (3, 98), - "MSTORE8": (3, 98), - # assume 64 byte r/w cost as upper bound - "SLOAD": (400, 400), - "SSTORE": (5000, 25000), - "JUMP": (8, 8), - "JUMPI": (10, 10), - "PC": (2, 2), - "MSIZE": (2, 2), - "GAS": (2, 2), - "JUMPDEST": (1, 1), - "PUSH1": (3, 3), - "PUSH2": (3, 3), - "PUSH3": (3, 3), - "PUSH4": (3, 3), - "PUSH5": (3, 3), - "PUSH6": (3, 3), - "PUSH7": (3, 3), - "PUSH8": (3, 3), - "PUSH9": (3, 3), - "PUSH10": (3, 3), - "PUSH11": (3, 3), - "PUSH12": (3, 3), - "PUSH13": (3, 3), - "PUSH14": (3, 3), - "PUSH15": (3, 3), - "PUSH16": (3, 3), - "PUSH17": (3, 3), - "PUSH18": (3, 3), - "PUSH19": (3, 3), - "PUSH20": (3, 3), - "PUSH21": (3, 3), - "PUSH22": (3, 3), - "PUSH23": (3, 3), - "PUSH24": (3, 3), - "PUSH25": (3, 3), - "PUSH26": (3, 3), - "PUSH27": (3, 3), - "PUSH28": (3, 3), - "PUSH29": (3, 3), - "PUSH30": (3, 3), - "PUSH31": (3, 3), - "PUSH32": (3, 3), - "DUP1": (3, 3), - "DUP2": (3, 3), - "DUP3": (3, 3), - "DUP4": (3, 3), - "DUP5": (3, 3), - "DUP6": (3, 3), - "DUP7": (3, 3), - "DUP8": (3, 3), - "DUP9": (3, 3), - "DUP10": (3, 3), - "DUP11": (3, 3), - "DUP12": (3, 3), - "DUP13": (3, 3), - "DUP14": (3, 3), - "DUP15": (3, 3), - "DUP16": (3, 3), - "SWAP1": (3, 3), - "SWAP2": (3, 3), - "SWAP3": (3, 3), - "SWAP4": (3, 3), - "SWAP5": (3, 3), - "SWAP6": (3, 3), - "SWAP7": (3, 3), - "SWAP8": (3, 3), - "SWAP9": (3, 3), - "SWAP10": (3, 3), - "SWAP11": (3, 3), - "SWAP12": (3, 3), - "SWAP13": (3, 3), - "SWAP14": (3, 3), - "SWAP15": (3, 3), - "SWAP16": (3, 3), - # apparently Solidity only allows byte32 as input to the log - # function. Virtually it could be as large as the block gas limit - # allows, but let's stick to the reasonable standard here. - # https://ethereum.stackexchange.com/a/1691 - "LOG0": (375, 375 + 8 * 32), - "LOG1": (2 * 375, 2 * 375 + 8 * 32), - "LOG2": (3 * 375, 3 * 375 + 8 * 32), - "LOG3": (4 * 375, 4 * 375 + 8 * 32), - "LOG4": (5 * 375, 5 * 375 + 8 * 32), - "CREATE": (32000, 32000), - "CREATE2": (32000, 32000), # TODO: Make the gas values dynamic - "CALL": (700, 700 + 9000 + 25000), - "NATIVE_COST": calculate_native_gas, - "CALLCODE": (700, 700 + 9000 + 25000), - "RETURN": (0, 0), - "DELEGATECALL": (700, 700 + 9000 + 25000), - "STATICCALL": (700, 700 + 9000 + 25000), - "REVERT": (0, 0), - "SUICIDE": (5000, 30000), - "ASSERT_FAIL": (0, 0), - "INVALID": (0, 0), -} # type: Dict[str, Union[Tuple[int, int], Callable]] diff --git a/mythril/laser/ethereum/instruction_data.py b/mythril/laser/ethereum/instruction_data.py new file mode 100644 index 00000000..127e33c8 --- /dev/null +++ b/mythril/laser/ethereum/instruction_data.py @@ -0,0 +1,222 @@ +from ethereum import opcodes +from ethereum.utils import ceil32 +from typing import Callable, Dict, Tuple, Union + + +Z_OPERATOR_TUPLE = (0, 1) +UN_OPERATOR_TUPLE = (1, 1) +BIN_OPERATOR_TUPLE = (2, 1) +T_OPERATOR_TUPLE = (3, 1) +GAS = "gas" +STACK = "stack" + +# Gas tuple contains (min_gas, max_gas) +# stack tuple contains (no_of_elements_popped, no_of_elements_pushed) + +OPCODES = { + "STOP": {GAS: (0, 0), STACK: (0, 0)}, + "ADD": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "MUL": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE}, + "SUB": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "DIV": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE}, + "SDIV": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE}, + "MOD": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE}, + "SMOD": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE}, + "ADDMOD": {GAS: (8, 8), STACK: BIN_OPERATOR_TUPLE}, + "MULMOD": {GAS: (8, 8), STACK: T_OPERATOR_TUPLE}, + "EXP": {GAS: (10, 340), STACK: BIN_OPERATOR_TUPLE}, # exponent max 2^32 + "SIGNEXTEND": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE}, + "LT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "GT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "SLT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "SGT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "EQ": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "AND": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "ISZERO": {GAS: (3, 3), STACK: UN_OPERATOR_TUPLE}, + "OR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "XOR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "NOT": {GAS: (3, 3), STACK: UN_OPERATOR_TUPLE}, + "BYTE": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "SHL": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "SHR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "SAR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE}, + "SHA3": { + GAS: ( + 30, + 30 + 6 * 8, + ), # max can be larger, but usually storage location with 8 words + STACK: BIN_OPERATOR_TUPLE, + }, + "ADDRESS": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "BALANCE": {GAS: (400, 400), STACK: UN_OPERATOR_TUPLE}, + "ORIGIN": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "CALLER": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "CALLVALUE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "CALLDATALOAD": {GAS: (3, 3), STACK: UN_OPERATOR_TUPLE}, + "CALLDATASIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "CALLDATACOPY": { + GAS: (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556 + STACK: (3, 0), + }, + "CODESIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "CODECOPY": { + GAS: (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556, + STACK: (3, 0), + }, + "GASPRICE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "EXTCODESIZE": {GAS: (700, 700), STACK: Z_OPERATOR_TUPLE}, + "EXTCODECOPY": { + GAS: (700, 700 + 3 * 768), # https://ethereum.stackexchange.com/a/47556 + STACK: (4, 0), + }, + "EXTCODEHASH": {GAS: (400, 400), STACK: UN_OPERATOR_TUPLE}, + "RETURNDATASIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "RETURNDATACOPY": {GAS: (3, 3), STACK: (3, 0)}, + "BLOCKHASH": {GAS: (20, 20), STACK: UN_OPERATOR_TUPLE}, + "COINBASE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "TIMESTAMP": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "NUMBER": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "DIFFICULTY": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "GASLIMIT": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "POP": {GAS: (2, 2), STACK: (1, 0)}, + # assume 1KB memory r/w cost as upper bound + "MLOAD": {GAS: (3, 96), STACK: UN_OPERATOR_TUPLE}, + "MSTORE": {GAS: (3, 98), STACK: (2, 0)}, + "MSTORE8": {GAS: (3, 98), STACK: (2, 0)}, + # assume 64 byte r/w cost as upper bound + "SLOAD": {GAS: (400, 400), STACK: UN_OPERATOR_TUPLE}, + "SSTORE": {GAS: (5000, 25000), STACK: (1, 0)}, + "JUMP": {GAS: (8, 8), STACK: (1, 0)}, + "JUMPI": {GAS: (10, 10), STACK: (2, 0)}, + "PC": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "MSIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "GAS": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE}, + "JUMPDEST": {GAS: (1, 1), STACK: (0, 0)}, + "PUSH1": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH2": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH3": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH4": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH5": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH6": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH7": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH8": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH9": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH10": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH11": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH12": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH13": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH14": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH15": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH16": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH17": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH18": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH19": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH20": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH21": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH22": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH23": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH24": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH25": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH26": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH27": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH28": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH29": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH30": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH31": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "PUSH32": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP1": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP2": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP3": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP4": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP5": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP6": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP7": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP8": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP9": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP10": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP11": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP12": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP13": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP14": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP15": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "DUP16": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE}, + "SWAP1": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP2": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP3": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP4": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP5": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP6": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP7": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP8": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP9": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP10": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP11": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP12": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP13": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP14": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP15": {GAS: (3, 3), STACK: (0, 0)}, + "SWAP16": {GAS: (3, 3), STACK: (0, 0)}, + # apparently Solidity only allows byte32 as input to the log + # function. Virtually it could be as large as the block gas limit + # allows, but let's stick to the reasonable standard here. + # https://ethereum.stackexchange.com/a/1691 + "LOG0": {GAS: (375, 375 + 8 * 32), STACK: (2, 0)}, + "LOG1": {GAS: (2 * 375, 2 * 375 + 8 * 32), STACK: (3, 0)}, + "LOG2": {GAS: (3 * 375, 3 * 375 + 8 * 32), STACK: (4, 0)}, + "LOG3": {GAS: (4 * 375, 4 * 375 + 8 * 32), STACK: (5, 0)}, + "LOG4": {GAS: (5 * 375, 5 * 375 + 8 * 32), STACK: (6, 0)}, + "CREATE": {GAS: (32000, 32000), STACK: T_OPERATOR_TUPLE}, + "CREATE2": { + GAS: (32000, 32000), # TODO: Make the gas values dynamic + STACK: (4, 1), + }, + "CALL": {GAS: (700, 700 + 9000 + 25000), STACK: (7, 1)}, + "CALLCODE": {GAS: (700, 700 + 9000 + 25000), STACK: (7, 1)}, + "RETURN": {GAS: (0, 0), STACK: (2, 0)}, + "DELEGATECALL": {GAS: (700, 700 + 9000 + 25000), STACK: (6, 1)}, + "STATICCALL": {GAS: (700, 700 + 9000 + 25000), STACK: (6, 1)}, + "REVERT": {GAS: (0, 0), STACK: (2, 0)}, + "SUICIDE": {GAS: (5000, 30000), STACK: (1, 0)}, + "ASSERT_FAIL": {GAS: (0, 0), STACK: (0, 0)}, + "INVALID": {GAS: (0, 0), STACK: (0, 0)}, +} # type: Dict[str, Dict[str, Tuple[int, int]]] + + +def calculate_sha3_gas(length: int): + """ + + :param length: + :return: + """ + gas_val = 30 + opcodes.GSHA3WORD * (ceil32(length) // 32) + return gas_val, gas_val + + +def calculate_native_gas(size: int, contract: str): + """ + + :param size: + :param contract: + :return: + """ + gas_value = None + word_num = ceil32(size) // 32 + if contract == "ecrecover": + gas_value = opcodes.GECRECOVER + elif contract == "sha256": + gas_value = opcodes.GSHA256BASE + word_num * opcodes.GSHA256WORD + elif contract == "ripemd160": + gas_value = opcodes.GRIPEMD160BASE + word_num * opcodes.GRIPEMD160WORD + elif contract == "identity": + gas_value = opcodes.GIDENTITYBASE + word_num * opcodes.GIDENTITYWORD + else: + raise ValueError("Unknown contract type {}".format(contract)) + return gas_value, gas_value + + +def get_opcode_gas(opcode: str) -> Tuple[int, int]: + return OPCODES[opcode][GAS] + + +def get_required_stack_elements(opcode: str) -> int: + return OPCODES[opcode][STACK][0] diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 2f1c7f03..a91acd8e 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -34,6 +34,7 @@ from mythril.laser.ethereum.state.calldata import ConcreteCalldata, SymbolicCall import mythril.laser.ethereum.util as helper from mythril.laser.ethereum import util +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.laser.ethereum.call import get_call_parameters, native_call, get_call_data from mythril.laser.ethereum.evm_exceptions import ( VmException, @@ -43,7 +44,7 @@ from mythril.laser.ethereum.evm_exceptions import ( OutOfGasException, WriteProtection, ) -from mythril.laser.ethereum.gas import OPCODE_GAS +from mythril.laser.ethereum.instruction_data import get_opcode_gas, calculate_sha3_gas from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction import ( MessageCallTransaction, @@ -159,7 +160,7 @@ class StateTransition(object): if not self.enable_gas: return global_state opcode = global_state.instruction["opcode"] - min_gas, max_gas = cast(Tuple[int, int], OPCODE_GAS[opcode]) + min_gas, max_gas = get_opcode_gas(opcode) global_state.mstate.min_gas_used += min_gas global_state.mstate.max_gas_used += max_gas self.check_gas_usage_limit(global_state) @@ -619,23 +620,29 @@ class Instruction: :param global_state: :return: """ - state = global_state.mstate - s0, s1 = state.stack.pop(), state.stack.pop() + mstate = global_state.mstate + s0, s1 = mstate.stack.pop(), mstate.stack.pop() try: s0 = util.get_concrete_int(s0) s1 = util.get_concrete_int(s1) except TypeError: - return [] + log.debug("Unsupported symbolic argument for SIGNEXTEND") + mstate.stack.append( + global_state.new_bitvec( + "SIGNEXTEND({},{})".format(hash(s0), hash(s1)), 256 + ) + ) + return [global_state] if s0 <= 31: testbit = s0 * 8 + 7 if s1 & (1 << testbit): - state.stack.append(s1 | (TT256 - (1 << testbit))) + mstate.stack.append(s1 | (TT256 - (1 << testbit))) else: - state.stack.append(s1 & ((1 << testbit) - 1)) + mstate.stack.append(s1 & ((1 << testbit) - 1)) else: - state.stack.append(s1) + mstate.stack.append(s1) return [global_state] @@ -895,9 +902,7 @@ class Instruction: state = global_state.mstate address = state.stack.pop() - balance = global_state.world_state.balances[ - global_state.environment.active_account.address - ] + balance = global_state.world_state.balances[address] state.stack.append(balance) return [global_state] @@ -954,7 +959,7 @@ class Instruction: @staticmethod def _sha3_gas_helper(global_state, length): - min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length) + min_gas, max_gas = calculate_sha3_gas(length) global_state.mstate.min_gas_used += min_gas global_state.mstate.max_gas_used += max_gas StateTransition.check_gas_usage_limit(global_state) @@ -978,9 +983,9 @@ class Instruction: if isinstance(op0, Expression): op0 = simplify(op0) state.stack.append( - symbol_factory.BitVecSym("KECCAC_mem[" + str(op0) + "]", 256) + symbol_factory.BitVecSym("KECCAC_mem[{}]".format(hash(op0)), 256) ) - gas_tuple = cast(Tuple, OPCODE_GAS["SHA3"]) + gas_tuple = get_opcode_gas("SHA3") state.min_gas_used += gas_tuple[0] state.max_gas_used += gas_tuple[1] return [global_state] @@ -992,40 +997,21 @@ class Instruction: b if isinstance(b, BitVec) else symbol_factory.BitVecVal(b, 8) for b in state.memory[index : index + length] ] + if len(data_list) > 1: data = simplify(Concat(data_list)) elif len(data_list) == 1: data = data_list[0] else: - # length is 0; this only matters for input of the BitVecFuncVal - data = symbol_factory.BitVecVal(0, 1) - - if data.symbolic: - - annotations = set() # type: Set[Any] - - for b in state.memory[index : index + length]: - if isinstance(b, BitVec): - annotations = annotations.union(b.annotations) - - argument_hash = hash(state.memory[index]) - result = symbol_factory.BitVecFuncSym( - "KECCAC[invhash({})]".format(hash(argument_hash)), - "keccak256", - 256, - input_=data, - annotations=annotations, - ) - log.debug("Created BitVecFunc hash.") - - else: - keccak = utils.sha3(data.value.to_bytes(length, byteorder="big")) - result = symbol_factory.BitVecFuncVal( - util.concrete_int_from_bytes(keccak, 0), "keccak256", 256, input_=data - ) - log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak))) + # TODO: handle finding x where func(x)==func("") + result = keccak_function_manager.get_empty_keccak_hash() + state.stack.append(result) + return [global_state] + result, condition = keccak_function_manager.create_keccak(data) state.stack.append(result) + state.constraints.append(condition) + return [global_state] @StateTransition() @@ -1519,7 +1505,7 @@ class Instruction: new_state = copy(global_state) # add JUMP gas cost - min_gas, max_gas = cast(Tuple[int, int], OPCODE_GAS["JUMP"]) + min_gas, max_gas = get_opcode_gas("JUMP") new_state.mstate.min_gas_used += min_gas new_state.mstate.max_gas_used += max_gas @@ -1538,7 +1524,7 @@ class Instruction: """ state = global_state.mstate disassembly = global_state.environment.code - min_gas, max_gas = cast(Tuple[int, int], OPCODE_GAS["JUMPI"]) + min_gas, max_gas = get_opcode_gas("JUMPI") states = [] op0, condition = state.stack.pop(), state.stack.pop() @@ -1671,12 +1657,24 @@ class Instruction: code_raw = [] code_end = call_data.size - for i in range(call_data.size): + size = call_data.size + if isinstance(size, BitVec): + # This should be fine because of the below check + if size.symbolic: + size = 10 ** 5 + else: + size = size.value + for i in range(size): if call_data[i].symbolic: code_end = i break code_raw.append(call_data[i].value) + if len(code_raw) < 1: + global_state.mstate.stack.append(1) + log.debug("No code found for trying to execute a create type instruction.") + return global_state + code_str = bytes.hex(bytes(code_raw)) next_transaction_id = get_next_transaction_id() @@ -1731,16 +1729,7 @@ class Instruction: @StateTransition() def create_post(self, global_state: GlobalState) -> List[GlobalState]: - call_value, mem_offset, mem_size = global_state.mstate.pop(3) - call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) - if global_state.last_return_data: - return_val = symbol_factory.BitVecVal( - int(global_state.last_return_data, 16), 256 - ) - else: - return_val = symbol_factory.BitVecVal(0, 256) - global_state.mstate.stack.append(return_val) - return [global_state] + return self._handle_create_type_post(global_state) @StateTransition(is_state_mutation_instruction=True) def create2_(self, global_state: GlobalState) -> List[GlobalState]: @@ -1757,11 +1746,17 @@ class Instruction: @StateTransition() def create2_post(self, global_state: GlobalState) -> List[GlobalState]: - call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) - call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) + return self._handle_create_type_post(global_state, opcode="create2") + + @staticmethod + def _handle_create_type_post(global_state, opcode="cre ate"): + if opcode == "create2": + global_state.mstate.pop(4) + else: + global_state.mstate.pop(3) if global_state.last_return_data: return_val = symbol_factory.BitVecVal( - int(global_state.last_return_data), 256 + int(global_state.last_return_data, 16), 256 ) else: return_val = symbol_factory.BitVecVal(0, 256) @@ -1863,9 +1858,15 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader, True - ) + ( + callee_address, + callee_account, + call_data, + value, + gas, + memory_out_offset, + memory_out_size, + ) = get_call_parameters(global_state, self.dynamic_loader, True) if callee_account is not None and callee_account.code.bytecode == "": log.debug("The call is related to ether transfer between accounts") @@ -1944,9 +1945,15 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters( - global_state, self.dynamic_loader, True - ) + ( + callee_address, + callee_account, + call_data, + value, + gas, + _, + _, + ) = get_call_parameters(global_state, self.dynamic_loader, True) if callee_account is not None and callee_account.code.bytecode == "": log.debug("The call is related to ether transfer between accounts") sender = global_state.environment.active_account.address @@ -1993,9 +2000,15 @@ class Instruction: instr = global_state.get_current_instruction() try: - callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader, True - ) + ( + callee_address, + _, + _, + value, + _, + memory_out_offset, + memory_out_size, + ) = get_call_parameters(global_state, self.dynamic_loader, True) except ValueError as e: log.debug( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( @@ -2059,9 +2072,15 @@ class Instruction: environment = global_state.environment try: - callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters( - global_state, self.dynamic_loader - ) + ( + callee_address, + callee_account, + call_data, + value, + gas, + _, + _, + ) = get_call_parameters(global_state, self.dynamic_loader) if callee_account is not None and callee_account.code.bytecode == "": log.debug("The call is related to ether transfer between accounts") @@ -2109,9 +2128,15 @@ class Instruction: instr = global_state.get_current_instruction() try: - callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader - ) + ( + callee_address, + _, + _, + value, + _, + memory_out_offset, + memory_out_size, + ) = get_call_parameters(global_state, self.dynamic_loader) except ValueError as e: log.debug( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( @@ -2174,9 +2199,15 @@ class Instruction: instr = global_state.get_current_instruction() environment = global_state.environment try: - callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader - ) + ( + callee_address, + callee_account, + call_data, + value, + gas, + memory_out_offset, + memory_out_size, + ) = get_call_parameters(global_state, self.dynamic_loader) if callee_account is not None and callee_account.code.bytecode == "": log.debug("The call is related to ether transfer between accounts") @@ -2230,9 +2261,15 @@ class Instruction: try: with_value = function_name is not "staticcall" - callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader, with_value - ) + ( + callee_address, + callee_account, + call_data, + value, + gas, + memory_out_offset, + memory_out_size, + ) = get_call_parameters(global_state, self.dynamic_loader, with_value) except ValueError as e: log.debug( "Could not determine required parameters for {}, putting fresh symbol on the stack. \n{}".format( diff --git a/mythril/laser/ethereum/keccak_function_manager.py b/mythril/laser/ethereum/keccak_function_manager.py new file mode 100644 index 00000000..ba75861a --- /dev/null +++ b/mythril/laser/ethereum/keccak_function_manager.py @@ -0,0 +1,138 @@ +from ethereum import utils +from mythril.laser.smt import ( + BitVec, + Function, + URem, + symbol_factory, + ULE, + And, + ULT, + Bool, + Or, +) +from typing import Dict, Tuple, List, Optional + +TOTAL_PARTS = 10 ** 40 +PART = (2 ** 256 - 1) // TOTAL_PARTS +INTERVAL_DIFFERENCE = 10 ** 30 +hash_matcher = "fffffff" # This is usually the prefix for the hash in the output + + +class KeccakFunctionManager: + """ + A bunch of uninterpreted functions are considered like keccak256_160 ,... + where keccak256_160 means the input of keccak256() is 160 bit number. + the range of these functions are constrained to some mutually disjoint intervals + All the hashes modulo 64 are 0 as we need a spread among hashes for array type data structures + All the functions are kind of one to one due to constraint of the existence of inverse + for each encountered input. + For more info https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf + """ + + def __init__(self): + self.store_function = {} # type: Dict[int, Tuple[Function, Function]] + self.interval_hook_for_size = {} # type: Dict[int, int] + self._index_counter = TOTAL_PARTS - 34534 + self.hash_result_store = {} # type: Dict[int, List[BitVec]] + self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests + + @staticmethod + def find_concrete_keccak(data: BitVec) -> BitVec: + """ + Calculates concrete keccak + :param data: input bitvecval + :return: concrete keccak output + """ + keccak = symbol_factory.BitVecVal( + int.from_bytes( + utils.sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), + "big", + ), + 256, + ) + return keccak + + def get_function(self, length: int) -> Tuple[Function, Function]: + """ + Returns the keccak functions for the corresponding length + :param length: input size + :return: tuple of keccak and it's inverse + """ + try: + func, inverse = self.store_function[length] + except KeyError: + func = Function("keccak256_{}".format(length), length, 256) + inverse = Function("keccak256_{}-1".format(length), 256, length) + self.store_function[length] = (func, inverse) + self.hash_result_store[length] = [] + return func, inverse + + @staticmethod + def get_empty_keccak_hash() -> BitVec: + """ + returns sha3("") + :return: + """ + val = 89477152217924674838424037953991966239322087453347756267410168184682657981552 + return symbol_factory.BitVecVal(val, 256) + + def create_keccak(self, data: BitVec) -> Tuple[BitVec, Bool]: + """ + Creates Keccak of the data + :param data: input + :return: Tuple of keccak and the condition it should satisfy + """ + length = data.size() + func, inverse = self.get_function(length) + + condition = self._create_condition(func_input=data) + self.quick_inverse[func(data)] = data + self.hash_result_store[length].append(func(data)) + return func(data), condition + + def get_concrete_hash_data(self, model) -> Dict[int, List[Optional[int]]]: + """ + returns concrete values of hashes in the self.hash_result_store + :param model: The z3 model to query for concrete values + :return: A dictionary with concrete hashes { : [, ]} + """ + concrete_hashes = {} # type: Dict[int, List[Optional[int]]] + for size in self.hash_result_store: + concrete_hashes[size] = [] + for val in self.hash_result_store[size]: + eval_ = model.eval(val.raw) + try: + concrete_val = eval_.as_long() + concrete_hashes[size].append(concrete_val) + except AttributeError: + continue + return concrete_hashes + + def _create_condition(self, func_input: BitVec) -> Bool: + """ + Creates the constraints for hash + :param func_input: input of the hash + :return: condition + """ + length = func_input.size() + func, inv = self.get_function(length) + try: + index = self.interval_hook_for_size[length] + except KeyError: + self.interval_hook_for_size[length] = self._index_counter + index = self._index_counter + self._index_counter -= INTERVAL_DIFFERENCE + + lower_bound = index * PART + upper_bound = lower_bound + PART + + cond = And( + inv(func(func_input)) == func_input, + ULE(symbol_factory.BitVecVal(lower_bound, 256), func(func_input)), + ULT(func(func_input), symbol_factory.BitVecVal(upper_bound, 256)), + URem(func(func_input), symbol_factory.BitVecVal(64, 256)) == 0, + ) + return cond + + +keccak_function_manager = KeccakFunctionManager() diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py index 991a172c..e26319be 100644 --- a/mythril/laser/ethereum/natives.py +++ b/mythril/laser/ethereum/natives.py @@ -116,9 +116,7 @@ def mod_exp(data: List[int]) -> List[int]: return [] first_exp_bytes = extract32(bytes_data, 96 + baselen) >> (8 * max(32 - explen, 0)) - bitlength = -1 while first_exp_bytes: - bitlength += 1 first_exp_bytes >>= 1 base = bytearray(baselen) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 8d9c0640..1365c671 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -57,7 +57,6 @@ class Storage: self._standard_storage = K(256, 256, 0) # type: BaseArray else: self._standard_storage = Array("Storage", 256, 256) - self._map_storage = {} # type: Dict[BitVec, BaseArray] self.printable_storage = {} # type: Dict[BitVec, BitVec] @@ -75,11 +74,8 @@ class Storage: return Concat(symbol_factory.BitVecVal(0, 512 - input_.size()), input_) def __getitem__(self, item: BitVec) -> BitVec: - storage, is_keccak_storage = self._get_corresponding_storage(item) - if is_keccak_storage: - sanitized_item = self._sanitize(cast(BitVecFunc, item).input_) - else: - sanitized_item = item + storage = self._standard_storage + sanitized_item = item if ( self.address and self.address.value != 0 @@ -102,7 +98,6 @@ class Storage: self.printable_storage[item] = storage[sanitized_item] except ValueError as e: log.debug("Couldn't read storage at %s: %s", item, e) - return simplify(storage[sanitized_item]) @staticmethod @@ -116,29 +111,12 @@ class Storage: index = Extract(255, 0, key.input_) return simplify(index) - def _get_corresponding_storage(self, key: BitVec) -> Tuple[BaseArray, bool]: - index = self.get_map_index(key) - if index is None: - storage = self._standard_storage - is_keccak_storage = False - else: - storage_map = self._map_storage - try: - storage = storage_map[index] - except KeyError: - if isinstance(self._standard_storage, Array): - storage_map[index] = Array("Storage", 512, 256) - else: - storage_map[index] = K(512, 256, 0) - storage = storage_map[index] - is_keccak_storage = True - return storage, is_keccak_storage + def _get_corresponding_storage(self, key: BitVec) -> BaseArray: + return self._standard_storage def __setitem__(self, key, value: Any) -> None: - storage, is_keccak_storage = self._get_corresponding_storage(key) + storage = self._get_corresponding_storage(key) self.printable_storage[key] = value - if is_keccak_storage: - key = self._sanitize(key.input_) storage[key] = value if key.symbolic is False: self.storage_keys_loaded.add(int(key.value)) @@ -149,7 +127,6 @@ class Storage: concrete=concrete, address=self.address, dynamic_loader=self.dynld ) storage._standard_storage = deepcopy(self._standard_storage) - storage._map_storage = deepcopy(self._map_storage) storage.printable_storage = copy(self.printable_storage) storage.storage_keys_loaded = copy(self.storage_keys_loaded) return storage diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 010091a7..8772e868 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -41,6 +41,7 @@ class Constraints(list): """ :return: True/False based on the existence of solution of constraints """ + if self._is_possible is not None: return self._is_possible solver = Solver() @@ -115,8 +116,8 @@ class Constraints(list): :param constraints: :return: """ - constraints = self._get_smt_bool_list(constraints) - super(Constraints, self).__iadd__(constraints) + list_constraints = self._get_smt_bool_list(constraints) + super(Constraints, self).__iadd__(list_constraints) self._is_possible = None return self diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 5096516e..36aa26b2 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -9,7 +9,6 @@ from mythril.laser.ethereum.cfg import Node from mythril.laser.ethereum.state.environment import Environment from mythril.laser.ethereum.state.machine_state import MachineState from mythril.laser.ethereum.state.annotation import StateAnnotation -from mythril.laser.ethereum.evm_exceptions import ProgramCounterException if TYPE_CHECKING: from mythril.laser.ethereum.state.world_state import WorldState @@ -95,17 +94,15 @@ class GlobalState: :return: """ - instructions = self.environment.code.instruction_list - if self.mstate.pc >= len(instructions): - raise ProgramCounterException( - "PC: {} can not be reached.".format(self.mstate.pc) - ) - return instructions[self.mstate.pc] + try: + return instructions[self.mstate.pc] + except KeyError: + return {"address": self.mstate.pc, "opcode": "STOP"} @property def current_transaction( - self + self, ) -> Union["MessageCallTransaction", "ContractCreationTransaction", None]: """ diff --git a/mythril/laser/ethereum/state/machine_state.py b/mythril/laser/ethereum/state/machine_state.py index e7bca3c0..a30c8afa 100644 --- a/mythril/laser/ethereum/state/machine_state.py +++ b/mythril/laser/ethereum/state/machine_state.py @@ -95,6 +95,7 @@ class MachineState: depth=0, max_gas_used=0, min_gas_used=0, + prev_pc=-1, ) -> None: """Constructor for machineState. @@ -106,8 +107,9 @@ class MachineState: :param depth: :param max_gas_used: :param min_gas_used: + :param prev_pc: """ - self.pc = pc + self._pc = pc self.stack = MachineStack(stack) self.memory = memory or Memory() self.gas_limit = gas_limit @@ -115,6 +117,7 @@ class MachineState: self.max_gas_used = max_gas_used # upper gas usage bound self.constraints = constraints or Constraints() self.depth = depth + self.prev_pc = prev_pc # holds context of current pc def calculate_extension_size(self, start: int, size: int) -> int: """ @@ -210,11 +213,12 @@ class MachineState: gas_limit=self.gas_limit, max_gas_used=self.max_gas_used, min_gas_used=self.min_gas_used, - pc=self.pc, + pc=self._pc, stack=copy(self.stack), memory=copy(self.memory), constraints=copy(self.constraints), depth=self.depth, + prev_pc=self.prev_pc, ) def __str__(self): @@ -224,6 +228,19 @@ class MachineState: """ return str(self.as_dict) + @property + def pc(self) -> int: + """ + + :return: + """ + return self._pc + + @pc.setter + def pc(self, value): + self.prev_pc = self._pc + self._pc = value + @property def memory_size(self) -> int: """ @@ -239,11 +256,12 @@ class MachineState: :return: """ return dict( - pc=self.pc, + pc=self._pc, stack=self.stack, memory=self.memory, memsize=self.memory_size, gas=self.gas_limit, max_gas_used=self.max_gas_used, min_gas_used=self.min_gas_used, + prev_pc=self.prev_pc, ) diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index 151e60c1..5a7583ab 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py @@ -14,7 +14,7 @@ class JumpdestCountAnnotation(StateAnnotation): """State annotation that counts the number of jumps per destination.""" def __init__(self) -> None: - self._reached_count = {} # type: Dict[int, int] + self._reached_count = {} # type: Dict[str, int] def __copy__(self): result = JumpdestCountAnnotation() @@ -64,22 +64,30 @@ class BoundedLoopsStrategy(BasicSearchStrategy): else: annotation = annotations[0] - address = state.get_current_instruction()["address"] + cur_instr = state.get_current_instruction() - if address in annotation._reached_count: - annotation._reached_count[address] += 1 + if cur_instr["opcode"].upper() != "JUMPDEST": + return state + + # create unique instruction identifier + key = "{};{};{}".format( + cur_instr["opcode"], cur_instr["address"], state.mstate.prev_pc + ) + + if key in annotation._reached_count: + annotation._reached_count[key] += 1 else: - annotation._reached_count[address] = 1 + annotation._reached_count[key] = 1 # The creation transaction gets a higher loop bound to give it a better chance of success. # TODO: There's probably a nicer way to do this if isinstance( state.current_transaction, ContractCreationTransaction - ) and annotation._reached_count[address] < max(8, self.bound): + ) and annotation._reached_count[key] < max(8, self.bound): return state - elif annotation._reached_count[address] > self.bound: + elif annotation._reached_count[key] > self.bound: log.debug("Loop bound reached, skipping state") continue diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 8f9549cc..9e3a9fdc 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -10,7 +10,7 @@ from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction -from mythril.laser.ethereum.iprof import InstructionProfiler +from mythril.laser.ethereum.instruction_data import get_required_stack_elements from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( MutationAnnotation, @@ -20,6 +20,7 @@ from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy from abc import ABCMeta from mythril.laser.ethereum.time_handler import time_handler + from mythril.laser.ethereum.transaction import ( ContractCreationTransaction, TransactionEndSignal, @@ -29,6 +30,7 @@ from mythril.laser.ethereum.transaction import ( ) from mythril.laser.smt import symbol_factory + log = logging.getLogger(__name__) @@ -58,7 +60,7 @@ class LaserEVM: strategy=DepthFirstSearchStrategy, transaction_count=2, requires_statespace=True, - enable_iprof=False, + iprof=None, enable_coverage_strategy=False, instruction_laser_plugin=None, ) -> None: @@ -72,7 +74,7 @@ class LaserEVM: :param strategy: Execution search strategy :param transaction_count: The amount of transactions to execute :param requires_statespace: Variable indicating whether the statespace should be recorded - :param enable_iprof: Variable indicating whether instruction profiling should be turned on + :param iprof: Instruction Profiler """ self.open_states = [] # type: List[WorldState] @@ -107,7 +109,7 @@ class LaserEVM: self._start_sym_exec_hooks = [] # type: List[Callable] self._stop_sym_exec_hooks = [] # type: List[Callable] - self.iprof = InstructionProfiler() if enable_iprof else None + self.iprof = iprof if enable_coverage_strategy: from mythril.laser.ethereum.plugins.implementations.coverage.coverage_strategy import ( @@ -206,6 +208,7 @@ class LaserEVM: i, len(self.open_states) ) ) + for hook in self._start_sym_trans_hooks: hook() @@ -245,7 +248,6 @@ class LaserEVM: except NotImplementedError: log.debug("Encountered unimplemented instruction") continue - new_states = [ state for state in new_states if state.mstate.constraints.is_possible ] @@ -270,6 +272,25 @@ class LaserEVM: self.open_states.append(global_state.world_state) + def handle_vm_exception( + self, global_state: GlobalState, op_code: str, error_msg: str + ) -> List[GlobalState]: + transaction, return_global_state = global_state.transaction_stack.pop() + + if return_global_state is None: + # In this case we don't put an unmodified world state in the open_states list Since in the case of an + # exceptional halt all changes should be discarded, and this world state would not provide us with a + # previously unseen world state + log.debug("Encountered a VmException, ending path: `{}`".format(error_msg)) + new_global_states = [] # type: List[GlobalState] + else: + # First execute the post hook for the transaction ending instruction + self._execute_post_hook(op_code, [global_state]) + new_global_states = self._end_message_call( + return_global_state, global_state, revert_changes=True, return_data=None + ) + return new_global_states + def execute_state( self, global_state: GlobalState ) -> Tuple[List[GlobalState], Optional[str]]: @@ -289,6 +310,18 @@ class LaserEVM: except IndexError: self._add_world_state(global_state) return [], None + if len(global_state.mstate.stack) < get_required_stack_elements(op_code): + error_msg = ( + "Stack Underflow Exception due to insufficient " + "stack elements for the address {}".format( + instructions[global_state.mstate.pc]["address"] + ) + ) + new_global_states = self.handle_vm_exception( + global_state, op_code, error_msg + ) + self._execute_post_hook(op_code, new_global_states) + return new_global_states, op_code try: self._execute_pre_hook(op_code, global_state) @@ -302,23 +335,7 @@ class LaserEVM: ).evaluate(global_state) except VmException as e: - transaction, return_global_state = global_state.transaction_stack.pop() - - if return_global_state is None: - # In this case we don't put an unmodified world state in the open_states list Since in the case of an - # exceptional halt all changes should be discarded, and this world state would not provide us with a - # previously unseen world state - log.debug("Encountered a VmException, ending path: `{}`".format(str(e))) - new_global_states = [] - else: - # First execute the post hook for the transaction ending instruction - self._execute_post_hook(op_code, [global_state]) - new_global_states = self._end_message_call( - return_global_state, - global_state, - revert_changes=True, - return_data=None, - ) + new_global_states = self.handle_vm_exception(global_state, op_code, str(e)) except TransactionStartSignal as start_signal: # Setup new global state @@ -337,21 +354,24 @@ class LaserEVM: return [new_global_state], op_code except TransactionEndSignal as end_signal: - transaction, return_global_state = end_signal.global_state.transaction_stack[ - -1 - ] + ( + transaction, + return_global_state, + ) = end_signal.global_state.transaction_stack[-1] log.debug("Ending transaction %s.", transaction) - if return_global_state is None: if ( not isinstance(transaction, ContractCreationTransaction) or transaction.return_data ) and not end_signal.revert: check_potential_issues(global_state) - end_signal.global_state.world_state.node = global_state.node + end_signal.global_state.world_state.node.constraints += ( + end_signal.global_state.mstate.constraints + ) self._add_world_state(end_signal.global_state) + new_global_states = [] else: # First execute the post hook for the transaction ending instruction diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 164df8db..f995a584 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/mythril/laser/ethereum/transaction/concolic.py @@ -88,6 +88,9 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None: condition=None, ) ) + global_state.mstate.constraints += transaction.world_state.node.constraints + new_node.constraints = global_state.mstate.constraints + global_state.world_state.transaction_sequence.append(transaction) global_state.node = new_node new_node.states.append(global_state) diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index b8b6692c..09ee0173 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -1,6 +1,7 @@ """This module contains functions setting up and executing transactions with symbolic values.""" import logging +from typing import Optional from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.cfg import Node, Edge, JumpType @@ -17,14 +18,53 @@ from mythril.laser.smt import symbol_factory, Or, BitVec log = logging.getLogger(__name__) -CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE -ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF -ACTOR_ADDRESSES = [ - symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256), - symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256), - symbol_factory.BitVecVal(0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256), -] +class Actors: + def __init__( + self, + creator=0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, + attacker=0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, + someguy=0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, + ): + self.addresses = { + "CREATOR": symbol_factory.BitVecVal(creator, 256), + "ATTACKER": symbol_factory.BitVecVal(attacker, 256), + "SOMEGUY": symbol_factory.BitVecVal(someguy, 256), + } + + def __setitem__(self, actor: str, address: Optional[str]): + """ + Sets an actor to a desired address + + :param actor: Name of the actor to set + :param address: Address to set the actor to. None to delete the actor + """ + if address is None: + if actor in ("CREATOR", "ATTACKER"): + raise ValueError("Can't delete creator or attacker address") + del self.addresses[actor] + else: + if address[0:2] != "0x": + raise ValueError("Actor address not in valid format") + + self.addresses[actor] = symbol_factory.BitVecVal(int(address[2:], 16), 256) + + def __getitem__(self, actor: str): + return self.addresses[actor] + + @property + def creator(self): + return self.addresses["CREATOR"] + + @property + def attacker(self): + return self.addresses["ATTACKER"] + + def __len__(self): + return len(self.addresses) + + +ACTORS = Actors() def execute_message_call(laser_evm, callee_address: BitVec) -> None: @@ -98,7 +138,7 @@ def execute_contract_creation( "origin{}".format(next_transaction_id), 256 ), code=Disassembly(contract_initialization_code), - caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256), + caller=ACTORS["CREATOR"], contract_name=contract_name, call_data=None, call_value=symbol_factory.BitVecSym( @@ -123,7 +163,7 @@ def _setup_global_state_for_execution(laser_evm, transaction: BaseTransaction) - global_state.transaction_stack.append((transaction, None)) global_state.mstate.constraints.append( - Or(*[transaction.caller == actor for actor in ACTOR_ADDRESSES]) + Or(*[transaction.caller == actor for actor in ACTORS.addresses.values()]) ) new_node = Node( @@ -145,7 +185,7 @@ def _setup_global_state_for_execution(laser_evm, transaction: BaseTransaction) - ) global_state.mstate.constraints += transaction.world_state.node.constraints - new_node.constraints = global_state.mstate.constraints.as_list + new_node.constraints = global_state.mstate.constraints global_state.world_state.transaction_sequence.append(transaction) global_state.node = new_node diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 6ab752ce..86ded2ed 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -22,6 +22,7 @@ from mythril.laser.smt.bitvecfunc import BitVecFunc from mythril.laser.smt.expression import Expression, simplify from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not, And from mythril.laser.smt.array import K, Array, BaseArray +from mythril.laser.smt.function import Function from mythril.laser.smt.solver import Solver, Optimize, SolverStatistics from mythril.laser.smt.model import Model from mythril.laser.smt.bool import Bool as SMTBool @@ -47,6 +48,16 @@ class SymbolFactory(Generic[T, U]): """ raise NotImplementedError + @staticmethod + def BoolSym(name: str, annotations: Annotations = None) -> T: + """ + Creates a boolean symbol + :param name: The name of the Bool variable + :param annotations: The annotations to initialize the bool with + :return: The freshly created Bool() + """ + raise NotImplementedError + @staticmethod def BitVecVal(value: int, size: int, annotations: Annotations = None) -> U: """Creates a new bit vector with a concrete value. @@ -125,6 +136,17 @@ class _SmtSymbolFactory(SymbolFactory[SMTBool, BitVec]): raw = z3.BoolVal(value) return SMTBool(raw, annotations) + @staticmethod + def BoolSym(name: str, annotations: Annotations = None) -> SMTBool: + """ + Creates a boolean symbol + :param name: The name of the Bool variable + :param annotations: The annotations to initialize the bool with + :return: The freshly created Bool() + """ + raw = z3.Bool(name) + return SMTBool(raw, annotations) + @staticmethod def BitVecVal(value: int, size: int, annotations: Annotations = None) -> BitVec: """Creates a new bit vector with a concrete value.""" diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py index 8e68e0c9..c1f60607 100644 --- a/mythril/laser/smt/bitvec_helper.py +++ b/mythril/laser/smt/bitvec_helper.py @@ -1,8 +1,7 @@ -from typing import Union, overload, List, Set, cast, Any, Optional, Callable -from operator import lshift, rshift, ne, eq +from typing import Union, overload, List, Set, cast, Any, Callable import z3 -from mythril.laser.smt.bool import Bool, And, Or +from mythril.laser.smt.bool import Bool, Or from mythril.laser.smt.bitvec import BitVec from mythril.laser.smt.bitvecfunc import BitVecFunc from mythril.laser.smt.bitvecfunc import _arithmetic_helper as _func_arithmetic_helper diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index c645b146..e5bdfec4 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -3,7 +3,7 @@ from itertools import product from typing import Optional, Union, cast, Callable, List import z3 -from mythril.laser.smt.bitvec import BitVec, Annotations +from mythril.laser.smt.bitvec import BitVec, Annotations, _padded_operation from mythril.laser.smt.bool import Or, Bool, And @@ -109,7 +109,10 @@ def _comparison_helper( ) return And( - Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union), + Bool( + cast(z3.BoolRef, _padded_operation(a.raw, b.raw, operation)), + annotations=union, + ), Bool(condition) if b.nested_functions else Bool(True), a.input_ == b.input_ if inputs_equal else a.input_ != b.input_, ) diff --git a/mythril/laser/smt/function.py b/mythril/laser/smt/function.py new file mode 100644 index 00000000..77451871 --- /dev/null +++ b/mythril/laser/smt/function.py @@ -0,0 +1,25 @@ +from typing import cast +import z3 + +from mythril.laser.smt.bitvec import BitVec + + +class Function: + """An uninterpreted function.""" + + def __init__(self, name: str, domain: int, value_range: int): + """Initializes an uninterpreted function. + + :param name: Name of the Function + :param domain: The domain for the Function (10 -> all the values that a bv of size 10 could take) + :param value_range: The range for the values of the function (10 -> all the values that a bv of size 10 could take) + """ + self.domain = z3.BitVecSort(domain) + self.range = z3.BitVecSort(value_range) + self.raw = z3.Function(name, self.domain, self.range) + + def __call__(self, item: BitVec) -> BitVec: + """Function accessor, item can be symbolic.""" + return BitVec( + cast(z3.BitVecRef, self.raw(item.raw)), annotations=item.annotations + ) diff --git a/mythril/laser/smt/solver/solver.py b/mythril/laser/smt/solver/solver.py index 2f3d4ac1..aa79dc85 100644 --- a/mythril/laser/smt/solver/solver.py +++ b/mythril/laser/smt/solver/solver.py @@ -45,14 +45,14 @@ class BaseSolver(Generic[T]): self.add(*constraints) @stat_smt_query - def check(self) -> z3.CheckSatResult: + def check(self, *args) -> z3.CheckSatResult: """Returns z3 smt check result. Also suppresses the stdout when running z3 library's check() to avoid unnecessary output :return: The evaluated result which is either of sat, unsat or unknown """ old_stdout = sys.stdout sys.stdout = open(os.devnull, "w") - evaluate = self.raw.check() + evaluate = self.raw.check(args) sys.stdout = old_stdout return evaluate diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index d5e87369..a7920d57 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/mythril/mythril/mythril_analyzer.py @@ -5,6 +5,7 @@ import logging import traceback from typing import Optional, List +from mythril.laser.ethereum.iprof import InstructionProfiler from . import MythrilDisassembler from mythril.support.source_support import Source from mythril.support.loader import DynLoader @@ -61,7 +62,7 @@ class MythrilAnalyzer: self.execution_timeout = execution_timeout self.loop_bound = loop_bound self.create_timeout = create_timeout - self.enable_iprof = enable_iprof + self.iprof = InstructionProfiler() if enable_iprof else None self.disable_dependency_pruning = disable_dependency_pruning self.enable_coverage_strategy = enable_coverage_strategy self.custom_modules_directory = custom_modules_directory @@ -87,7 +88,7 @@ class MythrilAnalyzer: max_depth=self.max_depth, execution_timeout=self.execution_timeout, create_timeout=self.create_timeout, - enable_iprof=self.enable_iprof, + iprof=self.iprof, disable_dependency_pruning=self.disable_dependency_pruning, run_analysis_modules=False, enable_coverage_strategy=self.enable_coverage_strategy, @@ -111,6 +112,7 @@ class MythrilAnalyzer: :param transaction_count: The amount of transactions to be executed :return: The generated graph in html format """ + sym = SymExecWrapper( contract or self.contracts[0], self.address, @@ -124,7 +126,7 @@ class MythrilAnalyzer: execution_timeout=self.execution_timeout, transaction_count=transaction_count, create_timeout=self.create_timeout, - enable_iprof=self.enable_iprof, + iprof=self.iprof, disable_dependency_pruning=self.disable_dependency_pruning, run_analysis_modules=False, enable_coverage_strategy=self.enable_coverage_strategy, @@ -164,7 +166,7 @@ class MythrilAnalyzer: transaction_count=transaction_count, modules=modules, compulsory_statespace=False, - enable_iprof=self.enable_iprof, + iprof=self.iprof, disable_dependency_pruning=self.disable_dependency_pruning, enable_coverage_strategy=self.enable_coverage_strategy, custom_modules_directory=self.custom_modules_directory, @@ -172,6 +174,8 @@ class MythrilAnalyzer: issues = fire_lasers(sym, modules, self.custom_modules_directory) except KeyboardInterrupt: log.critical("Keyboard Interrupt") + if self.iprof is not None: + log.info("Instruction Statistics:\n{}".format(self.iprof)) issues = retrieve_callback_issues( modules, self.custom_modules_directory ) @@ -184,6 +188,8 @@ class MythrilAnalyzer: modules, self.custom_modules_directory ) exceptions.append(traceback.format_exc()) + if self.iprof is not None: + log.info("Instruction Statistics:\n{}".format(self.iprof)) for issue in issues: issue.add_code_info(contract) diff --git a/mythril/mythril/mythril_disassembler.py b/mythril/mythril/mythril_disassembler.py index e7ef1e3b..ad28f1f5 100644 --- a/mythril/mythril/mythril_disassembler.py +++ b/mythril/mythril/mythril_disassembler.py @@ -1,7 +1,7 @@ import logging import re import solc -import solcx +import sys import os from ethereum import utils @@ -10,11 +10,13 @@ from mythril.ethereum import util from mythril.ethereum.interface.rpc.client import EthJsonRpc from mythril.exceptions import CriticalError, CompilerError, NoContractFoundError from mythril.support import signatures -from mythril.support.truffle import analyze_truffle_project from mythril.ethereum.evmcontract import EVMContract from mythril.ethereum.interface.rpc.exceptions import ConnectionError from mythril.solidity.soliditycontract import SolidityContract, get_contracts_from_file +if sys.version_info[1] >= 6: + import solcx + log = logging.getLogger(__name__) @@ -68,23 +70,30 @@ class MythrilDisassembler: ): log.info("Given version is already installed") else: - try: - if version.startswith("0.4"): + if version.startswith("0.4"): + try: solc.install_solc("v" + version) - else: + except solc.exceptions.SolcError: + raise CriticalError( + "There was an error when trying to install the specified solc version" + ) + elif sys.version_info[1] >= 6: + # solcx supports python 3.6+ + try: solcx.install_solc("v" + version) - solc_binary = util.solc_exists(version) - if not solc_binary: - raise solc.exceptions.SolcError() - except solc.exceptions.SolcError: - raise CriticalError( - "There was an error when trying to install the specified solc version" - ) - except solcx.exceptions.SolcError: + except solcx.exceptions.SolcError: + raise CriticalError( + "There was an error when trying to install the specified solc version" + ) + else: raise CriticalError( - "There was an error when trying to install the specified solc version" + "Py-Solc doesn't support 0.5.*. You can switch to python 3.6 which uses solcx." ) + solc_binary = util.solc_exists(version) + if not solc_binary: + raise solc.exceptions.SolcError() + log.info("Setting the compiler to %s", solc_binary) return solc_binary @@ -225,16 +234,6 @@ class MythrilDisassembler: return address, contracts - def analyze_truffle_project(self, *args, **kwargs) -> None: - """ - :param args: - :param kwargs: - :return: - """ - analyze_truffle_project( - self.sigs, *args, **kwargs - ) # just passthru by passing signatures for now - @staticmethod def hash_for_function_signature(func: str) -> str: """ diff --git a/mythril/support/truffle.py b/mythril/support/truffle.py deleted file mode 100644 index b42b1e10..00000000 --- a/mythril/support/truffle.py +++ /dev/null @@ -1,205 +0,0 @@ -"""This module contains functionality used to easily analyse Truffle -projects.""" -import json -import logging -import os -import re -import sys -import warnings -from pathlib import PurePath - -from ethereum.utils import sha3 - -from mythril.analysis.report import Report -from mythril.analysis.security import fire_lasers -from mythril.analysis.symbolic import SymExecWrapper -from mythril.ethereum import util -from mythril.ethereum.evmcontract import EVMContract -from mythril.laser.ethereum.util import get_instruction_index -from mythril.solidity.soliditycontract import SourceMapping - -log = logging.getLogger(__name__) - - -def format_Warning(message, category, filename, lineno, line=""): - return "{}: {}\n\n".format(str(filename), str(message)) - - -warnings.formatwarning = format_Warning - - -def analyze_truffle_project(sigs, args): - """ - - :param sigs: - :param args: - """ - warnings.warn( - "The option --truffle is being deprecated, Please use the truffle-security plugin, https://github.com/ConsenSys/truffle-security", - FutureWarning, - ) - - project_root = os.getcwd() - - build_dir = os.path.join(project_root, "build", "contracts") - - files = os.listdir(build_dir) - - for filename in files: - - if re.match(r".*\.json$", filename) and filename != "Migrations.json": - - with open(os.path.join(build_dir, filename)) as cf: - contractdata = json.load(cf) - - try: - name = contractdata["contractName"] - bytecode = contractdata["deployedBytecode"] - filename = PurePath(contractdata["sourcePath"]).name - except KeyError: - print( - "Unable to parse contract data. Please use Truffle 4 to compile your project." - ) - sys.exit() - if len(bytecode) < 4: - continue - get_sigs_from_truffle(sigs, contractdata) - - ethcontract = EVMContract(bytecode, name=name) - - address = util.get_indexed_address(0) - sym = SymExecWrapper( - ethcontract, - address, - args.strategy, - max_depth=args.max_depth, - create_timeout=args.create_timeout, - execution_timeout=args.execution_timeout, - transaction_count=args.transaction_count, - modules=args.modules or [], - compulsory_statespace=False, - ) - issues = fire_lasers(sym) - - if not len(issues): - if args.outform == "text" or args.outform == "markdown": - print("# Analysis result for " + name + "\n\nNo issues found.") - else: - result = { - "contract": name, - "result": {"success": True, "error": None, "issues": []}, - } - print(json.dumps(result)) - else: - - report = Report() - # augment with source code - - deployed_disassembly = ethcontract.disassembly - constructor_disassembly = ethcontract.creation_disassembly - - source = contractdata["source"] - - deployed_source_map = contractdata["deployedSourceMap"].split(";") - source_map = contractdata["sourceMap"].split(";") - - deployed_mappings = get_mappings(source, deployed_source_map) - constructor_mappings = get_mappings(source, source_map) - - for issue in issues: - if issue.function == "constructor": - mappings = constructor_mappings - disassembly = constructor_disassembly - else: - mappings = deployed_mappings - disassembly = deployed_disassembly - - index = get_instruction_index( - disassembly.instruction_list, issue.address - ) - - if index: - try: - offset = mappings[index].offset - length = mappings[index].length - - issue.filename = filename - issue.code = source.encode("utf-8")[ - offset : offset + length - ].decode("utf-8") - issue.lineno = mappings[index].lineno - except IndexError: - log.debug("No code mapping at index %d", index) - - report.append_issue(issue) - - if args.outform == "json": - - result = { - "contract": name, - "result": { - "success": True, - "error": None, - "issues": list(map(lambda x: x.as_dict, issues)), - }, - } - print(json.dumps(result)) - - else: - if args.outform == "text": - print( - "# Analysis result for " + name + ":\n\n" + report.as_text() - ) - elif args.outform == "markdown": - print(report.as_markdown()) - - -def get_sigs_from_truffle(sigs, contract_data): - """ - - :param sigs: - :param contract_data: - """ - abis = contract_data["abi"] - for abi in abis: - if abi["type"] != "function": - continue - function_name = abi["name"] - list_of_args = ",".join([input["type"] for input in abi["inputs"]]) - signature = function_name + "(" + list_of_args + ")" - sigs.add("0x" + sha3(signature)[:4].hex(), signature) - - -def get_mappings(source, deployed_source_map): - """ - - :param source: - :param deployed_source_map: - :return: - """ - mappings = [] - prev_item = "" - for item in deployed_source_map: - if item == "": - item = prev_item - - mapping = item.split(":") - - if len(mapping) > 0 and len(mapping[0]) > 0: - offset = int(mapping[0]) - - if len(mapping) > 1 and len(mapping[1]) > 0: - length = int(mapping[1]) - - if len(mapping) > 2 and len(mapping[2]) > 0: - idx = int(mapping[2]) - - if idx == -1: - lineno = None - else: - lineno = source.encode("utf-8")[0:offset].count("\n".encode("utf-8")) + 1 - prev_item = item - - mappings.append(SourceMapping(idx, offset, length, lineno, item)) - - return mappings diff --git a/tests/cmd_line_test.py b/tests/cmd_line_test.py index 258a6882..574c5616 100644 --- a/tests/cmd_line_test.py +++ b/tests/cmd_line_test.py @@ -59,26 +59,17 @@ class CommandLineToolTestCase(BaseTestCase): self.assertIn(""""success": false""", output_of(command)) def test_only_epic(self): - command = "python3 {}".format(MYTH) - self.assertIn("usage: ", output_of(command)) + command = "python3 {} --epic".format(MYTH) + # Just check for crashes + output_of(command) def test_storage(self): - solidity_file = str(TESTDATA / "input_contracts" / "origin.sol") command = """python3 {} read-storage "438767356, 3" 0x76799f77587738bfeef09452df215b63d2cfb08a """.format( MYTH ) self.assertIn("0x1a270efc", output_of(command)) -class TruffleTestCase(BaseTestCase): - def test_analysis_truffle_project(self): - truffle_project_root = str(TESTS_DIR / "truffle_project") - command = "cd {}; truffle compile; python3 {} truffle -t 2".format( - truffle_project_root, MYTH - ) - self.assertIn("=== Unprotected Ether Withdrawal ====", output_of(command)) - - class InfuraTestCase(BaseTestCase): def test_infura_mainnet(self): command = "python3 {} disassemble --rpc infura-mainnet -a 0x2a0c0dbecc7e4d658f48e01e3fa353f44050c208".format( diff --git a/tests/instructions/create_test.py b/tests/instructions/create_test.py index 0a97565e..04f0decd 100644 --- a/tests/instructions/create_test.py +++ b/tests/instructions/create_test.py @@ -1,6 +1,6 @@ from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.cfg import Node from mythril.laser.ethereum.state.environment import Environment -from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.machine_state import MachineState from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState @@ -30,11 +30,12 @@ def execute_create(): calldata = ConcreteCalldata(0, code_raw) world_state = WorldState() + world_state.node = Node("Contract") account = world_state.create_account(balance=1000000, address=101) account.code = Disassembly("60a760006000f000") environment = Environment(account, None, calldata, None, None, None) og_state = GlobalState( - world_state, environment, None, MachineState(gas_limit=8000000) + world_state, environment, world_state.node, MachineState(gas_limit=8000000) ) og_state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) diff --git a/tests/instructions/extcodecopy_test.py b/tests/instructions/extcodecopy_test.py new file mode 100644 index 00000000..ca006fc2 --- /dev/null +++ b/tests/instructions/extcodecopy_test.py @@ -0,0 +1,57 @@ +from mythril.laser.smt import symbol_factory +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction + + +def test_extcodecopy(): + # Arrange + new_world_state = WorldState() + new_account = new_world_state.create_account(balance=10, address=101) + new_account.code = Disassembly("60616240") + ext_account = new_world_state.create_account(balance=1000, address=121) + ext_account.code = Disassembly("6040404040") + + new_environment = Environment(new_account, None, None, None, None, None) + state = GlobalState( + new_world_state, new_environment, None, MachineState(gas_limit=8000000) + ) + state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + + state.mstate.stack = [3, 0, 0, 121] + instruction = Instruction("extcodecopy", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + # Assert + assert new_state.mstate.memory[0:3] == [96, 64, 64] + + +def test_extcodecopy_fail(): + # Arrange + new_world_state = WorldState() + new_account = new_world_state.create_account(balance=10, address=101) + new_account.code = Disassembly("60616240") + new_environment = Environment(new_account, None, None, None, None, None) + state = GlobalState( + new_world_state, new_environment, None, MachineState(gas_limit=8000000) + ) + state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + + state.mstate.stack = [2, 2, 2, symbol_factory.BitVecSym("FAIL", 256)] + instruction = Instruction("extcodecopy", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert new_state.mstate.stack == [] + assert new_state.mstate.memory._memory == state.mstate.memory._memory diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 244b5844..8bbca5ca 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -1,10 +1,10 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.transaction.concolic import execute_message_call from mythril.laser.smt import Expression, BitVec, symbol_factory -from mythril.analysis.solver import get_model from datetime import datetime import binascii @@ -117,7 +117,6 @@ def test_vmtest( # Arrange if test_name in ignored_test_names: return - world_state = WorldState() for address, details in pre_condition.items(): @@ -178,7 +177,15 @@ def test_vmtest( expected = int(value, 16) actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): - actual = actual.value + if ( + actual.symbolic + and actual in keccak_function_manager.quick_inverse + ): + actual = keccak_function_manager.find_concrete_keccak( + keccak_function_manager.quick_inverse[actual] + ) + else: + actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual else: if type(actual) == bytes: diff --git a/tests/laser/keccak_tests.py b/tests/laser/keccak_tests.py new file mode 100644 index 00000000..8a3ae00e --- /dev/null +++ b/tests/laser/keccak_tests.py @@ -0,0 +1,138 @@ +from mythril.laser.smt import Solver, symbol_factory, And +from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager +import z3 +import pytest + + +@pytest.mark.parametrize( + "input1, input2, expected", + [ + (symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(101, 8), z3.unsat), + (symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(100, 16), z3.unsat), + (symbol_factory.BitVecVal(100, 8), symbol_factory.BitVecVal(100, 8), z3.sat), + ( + symbol_factory.BitVecSym("N1", 256), + symbol_factory.BitVecSym("N2", 256), + z3.sat, + ), + ( + symbol_factory.BitVecVal(100, 256), + symbol_factory.BitVecSym("N1", 256), + z3.sat, + ), + ( + symbol_factory.BitVecVal(100, 8), + symbol_factory.BitVecSym("N1", 256), + z3.unsat, + ), + ], +) +def test_keccak_basic(input1, input2, expected): + s = Solver() + + o1, c1 = keccak_function_manager.create_keccak(input1) + o2, c2 = keccak_function_manager.create_keccak(input2) + s.add(And(c1, c2)) + + s.add(o1 == o2) + assert s.check() == expected + + +def test_keccak_symbol_and_val(): + """ + check keccak(100) == keccak(n) && n == 10 + :return: + """ + s = Solver() + hundred = symbol_factory.BitVecVal(100, 256) + n = symbol_factory.BitVecSym("n", 256) + o1, c1 = keccak_function_manager.create_keccak(hundred) + o2, c2 = keccak_function_manager.create_keccak(n) + s.add(And(c1, c2)) + s.add(o1 == o2) + s.add(n == symbol_factory.BitVecVal(10, 256)) + assert s.check() == z3.unsat + + +def test_keccak_complex_eq(): + """ + check for keccak(keccak(b)*2) == keccak(keccak(a)*2) && a != b + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + b = symbol_factory.BitVecSym("b", 160) + o1, c1 = keccak_function_manager.create_keccak(a) + o2, c2 = keccak_function_manager.create_keccak(b) + s.add(And(c1, c2)) + two = symbol_factory.BitVecVal(2, 256) + o1 = two * o1 + o2 = two * o2 + o1, c1 = keccak_function_manager.create_keccak(o1) + o2, c2 = keccak_function_manager.create_keccak(o2) + + s.add(And(c1, c2)) + s.add(o1 == o2) + s.add(a != b) + + assert s.check() == z3.unsat + + +def test_keccak_complex_eq2(): + """ + check for keccak(keccak(b)*2) == keccak(keccak(a)*2) + This isn't combined with prev test because incremental solving here requires extra-extra work + (solution is literally the opposite of prev one) so it will take forever to solve. + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + b = symbol_factory.BitVecSym("b", 160) + o1, c1 = keccak_function_manager.create_keccak(a) + o2, c2 = keccak_function_manager.create_keccak(b) + s.add(And(c1, c2)) + two = symbol_factory.BitVecVal(2, 256) + o1 = two * o1 + o2 = two * o2 + o1, c1 = keccak_function_manager.create_keccak(o1) + o2, c2 = keccak_function_manager.create_keccak(o2) + + s.add(And(c1, c2)) + s.add(o1 == o2) + + assert s.check() == z3.sat + + +def test_keccak_simple_number(): + """ + check for keccak(b) == 10 + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + ten = symbol_factory.BitVecVal(10, 256) + o, c = keccak_function_manager.create_keccak(a) + + s.add(c) + s.add(ten == o) + + assert s.check() == z3.unsat + + +def test_keccak_other_num(): + """ + check keccak(keccak(a)*2) == b + :return: + """ + s = Solver() + a = symbol_factory.BitVecSym("a", 160) + b = symbol_factory.BitVecSym("b", 256) + o, c = keccak_function_manager.create_keccak(a) + two = symbol_factory.BitVecVal(2, 256) + o = two * o + s.add(c) + o, c = keccak_function_manager.create_keccak(o) + s.add(c) + s.add(b == o) + + assert s.check() == z3.sat diff --git a/tests/laser/transaction/create_transaction_test.py b/tests/laser/transaction/create_transaction_test.py index 574dcc06..ad39fb77 100644 --- a/tests/laser/transaction/create_transaction_test.py +++ b/tests/laser/transaction/create_transaction_test.py @@ -11,10 +11,7 @@ from mythril.analysis.symbolic import SymExecWrapper def test_create(): - contract = SolidityContract( - str(tests.TESTDATA_INPUTS_CONTRACTS / "calls.sol"), - solc_binary=MythrilDisassembler._init_solc_binary("0.5.0"), - ) + contract = SolidityContract(str(tests.TESTDATA_INPUTS_CONTRACTS / "calls.sol")) laser_evm = svm.LaserEVM({}) @@ -35,10 +32,7 @@ def test_create(): def test_sym_exec(): - contract = SolidityContract( - str(tests.TESTDATA_INPUTS_CONTRACTS / "calls.sol"), - solc_binary=MythrilDisassembler._init_solc_binary("0.5.0"), - ) + contract = SolidityContract(str(tests.TESTDATA_INPUTS_CONTRACTS / "calls.sol")) sym = SymExecWrapper( contract, diff --git a/tests/native_test.py b/tests/native_test.py index 82bb36b4..3105028d 100644 --- a/tests/native_test.py +++ b/tests/native_test.py @@ -78,10 +78,7 @@ class NativeTests(BaseTestCase): """""" # The solidity version (0.5.3 at the moment) should be kept in sync with # pragma in ./tests/native_tests.sol - disassembly = SolidityContract( - "./tests/native_tests.sol", - solc_binary=MythrilDisassembler._init_solc_binary("0.5.3"), - ).disassembly + disassembly = SolidityContract("./tests/native_tests.sol").disassembly account = Account("0x0000000000000000000000000000000000000000", disassembly) world_state = WorldState() world_state.put_account(account) diff --git a/tests/solidity_contract_test.py b/tests/solidity_contract_test.py index 4edb8e6e..87023116 100644 --- a/tests/solidity_contract_test.py +++ b/tests/solidity_contract_test.py @@ -10,9 +10,7 @@ TEST_FILES = Path(__file__).parent / "testdata/input_contracts" class SolidityContractTest(BaseTestCase): def test_get_source_info_without_name_gets_latest_contract_info(self): input_file = TEST_FILES / "multi_contracts.sol" - contract = SolidityContract( - str(input_file), solc_binary=MythrilDisassembler._init_solc_binary("0.5.0") - ) + contract = SolidityContract(str(input_file)) code_info = contract.get_source_info(142) @@ -22,11 +20,7 @@ class SolidityContractTest(BaseTestCase): def test_get_source_info_with_contract_name_specified(self): input_file = TEST_FILES / "multi_contracts.sol" - contract = SolidityContract( - str(input_file), - name="Transfer1", - solc_binary=MythrilDisassembler._init_solc_binary("0.5.0"), - ) + contract = SolidityContract(str(input_file), name="Transfer1") code_info = contract.get_source_info(142) @@ -36,11 +30,7 @@ class SolidityContractTest(BaseTestCase): def test_get_source_info_with_contract_name_specified_constructor(self): input_file = TEST_FILES / "constructor_assert.sol" - contract = SolidityContract( - str(input_file), - name="AssertFail", - solc_binary=MythrilDisassembler._init_solc_binary("0.5.0"), - ) + contract = SolidityContract(str(input_file), name="AssertFail") code_info = contract.get_source_info(70, constructor=True) diff --git a/tests/truffle_project/README.md b/tests/truffle_project/README.md deleted file mode 100644 index 6629e939..00000000 --- a/tests/truffle_project/README.md +++ /dev/null @@ -1,30 +0,0 @@ -Truffle Hello World Demo -======================== - -``` -npm install -g truffle ethereumjs-testrpc -``` - -This repo is created by following commands: - -``` -truffle init -truffle compile -``` - -In order to run `truffle migrate`, we need to setup `truffle.js` first: - -``` -networks: { - development: { - host: "localhost", - port: 8545, - network_id: "*" // Match any network id - } -} -``` - -Resources ---------- - -- diff --git a/tests/truffle_project/contracts/Migrations.sol b/tests/truffle_project/contracts/Migrations.sol deleted file mode 100644 index f170cb4f..00000000 --- a/tests/truffle_project/contracts/Migrations.sol +++ /dev/null @@ -1,23 +0,0 @@ -pragma solidity ^0.4.17; - -contract Migrations { - address public owner; - uint public last_completed_migration; - - modifier restricted() { - if (msg.sender == owner) _; - } - - function Migrations() public { - owner = msg.sender; - } - - function setCompleted(uint completed) public restricted { - last_completed_migration = completed; - } - - function upgrade(address new_address) public restricted { - Migrations upgraded = Migrations(new_address); - upgraded.setCompleted(last_completed_migration); - } -} diff --git a/tests/truffle_project/contracts/ether_send.sol b/tests/truffle_project/contracts/ether_send.sol deleted file mode 100644 index c8e5bc46..00000000 --- a/tests/truffle_project/contracts/ether_send.sol +++ /dev/null @@ -1,34 +0,0 @@ -contract Crowdfunding { - - mapping(address => uint) public balances; - address public owner; - uint256 INVEST_MIN = 1 ether; - uint256 INVEST_MAX = 10 ether; - - modifier onlyOwner() { - require(msg.sender == owner); - _; - } - - function crowdfunding() { - owner = msg.sender; - } - - function withdrawfunds() onlyOwner { - msg.sender.transfer(this.balance); - } - - function invest() public payable { - require(msg.value > INVEST_MIN && msg.value < INVEST_MAX); - - balances[msg.sender] += msg.value; - } - - function getBalance() public constant returns (uint) { - return balances[msg.sender]; - } - - function() public payable { - invest(); - } -} \ No newline at end of file diff --git a/tests/truffle_project/migrations/1_initial_migration.js b/tests/truffle_project/migrations/1_initial_migration.js deleted file mode 100644 index 4d5f3f9b..00000000 --- a/tests/truffle_project/migrations/1_initial_migration.js +++ /dev/null @@ -1,5 +0,0 @@ -var Migrations = artifacts.require("./Migrations.sol"); - -module.exports = function(deployer) { - deployer.deploy(Migrations); -}; diff --git a/tests/truffle_project/truffle-config.js b/tests/truffle_project/truffle-config.js deleted file mode 100644 index a6330d6d..00000000 --- a/tests/truffle_project/truffle-config.js +++ /dev/null @@ -1,4 +0,0 @@ -module.exports = { - // See - // to customize your Truffle configuration! -}; diff --git a/tests/truffle_project/truffle.js b/tests/truffle_project/truffle.js deleted file mode 100644 index 1a56d124..00000000 --- a/tests/truffle_project/truffle.js +++ /dev/null @@ -1,11 +0,0 @@ -module.exports = { - // See - // to customize your Truffle configuration! - networks: { - development: { - host: "localhost", - port: 8545, - network_id: "*" // Match any network id - } - } -}; diff --git a/tox.ini b/tox.ini index 804b6791..ec2ec40d 100644 --- a/tox.ini +++ b/tox.ini @@ -1,5 +1,5 @@ [tox] -envlist = py36 +envlist = py35, py36 [testenv] deps =