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)¶
- property accounts¶
- property 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
- property completed_transactions¶
- constrain(constraint)¶
- property 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.
- property 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
- property normal_accounts¶
- preconstraint_for_call_transaction(address: Union[int, manticore.ethereum.account.EVMAccount], data: manticore.core.smtlib.expression.Array, value: Optional[Union[int, manticore.core.smtlib.expression.Expression]] = 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)
- property 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.
- property workspace¶
- property 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)¶
- property blocknumber¶
Alias for field number 0
- property coinbase¶
Alias for field number 4
- property difficulty¶
Alias for field number 2
- property gaslimit¶
Alias for field number 3
- property 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
- property allocated¶
- property bytecode¶
- change_last_result(result)¶
- static check256int(value)¶
- check_oog()¶
- property constraints¶
- disassemble()¶
- execute()¶
- fail_if(failed)¶
- property gas¶
- property instruction¶
Current instruction pointed by self.pc
- is_failed()¶
- property 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)¶
- property world¶
- write_buffer(offset, data)¶
- exception manticore.platforms.evm.EVMException¶
- class manticore.platforms.evm.EVMLog(address, memlog, topics)¶
- property address¶
Alias for field number 0
- property memlog¶
Alias for field number 1
- property topics¶
Alias for field number 2
- class manticore.platforms.evm.EVMWorld(constraints, fork='istanbul', **kwargs)¶
- account_exists(address)¶
- property accounts¶
- add_refund(value)¶
- add_to_balance(address, value)¶
- property 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)¶
- property constraints¶
- property 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.
- property current_human_transaction¶
Current ongoing human transaction
- property current_transaction¶
current tx
- property current_vm¶
current vm
- delete_account(address)¶
- property deleted_accounts¶
- property depth¶
- dump(stream, state, mevm, message)¶
- end_block(block_reward=None)¶
- property 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.
- property human_transactions¶
Completed human transaction
- increase_nonce(address)¶
- property last_human_transaction¶
Last completed human transaction
- property last_transaction¶
Last completed transaction
- log(address, topics, data)¶
- log_storage(addr)¶
- property logs¶
- new_address(sender=None, nonce=None)¶
Create a fresh 160bit address
- property 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
- property 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)¶
- property address¶
Alias for field number 1
- property caller¶
Alias for field number 4
- property data¶
Alias for field number 3
- property failed¶
Alias for field number 7
- property gas¶
Alias for field number 6
- property price¶
Alias for field number 2
- property type¶
Alias for field number 0
- property 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¶
- property 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¶
- property result¶
- property return_data¶
- property return_value¶
- set_result(result, return_data=None, used_gas=None)¶
- property sort¶
- to_dict(mevm)¶
Only meant to be used with concrete Transaction objects! (after calling .concretize())
- property 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)¶