Use Manticore to find an input allowing an attacker to generate free tokens in token.sol. Propose a fix of the contract, and test your fix using your Manticore script.
Follow the pattern initialization, exploration and property for the script.
- Create one account
- Create the contract account
is_valid_buywith two symbolic values for tokens_amount and wei_amount
- An attack is found if on a state alive
wei_amount == 0 and tokens_amount >= 1
m.ready_statesreturns the list of state alive
Operators.AND(a, b)allows to create and AND condition
- You can use the template proposed in template.py