EVM

ABI

class manticore.ethereum.ABI

This class contains methods to handle the ABI. The Application Binary Interface is the standard way to interact with contracts in the Ethereum ecosystem, both from outside the blockchain and for contract-to-contract interaction.

static deserialize(type_spec, data)
static function_call(type_spec, *args)

Build transaction data from function signature and arguments

static function_selector(method_name_and_signature)

Makes a function hash id from a method signature

static serialize(ty, *values, **kwargs)

Serialize value using type specification in ty. ABI.serialize(‘int256’, 1000) ABI.serialize(‘(int, int256)’, 1000, 2000)

Manager

class manticore.ethereum.ManticoreEVM(plugins=None, **kwargs)

Manticore EVM manager

Usage Ex:

from manticore.ethereum import ManticoreEVM, ABI
m = ManticoreEVM()
#And now make the contract account to analyze
source_code = '''
    pragma solidity ^0.4.15;
    contract AnInt {
        uint private i=0;
        function set(uint value){
            i=value
        }
    }
'''
#Initialize user and contracts
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)
contract_account.set(12345, value=100)

m.finalize()
account_name(address)
accounts
all_sound_states

Iterator over all sound states. This tries to solve any symbolic imprecision added by unsound_symbolication and then iterates over the resultant set.

This is the recommended to iterate over resultant steas after an exploration that included unsound symbolication

completed_transactions
constrain(constraint)
contract_accounts
create_account(balance=0, address=None, code=None, name=None, nonce=None)

Low level creates an account. This won’t generate a transaction.

Parameters:
  • balance (int or BitVecVariable) – balance to be set on creation (optional)
  • address (int) – the address for the new account (optional)
  • code – the runtime code for the new account (None means normal account), str or bytes (optional)
  • nonce – force a specific nonce
  • name – a global account name eg. for use as reference in the reports (optional)
Returns:

an EVMAccount

create_contract(owner, balance=0, address=None, init=None, name=None, gas=None)

Creates a contract

Parameters:
  • owner (int or EVMAccount) – owner account (will be default caller in any transactions)
  • balance (int or BitVecVariable) – balance to be transferred on creation
  • address (int) – the address for the new contract (optional)
  • init (str) – initializing evm bytecode and arguments
  • name (str) – a unique name for reference
  • gas – gas budget for the creation/initialization of the contract
Return type:

EVMAccount

current_location(state)
end_block()
finalize(procs=None, only_alive_states=False)

Terminate and generate testcases for all currently alive states (contract states that cleanly executed to a STOP or RETURN in the last symbolic transaction).

Parameters:
  • procs – force the number of local processes to use in the reporting
  • only_alive_states (bool) – if True, killed states (revert/throw/txerror) do not generate testscases

generation. Uses global configuration constant by default

fix_unsound_all(procs=None)
Parameters:procs – force the number of local processes to use
fix_unsound_symbolication(state)
fix_unsound_symbolication_fake(state)

This method goes through all the applied symbolic functions and tries to find a concrete matching set of pairs

fix_unsound_symbolication_sound(state)

This method goes through all the applied symbolic functions and tries to find a concrete matching set of pairs

generate_testcase(state, message='', only_if=None, name='user')

The only_if parameter should be a symbolic expression. If this argument is provided, and the expression can be true in this state, a testcase is generated such that the expression will be true in the state. If it is impossible for the expression to be true in the state, a testcase is not generated.

This is useful for conveniently checking a particular invariant in a state, and generating a testcase if the invariant can be violated.

For example, invariant: “balance” must not be 0. We can check if this can be violated and generate a testcase:

m.generate_testcase(state, 'balance CAN be 0', only_if=balance == 0)
# testcase generated with an input that will violate invariant (make balance == 0)
get_account(name)
get_balance(address, state_id=None)

Balance for account address on state state_id

get_code(address, state_id=None)

Storage data for offset on account address on state state_id

get_metadata(address) → Optional[manticore.ethereum.solidity.SolidityMetadata]

Gets the solidity metadata for address. This is available only if address is a contract created from solidity

get_nonce(address)
get_storage_data(address, offset, state_id=None)

Storage data for offset on account address on state state_id

get_world(state_id=None)

Returns the evm world of state_id state.

global_coverage(account)

Returns code coverage for the contract on account_address. This sums up all the visited code lines from any of the explored states.

global_findings
human_transactions(state_id=None)

Transactions list for state state_id

last_return(state_id=None)

Last returned buffer for state state_id

make_symbolic_address(*accounts, name=None, select='both')

Creates a symbolic address and constrains it to pre-existing addresses or the 0 address.

