From e56ddcad88025159f049c378448f89988b6e0674 Mon Sep 17 00:00:00 2001 From: alpharush <0xalpharush@protonmail.com> Date: Wed, 8 Mar 2023 15:05:34 -0600 Subject: [PATCH 1/2] fix spelling and formatting --- program-analysis/manticore/exercises/example.md | 12 ++++++------ program-analysis/manticore/exercises/exercise1.md | 12 ++++++------ program-analysis/manticore/exercises/exercise2.md | 10 +++++----- 3 files changed, 17 insertions(+), 17 deletions(-) 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..f6ee52e3 100644 --- a/program-analysis/manticore/exercises/exercise1.md +++ b/program-analysis/manticore/exercises/exercise1.md @@ -1,5 +1,5 @@ -# Exercice 1 : Arithmetic +# Exercice 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. @@ -8,25 +8,25 @@ Propose a fix of the contract, and test your fix using your Manticore script. Follow the pattern initilization, 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). From fc2a7d89314f6609c2d346bf48e6599ed58fc1b4 Mon Sep 17 00:00:00 2001 From: alpharush <0xalpharush@protonmail.com> Date: Wed, 8 Mar 2023 15:07:11 -0600 Subject: [PATCH 2/2] more spelling fixes --- program-analysis/manticore/exercises/exercise1.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/program-analysis/manticore/exercises/exercise1.md b/program-analysis/manticore/exercises/exercise1.md index f6ee52e3..3cd1712c 100644 --- a/program-analysis/manticore/exercises/exercise1.md +++ b/program-analysis/manticore/exercises/exercise1.md @@ -1,12 +1,12 @@ -# Exercice 1 : Arithmetic rounding +# 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