mythril.laser.ethereum.function_managers package

Submodules

mythril.laser.ethereum.function_managers.exponent_function_manager module

class mythril.laser.ethereum.function_managers.exponent_function_manager.ExponentFunctionManager

Bases: object

Uses an uninterpreted function for exponentiation with the following properties: 1) power(a, b) > 0 2) if a = 256 => forall i if b = i then power(a, b) = (256 ^ i) % (2^256)

Only these two properties are added as to handle indexing of boolean arrays. Caution should be exercised when increasing the conditions since it severely affects the solving time.

create_condition(base: mythril.laser.smt.bitvec.BitVec, exponent: mythril.laser.smt.bitvec.BitVec) → Tuple[mythril.laser.smt.bitvec.BitVec, mythril.laser.smt.bool.Bool]

Creates a condition for exponentiation :param base: The base of exponentiation :param exponent: The exponent of the exponentiation :return: Tuple of condition and the exponentiation result

mythril.laser.ethereum.function_managers.keccak_function_manager module

class mythril.laser.ethereum.function_managers.keccak_function_manager.KeccakFunctionManager

Bases: object

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

create_conditions() → mythril.laser.smt.bool.Bool

create_keccak(data: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bitvec.BitVec

Creates Keccak of the data :param data: input :return: Tuple of keccak and the condition it should satisfy

static find_concrete_keccak(data: mythril.laser.smt.bitvec.BitVec) → mythril.laser.smt.bitvec.BitVec

Calculates concrete keccak :param data: input bitvecval :return: concrete keccak output

get_concrete_hash_data(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>]}

static get_empty_keccak_hash() → mythril.laser.smt.bitvec.BitVec

returns sha3(“”) :return:

get_function(length: int) → Tuple[mythril.laser.smt.function.Function, mythril.laser.smt.function.Function]

Returns the keccak functions for the corresponding length :param length: input size :return: tuple of keccak and it’s inverse

hash_matcher = 'fffffff'

reset()

Module contents