Parameters:
  • name – Name of the symbolic variable. Defaults to ‘TXADDR’ and later to ‘TXADDR_<number>’
  • select – Whether to select contracts or normal accounts. Not implemented for now.
Returns:

Symbolic address in form of a BitVecVariable.

make_symbolic_arguments(types)

Build a reasonable set of symbolic arguments matching the types list

make_symbolic_buffer(size, name=None, avoid_collisions=False)

Creates a symbolic buffer of size bytes to be used in transactions. You can operate on it normally and add constraints to manticore.constraints via manticore.constrain(constraint_expression)

Example use:

symbolic_data = m.make_symbolic_buffer(320)
m.constrain(symbolic_data[0] == 0x65)
m.transaction(caller=attacker_account,
                address=contract_account,
                data=symbolic_data,
                value=100000 )
make_symbolic_value(nbits=256, name=None)

Creates a symbolic value, normally a uint256, to be used in transactions. You can operate on it normally and add constraints to manticore.constraints via manticore.constrain(constraint_expression)

Example use:

symbolic_value = m.make_symbolic_value()
m.constrain(symbolic_value > 100)
m.constrain(symbolic_value < 1000)
m.transaction(caller=attacker_account,
                address=contract_account,
                data=data,
                value=symbolic_value )
multi_tx_analysis(solidity_filename, contract_name=None, tx_limit=None, tx_use_coverage=True, tx_send_ether=True, tx_account='attacker', tx_preconstrain=False, args=None, compile_args=None)
new_address()

Create a fresh 160bit address

normal_accounts
preconstraint_for_call_transaction(address: Union[int, manticore.ethereum.account.EVMAccount], data: manticore.core.smtlib.expression.Array, value: Union[int, manticore.core.smtlib.expression.Expression, None] = None, contract_metadata: Optional[manticore.ethereum.solidity.SolidityMetadata] = None)

Returns a constraint that excludes combinations of value and data that would cause an exception in the EVM contract dispatcher.

Parameters:
  • address – address of the contract to call
  • value – balance to be transferred (optional)
  • data – symbolic transaction data
  • contract_metadata – SolidityMetadata for the contract (optional)
ready_sound_states

Iterator over sound ready states. This tries to solve any symbolic imprecision added by unsound_symbolication and then iterates over the resultant set.

This is the recommended way to iterate over the resultant states after an exploration that included unsound symbolication

register_detector(d)

Unregisters a plugin. This will invoke detector’s on_unregister callback. Shall be called after .finalize.

run(**kwargs)

Runs analysis.

solidity_create_contract(source_code, owner, name=None, contract_name=None, libraries=None, balance=0, address=None, args=(), gas=None, compile_args=None)

Creates a solidity contract and library dependencies

Parameters:
  • source_code (string (filename, directory, etherscan address) or a file handle) – solidity source code
  • owner (int or EVMAccount) – owner account (will be default caller in any transactions)
  • contract_name (str) – Name of the contract to analyze (optional if there is a single one in the source code)
  • balance (int or BitVecVariable) – balance to be transferred on creation
  • address (int or EVMAccount) – the address for the new contract (optional)
  • args (tuple) – constructor arguments
  • compile_args (dict) – crytic compile options #FIXME(https://github.com/crytic/crytic-compile/wiki/Configuration)
  • gas (int) – gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source)
Return type:

EVMAccount

start_block(blocknumber=None, timestamp=None, difficulty=0, gaslimit=0, coinbase=None)
transaction(caller, address, value, data, gas=None, price=1)

Issue a symbolic transaction in all running states

Parameters:
  • caller (int or EVMAccount) – the address of the account sending the transaction
  • address (int or EVMAccount) – the address of the contract to call
  • value (int or BitVecVariable) – balance to be transfered on creation
  • data – initial data
  • gas – gas budget
  • price – gas unit price
Raises:

NoAliveStates – if there are no alive states to execute

transactions(state_id=None)

Transactions list for state state_id

unregister_detector(d)

Unregisters a detector. This will invoke detector’s on_unregister callback. Shall be called after .finalize - otherwise, finalize won’t add detector’s finding to global.findings.

workspace
world

The world instance or None if there is more than one state

EVM

Symbolic EVM implementation based on the yellow paper: http://gavwood.com/paper.pdf

class manticore.platforms.evm.BlockHeader(blocknumber, timestamp, difficulty, gaslimit, coinbase)
blocknumber

Alias for field number 0

coinbase

Alias for field number 4

difficulty

Alias for field number 2

gaslimit

Alias for field number 3

timestamp

Alias for field number 1

exception manticore.platforms.evm.ConcretizeArgument(pos, expression=None, policy='SAMPLED')

Raised when a symbolic argument needs to be concretized.

