Getting Started EVM

The basics

To initialize manticore for EVM you can do the following:

from manticore.ethereum import ManticoreEVM

m = MaticoreEVM()

Initially there is a single empty EVM state. ManticoreEVM provides convenient methods to populate the initial state directly from the ManticoreEVM object. The user can create accounts and send transactions at any state. The transactions are emulated even if symbolic arguments were provided. The resultan list of states can be later examined offline. There is also an api to register plugins that can react at realtime to special EVM events like: execute_evm_instruction, open_transaction, close_transaction and others

Adding accounts

create_account

owner_account = m.create_account(balance=1000)

Creating the contract

You can create a contract in manticoreEVM emulated execution environment from its solidity source code. Assigning a name= argument will help understanding the logs after.

contract_account = m.solidity_create_contract(source_code, owner=owner_account)

Once you have the contract setup to your liking you can perform functions on the contract by calling the function

contract_account.function(...)

# You can also pass symbolic values to functions with
contract_account.function(m.make_symbolic_value(name="Name"), ...)

Performing a transaction

low level. can do it using the ABI.xxxxx things transaction

m.transaction(
    caller=user_account, address=contract_account, value=uservalue, data=userdata
)

ABI

serialize and deserialize types to/from buffers

ABI.serialize("uint,uint", m.make_symbolic_value(), m.make_symbolic_value())

...

Search for broken properties over all states. , save? load states in list of states

m.allstates
for st in m.all_states

Symbolic values

You can create symbolic values and pass them as parameters to most functions. (name= is optional)

symbolic_data = m.make_symbolic_buffer(320)
symbolic_value = m.make_symbolic_value(name="value")

m.transaction(
    caller=user_account, address=contract_account, value=symbolic_value, data=symbolic_data
)

Operating on a running contract

EVM provides a way register callbacks to a number of different EVM events via plugin objects plugins.

EVM State

You can access the world in a plugin callback with:

from manticore.core.plugin import Plugin

class testplugin(Plugin)
	def will_decode_instruction_callback(self, state, pc):
		world = state.platform

world

state