diff --git a/program-analysis/manticore/exercises/example.md b/program-analysis/manticore/exercises/example.md index 5d118e7c..8b295edb 100644 --- a/program-analysis/manticore/exercises/example.md +++ b/program-analysis/manticore/exercises/example.md @@ -1,23 +1,23 @@ # Example: Arithmetic overflow This scenario is given as an example. You can follow its structure to solve the exercises. -[`my_token.py`](example/my_token.py) uses manticore to find for an attacker to generate tokens during a transfer on Token ([my_token.sol](example/my_token.sol)). +[`my_token.py`](example/my_token.py) uses Manticore to find for an attacker to generate tokens during a transfer on Token ([my_token.sol](example/my_token.sol)). -## Proposed scenario +## Proposed scenario -We use the pattern initilization, exploration and property for our scripts. +We use the pattern initialization, exploration and property for our scripts. -### Initialization +## Initialization - Create one user account - Create the contract account -### Exploration +## Exploration - Call balances on the user account - Call transfer with symbolic destination and value - Call balances on the user account -### Property +## Property - Check if the user can have more token after the transfer than before. diff --git a/program-analysis/manticore/exercises/exercise1.md b/program-analysis/manticore/exercises/exercise1.md index 786c6ab6..3cd1712c 100644 --- a/program-analysis/manticore/exercises/exercise1.md +++ b/program-analysis/manticore/exercises/exercise1.md @@ -1,32 +1,32 @@ -# Exercice 1 : Arithmetic +# Exercise 1 : Arithmetic rounding Use Manticore to find an input allowing an attacker to generate free tokens in [exercise1/token.sol](./exercise1/token.sol). Propose a fix of the contract, and test your fix using your Manticore script. ## Proposed scenario -Follow the pattern initilization, exploration and property for the script. +Follow the pattern initialization, exploration and property for the script. -### Initialization +## Initialization - Create one account - Create the contract account -### Exploration +## Exploration - Call `is_valid_buy` with two symbolic values for tokens_amount and wei_amount -### Property +## Property - An attack is found if on a state alive `wei_amount == 0 and tokens_amount >= 1` -### Hints +## Hints - `m.ready_states` returns the list of state alive - `Operators.AND(a, b)` allows to create and AND condition - You can use the template proposed in [exercise1/template.py](./exercise1/template.py) -### Solution +## Solution [exercise1/solution.py](./exercise1/solution.py) \ No newline at end of file diff --git a/program-analysis/manticore/exercises/exercise2.md b/program-analysis/manticore/exercises/exercise2.md index 917891df..3baf3875 100644 --- a/program-analysis/manticore/exercises/exercise2.md +++ b/program-analysis/manticore/exercises/exercise2.md @@ -1,12 +1,12 @@ -# Exercice 2 : Arithmetic on multi transactions +# Exercise 2 : Arithmetic overflow through multiple transactions Use Manticore to find if an overflow is possible in Overflow.add. Propose a fix of the contract, and test your fix using your Manticore script. ## Proposed scenario -Follow the pattern initilization, exploration and property for the script. +Follow the pattern initialization, exploration and property for the script. -### Initialization +## Initialization - Create one user account - Create the contract account @@ -20,7 +20,7 @@ Follow the pattern initilization, exploration and property for the script. - Check if it is possible for the value returned by sellerBalance() to be lower than the first input. -## Hints: +## Hints - The value returned by the last transaction can be accessed through: @@ -36,6 +36,6 @@ data = ABI.deserialize("uint", data) - You can use the template proposed in [exercise2/template.py](./exercise2/template.py) -### Solution +## Solution [exercise2/solution.py](./exercise2/solution.py).