exception manticore.platforms.evm.ConcretizeFee(policy='MINMAX')

Raised when a symbolic gas fee needs to be concretized.

exception manticore.platforms.evm.ConcretizeGas(policy='MINMAX')

Raised when a symbolic gas needs to be concretized.

class manticore.platforms.evm.EVM(constraints, address, data, caller, value, bytecode, world=None, gas=None, fork='istanbul', **kwargs)

Machine State. The machine state is defined as the tuple (g, pc, m, i, s) which are the gas available, the program counter pc , the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents are a series of zeroes of bitsize 256

CHAINID()

Get current chainid.

EXTCODEHASH(account)

Get hash of code

SAR(a, b)

Arithmetic Shift Right operation

SELFBALANCE()
SELFDESTRUCT_gas(recipient)
SHL(a, b)

Shift Left operation

SHR(a, b)

Logical Shift Right operation

allocated
bytecode
change_last_result(result)
static check256int(value)
check_oog()
constraints
disassemble()
execute()
fail_if(failed)
gas
instruction

Current instruction pointed by self.pc

is_failed()
pc
read_buffer(offset, size)
read_code(address, size=1)

Read size byte from bytecode. If less than size bytes are available result will be pad with

safe_add(a, b, *args)
safe_mul(a, b)
class transact(pre=None, pos=None, doc=None)
pos(pos)
world
write_buffer(offset, data)
exception manticore.platforms.evm.EVMException
class manticore.platforms.evm.EVMLog(address, memlog, topics)
address

Alias for field number 0

memlog

Alias for field number 1

topics

Alias for field number 2

class manticore.platforms.evm.EVMWorld(constraints, fork='istanbul', **kwargs)
account_exists(address)
accounts
add_refund(value)
add_to_balance(address, value)
all_transactions
block_coinbase()
block_difficulty()
block_gaslimit()
block_hash(block_number=None, force_recent=True)

Calculates a block’s hash

Parameters:
  • block_number – the block number for which to calculate the hash, defaulting to the most recent block
  • force_recent – if True (the default) return zero for any block that is in the future or older than 256 blocks
Returns:

the block hash

block_number()
block_prevhash()
block_timestamp()
static calculate_new_address(sender=None, nonce=None)
constraints
contract_accounts
create_account(address=None, balance=0, code=None, storage=None, nonce=None)

Low level account creation. No transaction is done.

Parameters:
  • address – the address of the account, if known. If omitted, a new address will be generated as closely to the Yellow Paper as possible.
  • balance – the initial balance of the account in Wei
  • code – the runtime code of the account, if a contract
  • storage – storage array
  • nonce – the nonce for the account; contracts should have a nonce greater than or equal to 1
create_contract(price=0, address=None, caller=None, balance=0, init=None, gas=None)

Initiates a CREATE a contract account. Sends a transaction to initialize the contract. Do a world.run() after this to explore all _possible_ outputs

Parameters:
  • address – the address of the new account, if known. If omitted, a new address will be generated as closely to the Yellow Paper as possible.
  • balance – the initial balance of the account in Wei
  • init – the initialization code of the contract

The way that the Solidity compiler expects the constructor arguments to be passed is by appending the arguments to the byte code produced by the Solidity compiler. The arguments are formatted as defined in the Ethereum ABI2. The arguments are then copied from the init byte array to the EVM memory through the CODECOPY opcode with appropriate values on the stack. This is done when the byte code in the init byte array is actually run on the network.

current_human_transaction

Current ongoing human transaction

current_transaction

current tx

current_vm

current vm

delete_account(address)
deleted_accounts
depth
dump(stream, state, mevm, message)
end_block(block_reward=None)
evmfork
execute()
get_balance(address)
get_code(address)
get_nonce(address)
get_storage(address)

Gets the storage of an account

Parameters:address – account address
Returns:account storage
Return type:bytearray or ArrayProxy
get_storage_data(storage_address, offset)

Read a value from a storage slot on the specified account

Parameters:
  • storage_address – an account address
  • offset (int or BitVec) – the storage slot to use.
Returns:

the value

Return type:

int or BitVec

get_storage_items(address)

Gets all items in an account storage

Parameters:address – account address
Returns:all items in account storage. items are tuple of (index, value). value can be symbolic
Return type:list[(storage_index, storage_value)]
has_code(address)
has_storage(address)

True if something has been written to the storage. Note that if a slot has been erased from the storage this function may lose any meaning.

human_transactions

Completed human transaction

increase_nonce(address)
last_human_transaction

Last completed human transaction

last_transaction

Last completed transaction

log(address, topics, data)
log_storage(addr)
logs
new_address(sender=None, nonce=None)

Create a fresh 160bit address

