mirror of https://github.com/ConsenSys/mythril
Nikhil Parasaram
5 years ago
commit
8b2393e40c
@ -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="<text/markdown/json/jsonv2>", |
||||
) |
||||
|
||||
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() |
||||
@ -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]] |
||||
@ -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] |
||||
@ -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 { <hash_input_size> : [<concrete_hash>, <concrete_hash>]} |
||||
""" |
||||
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() |
||||
@ -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 |
||||
) |
||||
@ -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 |
||||
@ -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 |
||||
@ -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 |
||||
@ -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 |
||||
--------- |
||||
|
||||
- <https://medium.com/etherereum-salon/eth-testing-472c2f73b4c3> |
||||
@ -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); |
||||
} |
||||
} |
||||
@ -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(); |
||||
} |
||||
} |
||||
@ -1,5 +0,0 @@ |
||||
var Migrations = artifacts.require("./Migrations.sol"); |
||||
|
||||
module.exports = function(deployer) { |
||||
deployer.deploy(Migrations); |
||||
}; |
||||
@ -1,4 +0,0 @@ |
||||
module.exports = { |
||||
// See <http://truffleframework.com/docs/advanced/configuration>
|
||||
// to customize your Truffle configuration!
|
||||
}; |
||||
@ -1,11 +0,0 @@ |
||||
module.exports = { |
||||
// See <http://truffleframework.com/docs/advanced/configuration>
|
||||
// to customize your Truffle configuration!
|
||||
networks: { |
||||
development: { |
||||
host: "localhost", |
||||
port: 8545, |
||||
network_id: "*" // Match any network id
|
||||
} |
||||
} |
||||
}; |
||||
Loading…
Reference in new issue