Last active
November 3, 2020 15:57
-
-
Save feliam/f43c87c5425a47e326da2a0f8c61230b to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from manticore import ManticoreEVM | |
from manticore.core.smtlib import Operators | |
m = ManticoreEVM() # initiate the blockchain | |
ETHER = 1**18 | |
# Create accounts and the target contract | |
user = m.create_account(balance=1*ETHER, name='owner') | |
attacker = m.create_account(balance=1*ETHER, name='attacker') | |
contract = m.solidity_create_contract('pepecoin.sol', owner=user) | |
# Prepare symbolic input | |
wei = m.make_symbolic_value(name='wei') | |
token = m.make_symbolic_value(name='token') | |
# The attacker try to buy some tokens | |
contract.buy(token, value=wei, caller=attacker) | |
# Property - check if the attacker got free money | |
prop = Operators.UGT(token, wei*10) | |
for state in m.ready_states: | |
if state.can_be_true(prop): | |
state.constrain(prop) | |
wei_sol, token_sol = state.solve_one_n(wei, token) | |
print(f'Bug found, free money!') | |
print(f'Call buy({token_sol}) and send {wei_sol} ethers') |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
https://gist.github.com/feliam/712a3089af6fb784b299553b6dd60bef