normal_accounts
send_funds(sender, recipient, value)
set_balance(address, value)
set_code(address, data)
set_storage_data(storage_address, offset, value)

Writes a value to a storage slot in specified account

Parameters:
  • storage_address – an account address
  • offset (int or BitVec) – the storage slot to use.
  • value (int or BitVec) – the value to write
start_block(blocknumber=4370000, timestamp=1524785992, difficulty=512, gaslimit=2147483647, coinbase=0)
start_transaction(sort, address, *, price=None, data=None, caller=None, value=0, gas=2300)

Initiate a transaction.

Parameters:
  • sort – the type of transaction. CREATE or CALL or DELEGATECALL
  • address – the address of the account which owns the code that is executing.
  • price – the price of gas in the transaction that originated this execution.
  • data – the byte array that is the input data to this execution
  • caller – the address of the account which caused the code to be executing. A 160-bit code used for identifying Accounts
  • value – the value, in Wei, passed to this account as part of the same procedure as execution. One Ether is defined as being 10**18 Wei.
  • bytecode – the byte array that is the machine code to be executed.
  • gas – gas budget for this transaction.
  • failed – True if the transaction must fail
sub_from_balance(address, value)
sub_refund(value)
symbolic_function(func, data)

Get an unsound symbolication for function func

transaction(address, price=0, data='', caller=None, value=0, gas=2300)

Initiates a CALL transaction on current state. Do a world.run() after this to explore all _possible_ outputs

transactions

Completed completed transaction

try_simplify_to_constant(data)
tx_gasprice()
tx_origin()
exception manticore.platforms.evm.EndTx(result, data=None)

The current transaction ends

is_rollback()
exception manticore.platforms.evm.InvalidOpcode

Trying to execute invalid opcode

exception manticore.platforms.evm.NotEnoughGas

Not enough gas for operation

class manticore.platforms.evm.PendingTransaction(type, address, price, data, caller, value, gas, failed)
address

Alias for field number 1

caller

Alias for field number 4

data

Alias for field number 3

failed

Alias for field number 7

gas

Alias for field number 6

price

Alias for field number 2

type

Alias for field number 0

value

Alias for field number 5

exception manticore.platforms.evm.Return(data=b'')

Program reached a RETURN instruction

exception manticore.platforms.evm.Revert(data)

Program reached a REVERT instruction

exception manticore.platforms.evm.SelfDestruct

Program reached a SELFDESTRUCT instruction

exception manticore.platforms.evm.StackOverflow

Attempted to push more than 1024 items

exception manticore.platforms.evm.StackUnderflow

Attempted to pop from an empty stack

exception manticore.platforms.evm.StartTx

A new transaction is started

exception manticore.platforms.evm.Stop

Program reached a STOP instruction

exception manticore.platforms.evm.TXError

A failed Transaction

exception manticore.platforms.evm.Throw
class manticore.platforms.evm.Transaction(sort, address, price, data, caller, value, gas=0, depth=None, result=None, return_data=None, used_gas=None)
address
caller
concretize(state, constrain=False)
Parameters:
  • state – a manticore state
  • constrain (bool) – If True, constrain expr to concretized value
data
depth
dump(stream, state, mevm, conc_tx=None)

Concretize and write a human readable version of the transaction into the stream. Used during testcase generation.

Parameters:
  • stream – Output stream to write to. Typically a file.
  • state (manticore.ethereum.State) – state that the tx exists in
  • mevm (manticore.ethereum.ManticoreEVM) – manticore instance
Returns:

gas
is_human

Returns whether this is a transaction made by human (in a script).

As an example for:
contract A { function a(B b) { b.b(); } } contract B { function b() {} }

Calling B.b() makes a human transaction. Calling A.a(B) makes a human transaction which makes an internal transaction (b.b()).

price
result
return_data
return_value
set_result(result, return_data=None, used_gas=None)
sort
to_dict(mevm)

Only meant to be used with concrete Transaction objects! (after calling .concretize())

used_gas
value
manticore.platforms.evm.ceil32(x)
manticore.platforms.evm.concretized_args(**policies)

Make sure an EVM instruction has all of its arguments concretized according to provided policies.

Example decoration:

@concretized_args(size=’ONE’, address=’’) def LOG(self, address, size, *topics): …

The above will make sure that the size parameter to LOG is Concretized when symbolic according to the ‘ONE’ policy and concretize address with the default policy.

Parameters:policies – A kwargs list of argument names and their respective policies. Provide None or ‘’ as policy to use default.
Returns:A function decorator
manticore.platforms.evm.globalfakesha3(data)
manticore.platforms.evm.globalsha3(data)
manticore.platforms.evm.to_signed(i)