From a5b22b98613185c95fda66da8593abe2e4a9997c Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 13:50:01 +0200 Subject: [PATCH 01/12] removed some lines --- .github/workflows/medusa.yml | 172 +++++++++++++++++++++++++++++++++++ 1 file changed, 172 insertions(+) create mode 100644 .github/workflows/medusa.yml diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml new file mode 100644 index 00000000..4646dc0d --- /dev/null +++ b/.github/workflows/medusa.yml @@ -0,0 +1,172 @@ +name: Run Medusa tests + +on: + push: + paths: + - ".github/workflows/medusa.yml" + - "program-analysis/echidna/**/*.sol" + - "program-analysis/echidna/**/*.yml" + branches: + - master + pull_request: + paths: + - ".github/workflows/medusa.yml" + - "program-analysis/echidna/**/*.sol" + - "program-analysis/echidna/**/*.yml" + schedule: + # run CI every day even if no PRs/merges occur + - cron: "0 12 * * *" + +jobs: + tests: + name: ${{ matrix.name }} + continue-on-error: ${{ matrix.flaky == true }} + runs-on: ubuntu-22.04 + strategy: + fail-fast: false + matrix: + include: + - name: Exercise 1 + workdir: program-analysis/echidna/exercises/exercise1/ + files: solution.sol + contract: TestToken + outcome: failure + expected: 'echidna_test_balance:\s*failed' + - name: Exercise 2 + workdir: program-analysis/echidna/exercises/exercise2/ + files: solution.sol + contract: TestToken + outcome: failure + expected: 'echidna_no_transfer:\s*failed' + - name: Exercise 3 + workdir: program-analysis/echidna/exercises/exercise3/ + files: solution.sol + contract: TestToken + outcome: failure + expected: 'echidna_test_balance:\s*failed' + - name: Exercise 4 + workdir: program-analysis/echidna/exercises/exercise4/ + files: solution.sol + config: config.yaml + contract: TestToken + outcome: failure + expected: 'transfer(address,uint256):\s*failed' + - name: Exercise 5 + workdir: dvdefi/ + files: . + config: naivereceiver.yaml + crytic-args: --hardhat-ignore-compile + contract: NaiveReceiverEchidna + outcome: failure + expected: 'echidna_test_contract_balance:\s*failed' + - name: Exercise 6 + workdir: dvdefi/ + files: . + config: unstoppable.yaml + crytic-args: --hardhat-ignore-compile + contract: UnstoppableEchidna + outcome: failure + expected: 'echidna_testFlashLoan:\s*failed' + - name: Exercise 7 + workdir: dvdefi/ + files: . + config: sideentrance.yaml + crytic-args: --hardhat-ignore-compile + contract: SideEntranceEchidna + outcome: failure + expected: 'testPoolBalance():\s*failed' + - name: TestToken + workdir: program-analysis/echidna/example/ + files: testtoken.sol + contract: TestToken + outcome: failure + expected: 'echidna_balance_under_1000:\s*failed' + - name: Multi + workdir: program-analysis/echidna/example/ + files: multi.sol + config: filter.yaml + outcome: failure + expected: 'echidna_state4:\s*failed' + - name: Assert + workdir: program-analysis/echidna/example/ + files: assert.sol + config: assert.yaml + outcome: failure + expected: 'inc(uint256):\s*failed' + - name: PopsicleBroken + workdir: program-analysis/echidna/example/ + files: PopsicleBroken.sol + solc-version: 0.8.4 + config: Popsicle.yaml + contract: PopsicleBroken + outcome: failure + expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*failed' + - name: PopsicleFixed + workdir: program-analysis/echidna/example/ + files: PopsicleFixed.sol + solc-version: 0.8.4 + config: Popsicle.yaml + contract: PopsicleFixed + outcome: success + expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*passing' + - name: TestDepositWithPermit + workdir: program-analysis/echidna/example/ + files: TestDepositWithPermit.sol + solc-version: 0.8.0 + config: testdeposit.yaml + contract: TestDepositWithPermit + outcome: success + expected: 'testERC20PermitDeposit(uint256):\s*passing' + - name: MultiABI + workdir: program-analysis/echidna/example/ + files: allContracts.sol + solc-version: 0.8.0 + config: allContracts.yaml + contract: EchidnaTest + outcome: failure + expected: 'test_flag_is_false():\s*failed' + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Checkout Damn Vulnerable DeFi solutions + uses: actions/checkout@v4 + if: startsWith(matrix.workdir, 'dvdefi') + with: + repository: crytic/damn-vulnerable-defi-echidna + ref: solutions + path: ${{ matrix.workdir }} + + - name: Set up Nodejs + uses: actions/setup-node@v3 + if: startsWith(matrix.workdir, 'dvdefi') + with: + node-version: 16 + + - name: Install dependencies and compile + if: startsWith(matrix.workdir, 'dvdefi') + run: | + yarn install --frozen-lockfile + npx hardhat compile --force + working-directory: ${{ matrix.workdir }} + + - name: Go setup + uses: actions/setup-go@v4 + with: + go-version: "^1.18.1" + + - name: Install medusa + run: | + git clone https://github.com/crytic/medusa.git + cd medusa + go build -o medusa -v . + go install -v . + sudo cp medusa /usr/bin + pip install crytic-compile + + - name: Run Medusa for Internal ERC20 tests + continue-on-error: true + working-directory: ${{ matrix.workdir }} + run: | + medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} \ No newline at end of file From a3814d82cded7fb90312103531717870ffa53da1 Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 14:04:56 +0200 Subject: [PATCH 02/12] output to a file and grep result --- .github/workflows/medusa.yml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index 4646dc0d..47a15063 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -100,7 +100,7 @@ jobs: config: Popsicle.yaml contract: PopsicleBroken outcome: failure - expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*failed' + expected: '"PopsicleBroken.totalBalanceAfterTransferIsPreserved(address,uint256)" resulted in an assertion failure after the following call sequence' - name: PopsicleFixed workdir: program-analysis/echidna/example/ files: PopsicleFixed.sol @@ -163,10 +163,22 @@ jobs: go build -o medusa -v . go install -v . sudo cp medusa /usr/bin - pip install crytic-compile + pip install crytic-compile solc-select - - name: Run Medusa for Internal ERC20 tests + - name: Run Medusa continue-on-error: true working-directory: ${{ matrix.workdir }} run: | - medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} \ No newline at end of file + solc-select install ${{ matrix.solc-version || '0.8.0' }} + solc-select use ${{ matrix.solc-version || '0.8.0' }} + medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} > ${{ matrix.files }}.out + + - name: Verify that the output is correct + run: | + if grep -q "${{ matrix.expected }}" "${{ matrix.files }}.out"; then + echo "Output matches" + else + echo "Output mismatch. Expected something matching '${{ matrix.expected }}'. Got the following:" + cat "${{ matrix.files }}.out" + exit 1 + fi \ No newline at end of file From f6cee8e91ba3cbb064c34e2e1f1410ad5567e98d Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 14:17:47 +0200 Subject: [PATCH 03/12] use no-color and escape special characters --- .github/workflows/medusa.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index 47a15063..3d14774c 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -100,7 +100,7 @@ jobs: config: Popsicle.yaml contract: PopsicleBroken outcome: failure - expected: '"PopsicleBroken.totalBalanceAfterTransferIsPreserved(address,uint256)" resulted in an assertion failure after the following call sequence' + expected: '\"PopsicleBroken.totalBalanceAfterTransferIsPreserved(address,uint256)\" resulted in an assertion failure after the following call sequence' - name: PopsicleFixed workdir: program-analysis/echidna/example/ files: PopsicleFixed.sol @@ -108,7 +108,7 @@ jobs: config: Popsicle.yaml contract: PopsicleFixed outcome: success - expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*passing' + expected: '\[PASSED\] Assertion Test: PopsicleFixed.totalBalanceAfterTransferIsPreserved(address,uint256)' - name: TestDepositWithPermit workdir: program-analysis/echidna/example/ files: TestDepositWithPermit.sol @@ -171,7 +171,7 @@ jobs: run: | solc-select install ${{ matrix.solc-version || '0.8.0' }} solc-select use ${{ matrix.solc-version || '0.8.0' }} - medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} > ${{ matrix.files }}.out + medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color > ${{ matrix.files }}.out || true - name: Verify that the output is correct run: | From 23818e910868a5c80a57d261ce91099b085fdb5c Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 14:22:05 +0200 Subject: [PATCH 04/12] fix --- .github/workflows/medusa.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index 3d14774c..a6fa27d9 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -174,6 +174,7 @@ jobs: medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color > ${{ matrix.files }}.out || true - name: Verify that the output is correct + working-directory: ${{ matrix.workdir }} run: | if grep -q "${{ matrix.expected }}" "${{ matrix.files }}.out"; then echo "Output matches" From f4ffffa2c52ca60de0d6d3d3924ad4fc927283c1 Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 14:35:51 +0200 Subject: [PATCH 05/12] added generic medusa config --- .github/workflows/medusa.yml | 2 +- program-analysis/echidna/example/medusa.json | 21 ++++++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) create mode 100644 program-analysis/echidna/example/medusa.json diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index a6fa27d9..ec45575b 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -171,7 +171,7 @@ jobs: run: | solc-select install ${{ matrix.solc-version || '0.8.0' }} solc-select use ${{ matrix.solc-version || '0.8.0' }} - medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color > ${{ matrix.files }}.out || true + medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color --config medusa.json > ${{ matrix.files }}.out || true - name: Verify that the output is correct working-directory: ${{ matrix.workdir }} diff --git a/program-analysis/echidna/example/medusa.json b/program-analysis/echidna/example/medusa.json new file mode 100644 index 00000000..ede08d68 --- /dev/null +++ b/program-analysis/echidna/example/medusa.json @@ -0,0 +1,21 @@ +{ + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": [ + "echidna_" + ] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } +} From 5b1d14e3e3374a416622bfdbb915f7458a6647e6 Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 14:44:40 +0200 Subject: [PATCH 06/12] more medusa configs --- .github/workflows/medusa.yml | 6 +++--- .../echidna/exercises/exercise1/medusa.json | 21 +++++++++++++++++++ .../echidna/exercises/exercise2/medusa.json | 21 +++++++++++++++++++ .../echidna/exercises/exercise3/medusa.json | 21 +++++++++++++++++++ .../echidna/exercises/exercise4/medusa.json | 21 +++++++++++++++++++ 5 files changed, 87 insertions(+), 3 deletions(-) create mode 100644 program-analysis/echidna/exercises/exercise1/medusa.json create mode 100644 program-analysis/echidna/exercises/exercise2/medusa.json create mode 100644 program-analysis/echidna/exercises/exercise3/medusa.json create mode 100644 program-analysis/echidna/exercises/exercise4/medusa.json diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index ec45575b..fb94101e 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -84,6 +84,7 @@ jobs: - name: Multi workdir: program-analysis/echidna/example/ files: multi.sol + contract: C config: filter.yaml outcome: failure expected: 'echidna_state4:\s*failed' @@ -91,13 +92,13 @@ jobs: workdir: program-analysis/echidna/example/ files: assert.sol config: assert.yaml + contract: Incrementor outcome: failure expected: 'inc(uint256):\s*failed' - name: PopsicleBroken workdir: program-analysis/echidna/example/ files: PopsicleBroken.sol solc-version: 0.8.4 - config: Popsicle.yaml contract: PopsicleBroken outcome: failure expected: '\"PopsicleBroken.totalBalanceAfterTransferIsPreserved(address,uint256)\" resulted in an assertion failure after the following call sequence' @@ -105,7 +106,6 @@ jobs: workdir: program-analysis/echidna/example/ files: PopsicleFixed.sol solc-version: 0.8.4 - config: Popsicle.yaml contract: PopsicleFixed outcome: success expected: '\[PASSED\] Assertion Test: PopsicleFixed.totalBalanceAfterTransferIsPreserved(address,uint256)' @@ -171,7 +171,7 @@ jobs: run: | solc-select install ${{ matrix.solc-version || '0.8.0' }} solc-select use ${{ matrix.solc-version || '0.8.0' }} - medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color --config medusa.json > ${{ matrix.files }}.out || true + medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color --test-limit 10000 --config medusa.json > ${{ matrix.files }}.out || true - name: Verify that the output is correct working-directory: ${{ matrix.workdir }} diff --git a/program-analysis/echidna/exercises/exercise1/medusa.json b/program-analysis/echidna/exercises/exercise1/medusa.json new file mode 100644 index 00000000..ede08d68 --- /dev/null +++ b/program-analysis/echidna/exercises/exercise1/medusa.json @@ -0,0 +1,21 @@ +{ + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": [ + "echidna_" + ] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } +} diff --git a/program-analysis/echidna/exercises/exercise2/medusa.json b/program-analysis/echidna/exercises/exercise2/medusa.json new file mode 100644 index 00000000..ede08d68 --- /dev/null +++ b/program-analysis/echidna/exercises/exercise2/medusa.json @@ -0,0 +1,21 @@ +{ + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": [ + "echidna_" + ] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } +} diff --git a/program-analysis/echidna/exercises/exercise3/medusa.json b/program-analysis/echidna/exercises/exercise3/medusa.json new file mode 100644 index 00000000..ede08d68 --- /dev/null +++ b/program-analysis/echidna/exercises/exercise3/medusa.json @@ -0,0 +1,21 @@ +{ + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": [ + "echidna_" + ] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } +} diff --git a/program-analysis/echidna/exercises/exercise4/medusa.json b/program-analysis/echidna/exercises/exercise4/medusa.json new file mode 100644 index 00000000..ede08d68 --- /dev/null +++ b/program-analysis/echidna/exercises/exercise4/medusa.json @@ -0,0 +1,21 @@ +{ + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": [ + "echidna_" + ] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } +} From d1e5d4b35b5db3666d653fad92656c28dd8037a1 Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 14:51:30 +0200 Subject: [PATCH 07/12] fixed medusa matching strings --- .github/workflows/medusa.yml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index fb94101e..23327476 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -31,26 +31,26 @@ jobs: files: solution.sol contract: TestToken outcome: failure - expected: 'echidna_test_balance:\s*failed' + expected: 'echidna_test_balance()\" failed after the following call sequence' - name: Exercise 2 workdir: program-analysis/echidna/exercises/exercise2/ files: solution.sol contract: TestToken outcome: failure - expected: 'echidna_no_transfer:\s*failed' + expected: 'echidna_no_transfer()\" failed after the following call sequence' - name: Exercise 3 workdir: program-analysis/echidna/exercises/exercise3/ files: solution.sol contract: TestToken outcome: failure - expected: 'echidna_test_balance:\s*failed' + expected: 'echidna_test_balance()\" failed after the following call sequence' - name: Exercise 4 workdir: program-analysis/echidna/exercises/exercise4/ files: solution.sol config: config.yaml contract: TestToken outcome: failure - expected: 'transfer(address,uint256):\s*failed' + expected: 'transfer(address,uint256)\" failed after the following call sequence' - name: Exercise 5 workdir: dvdefi/ files: . @@ -80,28 +80,28 @@ jobs: files: testtoken.sol contract: TestToken outcome: failure - expected: 'echidna_balance_under_1000:\s*failed' + expected: 'echidna_balance_under_1000()\" failed after the following call sequence' - name: Multi workdir: program-analysis/echidna/example/ files: multi.sol contract: C config: filter.yaml outcome: failure - expected: 'echidna_state4:\s*failed' + expected: 'echidna_state4()\" failed after the following call sequence' - name: Assert workdir: program-analysis/echidna/example/ files: assert.sol config: assert.yaml contract: Incrementor outcome: failure - expected: 'inc(uint256):\s*failed' + expected: 'inc(uint256)\" failed after the following call sequence' - name: PopsicleBroken workdir: program-analysis/echidna/example/ files: PopsicleBroken.sol solc-version: 0.8.4 contract: PopsicleBroken outcome: failure - expected: '\"PopsicleBroken.totalBalanceAfterTransferIsPreserved(address,uint256)\" resulted in an assertion failure after the following call sequence' + expected: 'PopsicleBroken.totalBalanceAfterTransferIsPreserved(address,uint256)\" resulted in an assertion failure after the following call sequence' - name: PopsicleFixed workdir: program-analysis/echidna/example/ files: PopsicleFixed.sol From e64c03efa0b666b0c79065d3be3f40cb404786e4 Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 14:57:00 +0200 Subject: [PATCH 08/12] fixes --- .github/workflows/medusa.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index 23327476..ca1acad2 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -87,14 +87,14 @@ jobs: contract: C config: filter.yaml outcome: failure - expected: 'echidna_state4()\" failed after the following call sequence' + expected: 'echidna_state4()\" resulted in an assertion failure after the following call sequence' - name: Assert workdir: program-analysis/echidna/example/ files: assert.sol config: assert.yaml contract: Incrementor outcome: failure - expected: 'inc(uint256)\" failed after the following call sequence' + expected: 'inc(uint256)\" resulted in an assertion failure after the following call sequence' - name: PopsicleBroken workdir: program-analysis/echidna/example/ files: PopsicleBroken.sol @@ -171,7 +171,7 @@ jobs: run: | solc-select install ${{ matrix.solc-version || '0.8.0' }} solc-select use ${{ matrix.solc-version || '0.8.0' }} - medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color --test-limit 10000 --config medusa.json > ${{ matrix.files }}.out || true + medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color --test-limit 30000 --config medusa.json > ${{ matrix.files }}.out || true - name: Verify that the output is correct working-directory: ${{ matrix.workdir }} From f54d0e6e7b1085d03eeb3765894333816bcb5455 Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 16:27:05 +0200 Subject: [PATCH 09/12] fixes --- .github/workflows/medusa.yml | 3 +- program-analysis/echidna/example/medusa.json | 4 +- .../echidna/exercises/exercise4/medusa.json | 63 ++++++++++++++++++- 3 files changed, 65 insertions(+), 5 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index ca1acad2..49335575 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -47,7 +47,6 @@ jobs: - name: Exercise 4 workdir: program-analysis/echidna/exercises/exercise4/ files: solution.sol - config: config.yaml contract: TestToken outcome: failure expected: 'transfer(address,uint256)\" failed after the following call sequence' @@ -87,7 +86,7 @@ jobs: contract: C config: filter.yaml outcome: failure - expected: 'echidna_state4()\" resulted in an assertion failure after the following call sequence' + expected: 'echidna_state4()\" failed after the following call sequence' - name: Assert workdir: program-analysis/echidna/example/ files: assert.sol diff --git a/program-analysis/echidna/example/medusa.json b/program-analysis/echidna/example/medusa.json index ede08d68..dca9033d 100644 --- a/program-analysis/echidna/example/medusa.json +++ b/program-analysis/echidna/example/medusa.json @@ -1,8 +1,10 @@ { "fuzzing": { "testing": { + "assertionTesting": { + "enabled": true + }, "propertyTesting": { - "enabled": true, "testPrefixes": [ "echidna_" ] diff --git a/program-analysis/echidna/exercises/exercise4/medusa.json b/program-analysis/echidna/exercises/exercise4/medusa.json index ede08d68..bb2a17a6 100644 --- a/program-analysis/echidna/exercises/exercise4/medusa.json +++ b/program-analysis/echidna/exercises/exercise4/medusa.json @@ -1,12 +1,66 @@ { "fuzzing": { + "workers": 10, + "workerResetLimit": 50, + "timeout": 0, + "testLimit": 0, + "callSequenceLength": 100, + "corpusDirectory": "", + "coverageEnabled": true, + "targetContracts": [], + "targetContractsBalances": [], + "constructorArgs": {}, + "deployerAddress": "0x30000", + "senderAddresses": [ + "0x10000", + "0x20000", + "0x30000" + ], + "blockNumberDelayMax": 60480, + "blockTimestampDelayMax": 604800, + "blockGasLimit": 125000000, + "transactionGasLimit": 12500000, "testing": { + "stopOnFailedTest": true, + "stopOnFailedContractMatching": false, + "stopOnNoTests": true, + "testAllContracts": false, + "traceAll": false, + "assertionTesting": { + "enabled": true, + "testViewMethods": false, + "panicCodeConfig": { + "failOnCompilerInsertedPanic": false, + "failOnAssertion": true, + "failOnArithmeticUnderflow": false, + "failOnDivideByZero": false, + "failOnEnumTypeConversionOutOfBounds": false, + "failOnIncorrectStorageAccess": false, + "failOnPopEmptyArray": false, + "failOnOutOfBoundsArrayAccess": false, + "failOnAllocateTooMuchMemory": false, + "failOnCallUninitializedVariable": false + } + }, "propertyTesting": { "enabled": true, "testPrefixes": [ - "echidna_" + "property_" + ] + }, + "optimizationTesting": { + "enabled": true, + "testPrefixes": [ + "optimize_" ] } + }, + "chainConfig": { + "codeSizeCheckDisabled": true, + "cheatCodes": { + "cheatCodesEnabled": true, + "enableFFI": false + } } }, "compilation": { @@ -17,5 +71,10 @@ "exportDirectory": "", "args": [] } + }, + "logging": { + "level": "info", + "logDirectory": "", + "noColor": false } -} +} \ No newline at end of file From 02aadc778aaba2fc09639c391394c5532c050d2f Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 16:35:12 +0200 Subject: [PATCH 10/12] fixes --- .github/workflows/medusa.yml | 2 +- program-analysis/echidna/example/medusa.json | 61 +++++++++++++++++++- 2 files changed, 60 insertions(+), 3 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index 49335575..b5c4d7cd 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -170,7 +170,7 @@ jobs: run: | solc-select install ${{ matrix.solc-version || '0.8.0' }} solc-select use ${{ matrix.solc-version || '0.8.0' }} - medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color --test-limit 30000 --config medusa.json > ${{ matrix.files }}.out || true + medusa fuzz --compilation-target ${{ matrix.files }} --target-contracts ${{ matrix.contract }} --no-color --test-limit 100000 --config medusa.json > ${{ matrix.files }}.out || true - name: Verify that the output is correct working-directory: ${{ matrix.workdir }} diff --git a/program-analysis/echidna/example/medusa.json b/program-analysis/echidna/example/medusa.json index dca9033d..02ffefd5 100644 --- a/program-analysis/echidna/example/medusa.json +++ b/program-analysis/echidna/example/medusa.json @@ -1,13 +1,65 @@ { "fuzzing": { + "workers": 10, + "workerResetLimit": 50, + "timeout": 0, + "testLimit": 0, + "callSequenceLength": 100, + "corpusDirectory": "", + "coverageEnabled": true, + "targetContracts": [], + "targetContractsBalances": [], + "constructorArgs": {}, + "deployerAddress": "0x30000", + "senderAddresses": [ + "0x10000", + "0x20000", + "0x30000" + ], + "blockNumberDelayMax": 60480, + "blockTimestampDelayMax": 604800, + "blockGasLimit": 125000000, + "transactionGasLimit": 12500000, "testing": { + "stopOnFailedTest": true, + "stopOnFailedContractMatching": false, + "stopOnNoTests": true, + "testAllContracts": false, + "traceAll": false, "assertionTesting": { - "enabled": true + "enabled": true, + "testViewMethods": false, + "panicCodeConfig": { + "failOnCompilerInsertedPanic": false, + "failOnAssertion": true, + "failOnArithmeticUnderflow": false, + "failOnDivideByZero": false, + "failOnEnumTypeConversionOutOfBounds": false, + "failOnIncorrectStorageAccess": false, + "failOnPopEmptyArray": false, + "failOnOutOfBoundsArrayAccess": false, + "failOnAllocateTooMuchMemory": false, + "failOnCallUninitializedVariable": false + } }, "propertyTesting": { + "enabled": true, "testPrefixes": [ "echidna_" ] + }, + "optimizationTesting": { + "enabled": false, + "testPrefixes": [ + "optimize_" + ] + } + }, + "chainConfig": { + "codeSizeCheckDisabled": true, + "cheatCodes": { + "cheatCodesEnabled": true, + "enableFFI": false } } }, @@ -19,5 +71,10 @@ "exportDirectory": "", "args": [] } + }, + "logging": { + "level": "info", + "logDirectory": "", + "noColor": false } -} +} \ No newline at end of file From 1699de765879f4059e6f5435e38a56ca456f43fd Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 16:39:17 +0200 Subject: [PATCH 11/12] fixes and disabled other tests --- .github/workflows/medusa.yml | 68 ++++++++++++++++++------------------ 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index b5c4d7cd..c1b9b33c 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -49,31 +49,31 @@ jobs: files: solution.sol contract: TestToken outcome: failure - expected: 'transfer(address,uint256)\" failed after the following call sequence' - - name: Exercise 5 - workdir: dvdefi/ - files: . - config: naivereceiver.yaml - crytic-args: --hardhat-ignore-compile - contract: NaiveReceiverEchidna - outcome: failure - expected: 'echidna_test_contract_balance:\s*failed' - - name: Exercise 6 - workdir: dvdefi/ - files: . - config: unstoppable.yaml - crytic-args: --hardhat-ignore-compile - contract: UnstoppableEchidna - outcome: failure - expected: 'echidna_testFlashLoan:\s*failed' - - name: Exercise 7 - workdir: dvdefi/ - files: . - config: sideentrance.yaml - crytic-args: --hardhat-ignore-compile - contract: SideEntranceEchidna - outcome: failure - expected: 'testPoolBalance():\s*failed' + expected: 'transfer(address,uint256)\" resulted in an assertion failure after the following call sequence:' + # - name: Exercise 5 + # workdir: dvdefi/ + # files: . + # config: naivereceiver.yaml + # crytic-args: --hardhat-ignore-compile + # contract: NaiveReceiverEchidna + # outcome: failure + # expected: 'echidna_test_contract_balance:\s*failed' + # - name: Exercise 6 + # workdir: dvdefi/ + # files: . + # config: unstoppable.yaml + # crytic-args: --hardhat-ignore-compile + # contract: UnstoppableEchidna + # outcome: failure + # expected: 'echidna_testFlashLoan:\s*failed' + # - name: Exercise 7 + # workdir: dvdefi/ + # files: . + # config: sideentrance.yaml + # crytic-args: --hardhat-ignore-compile + # contract: SideEntranceEchidna + # outcome: failure + # expected: 'testPoolBalance():\s*failed' - name: TestToken workdir: program-analysis/echidna/example/ files: testtoken.sol @@ -115,15 +115,15 @@ jobs: config: testdeposit.yaml contract: TestDepositWithPermit outcome: success - expected: 'testERC20PermitDeposit(uint256):\s*passing' - - name: MultiABI - workdir: program-analysis/echidna/example/ - files: allContracts.sol - solc-version: 0.8.0 - config: allContracts.yaml - contract: EchidnaTest - outcome: failure - expected: 'test_flag_is_false():\s*failed' + expected: '\[PASSED\] Assertion Test: TestDepositWithPermit.testERC20PermitDeposit(uint256)' + # - name: MultiABI + # workdir: program-analysis/echidna/example/ + # files: allContracts.sol + # solc-version: 0.8.0 + # config: allContracts.yaml + # contract: EchidnaTest + # outcome: failure + # expected: 'test_flag_is_false():\s*failed' steps: - name: Checkout repository From dcb2651a697371a19903315c2792800f27b91740 Mon Sep 17 00:00:00 2001 From: ggrieco-tob Date: Wed, 29 May 2024 17:06:21 +0200 Subject: [PATCH 12/12] format --- .github/workflows/medusa.yml | 16 +- program-analysis/echidna/example/medusa.json | 150 +++++++++--------- .../echidna/exercises/exercise1/medusa.json | 36 ++--- .../echidna/exercises/exercise2/medusa.json | 36 ++--- .../echidna/exercises/exercise3/medusa.json | 36 ++--- .../echidna/exercises/exercise4/medusa.json | 150 +++++++++--------- 6 files changed, 201 insertions(+), 223 deletions(-) diff --git a/.github/workflows/medusa.yml b/.github/workflows/medusa.yml index c1b9b33c..8f06b830 100644 --- a/.github/workflows/medusa.yml +++ b/.github/workflows/medusa.yml @@ -153,16 +153,16 @@ jobs: - name: Go setup uses: actions/setup-go@v4 with: - go-version: "^1.18.1" + go-version: "^1.18.1" - name: Install medusa run: | - git clone https://github.com/crytic/medusa.git - cd medusa - go build -o medusa -v . - go install -v . - sudo cp medusa /usr/bin - pip install crytic-compile solc-select + git clone https://github.com/crytic/medusa.git + cd medusa + go build -o medusa -v . + go install -v . + sudo cp medusa /usr/bin + pip install crytic-compile solc-select - name: Run Medusa continue-on-error: true @@ -181,4 +181,4 @@ jobs: echo "Output mismatch. Expected something matching '${{ matrix.expected }}'. Got the following:" cat "${{ matrix.files }}.out" exit 1 - fi \ No newline at end of file + fi diff --git a/program-analysis/echidna/example/medusa.json b/program-analysis/echidna/example/medusa.json index 02ffefd5..a8a951b9 100644 --- a/program-analysis/echidna/example/medusa.json +++ b/program-analysis/echidna/example/medusa.json @@ -1,80 +1,72 @@ { - "fuzzing": { - "workers": 10, - "workerResetLimit": 50, - "timeout": 0, - "testLimit": 0, - "callSequenceLength": 100, - "corpusDirectory": "", - "coverageEnabled": true, - "targetContracts": [], - "targetContractsBalances": [], - "constructorArgs": {}, - "deployerAddress": "0x30000", - "senderAddresses": [ - "0x10000", - "0x20000", - "0x30000" - ], - "blockNumberDelayMax": 60480, - "blockTimestampDelayMax": 604800, - "blockGasLimit": 125000000, - "transactionGasLimit": 12500000, - "testing": { - "stopOnFailedTest": true, - "stopOnFailedContractMatching": false, - "stopOnNoTests": true, - "testAllContracts": false, - "traceAll": false, - "assertionTesting": { - "enabled": true, - "testViewMethods": false, - "panicCodeConfig": { - "failOnCompilerInsertedPanic": false, - "failOnAssertion": true, - "failOnArithmeticUnderflow": false, - "failOnDivideByZero": false, - "failOnEnumTypeConversionOutOfBounds": false, - "failOnIncorrectStorageAccess": false, - "failOnPopEmptyArray": false, - "failOnOutOfBoundsArrayAccess": false, - "failOnAllocateTooMuchMemory": false, - "failOnCallUninitializedVariable": false - } - }, - "propertyTesting": { - "enabled": true, - "testPrefixes": [ - "echidna_" - ] - }, - "optimizationTesting": { - "enabled": false, - "testPrefixes": [ - "optimize_" - ] - } - }, - "chainConfig": { - "codeSizeCheckDisabled": true, - "cheatCodes": { - "cheatCodesEnabled": true, - "enableFFI": false - } - } - }, - "compilation": { - "platform": "crytic-compile", - "platformConfig": { - "target": ".", - "solcVersion": "", - "exportDirectory": "", - "args": [] - } - }, - "logging": { - "level": "info", - "logDirectory": "", - "noColor": false - } -} \ No newline at end of file + "fuzzing": { + "workers": 10, + "workerResetLimit": 50, + "timeout": 0, + "testLimit": 0, + "callSequenceLength": 100, + "corpusDirectory": "", + "coverageEnabled": true, + "targetContracts": [], + "targetContractsBalances": [], + "constructorArgs": {}, + "deployerAddress": "0x30000", + "senderAddresses": ["0x10000", "0x20000", "0x30000"], + "blockNumberDelayMax": 60480, + "blockTimestampDelayMax": 604800, + "blockGasLimit": 125000000, + "transactionGasLimit": 12500000, + "testing": { + "stopOnFailedTest": true, + "stopOnFailedContractMatching": false, + "stopOnNoTests": true, + "testAllContracts": false, + "traceAll": false, + "assertionTesting": { + "enabled": true, + "testViewMethods": false, + "panicCodeConfig": { + "failOnCompilerInsertedPanic": false, + "failOnAssertion": true, + "failOnArithmeticUnderflow": false, + "failOnDivideByZero": false, + "failOnEnumTypeConversionOutOfBounds": false, + "failOnIncorrectStorageAccess": false, + "failOnPopEmptyArray": false, + "failOnOutOfBoundsArrayAccess": false, + "failOnAllocateTooMuchMemory": false, + "failOnCallUninitializedVariable": false + } + }, + "propertyTesting": { + "enabled": true, + "testPrefixes": ["echidna_"] + }, + "optimizationTesting": { + "enabled": false, + "testPrefixes": ["optimize_"] + } + }, + "chainConfig": { + "codeSizeCheckDisabled": true, + "cheatCodes": { + "cheatCodesEnabled": true, + "enableFFI": false + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + }, + "logging": { + "level": "info", + "logDirectory": "", + "noColor": false + } +} diff --git a/program-analysis/echidna/exercises/exercise1/medusa.json b/program-analysis/echidna/exercises/exercise1/medusa.json index ede08d68..f75ee1d6 100644 --- a/program-analysis/echidna/exercises/exercise1/medusa.json +++ b/program-analysis/echidna/exercises/exercise1/medusa.json @@ -1,21 +1,19 @@ { - "fuzzing": { - "testing": { - "propertyTesting": { - "enabled": true, - "testPrefixes": [ - "echidna_" - ] - } - } - }, - "compilation": { - "platform": "crytic-compile", - "platformConfig": { - "target": ".", - "solcVersion": "", - "exportDirectory": "", - "args": [] - } - } + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": ["echidna_"] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } } diff --git a/program-analysis/echidna/exercises/exercise2/medusa.json b/program-analysis/echidna/exercises/exercise2/medusa.json index ede08d68..f75ee1d6 100644 --- a/program-analysis/echidna/exercises/exercise2/medusa.json +++ b/program-analysis/echidna/exercises/exercise2/medusa.json @@ -1,21 +1,19 @@ { - "fuzzing": { - "testing": { - "propertyTesting": { - "enabled": true, - "testPrefixes": [ - "echidna_" - ] - } - } - }, - "compilation": { - "platform": "crytic-compile", - "platformConfig": { - "target": ".", - "solcVersion": "", - "exportDirectory": "", - "args": [] - } - } + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": ["echidna_"] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } } diff --git a/program-analysis/echidna/exercises/exercise3/medusa.json b/program-analysis/echidna/exercises/exercise3/medusa.json index ede08d68..f75ee1d6 100644 --- a/program-analysis/echidna/exercises/exercise3/medusa.json +++ b/program-analysis/echidna/exercises/exercise3/medusa.json @@ -1,21 +1,19 @@ { - "fuzzing": { - "testing": { - "propertyTesting": { - "enabled": true, - "testPrefixes": [ - "echidna_" - ] - } - } - }, - "compilation": { - "platform": "crytic-compile", - "platformConfig": { - "target": ".", - "solcVersion": "", - "exportDirectory": "", - "args": [] - } - } + "fuzzing": { + "testing": { + "propertyTesting": { + "enabled": true, + "testPrefixes": ["echidna_"] + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + } } diff --git a/program-analysis/echidna/exercises/exercise4/medusa.json b/program-analysis/echidna/exercises/exercise4/medusa.json index bb2a17a6..2e8644b6 100644 --- a/program-analysis/echidna/exercises/exercise4/medusa.json +++ b/program-analysis/echidna/exercises/exercise4/medusa.json @@ -1,80 +1,72 @@ { - "fuzzing": { - "workers": 10, - "workerResetLimit": 50, - "timeout": 0, - "testLimit": 0, - "callSequenceLength": 100, - "corpusDirectory": "", - "coverageEnabled": true, - "targetContracts": [], - "targetContractsBalances": [], - "constructorArgs": {}, - "deployerAddress": "0x30000", - "senderAddresses": [ - "0x10000", - "0x20000", - "0x30000" - ], - "blockNumberDelayMax": 60480, - "blockTimestampDelayMax": 604800, - "blockGasLimit": 125000000, - "transactionGasLimit": 12500000, - "testing": { - "stopOnFailedTest": true, - "stopOnFailedContractMatching": false, - "stopOnNoTests": true, - "testAllContracts": false, - "traceAll": false, - "assertionTesting": { - "enabled": true, - "testViewMethods": false, - "panicCodeConfig": { - "failOnCompilerInsertedPanic": false, - "failOnAssertion": true, - "failOnArithmeticUnderflow": false, - "failOnDivideByZero": false, - "failOnEnumTypeConversionOutOfBounds": false, - "failOnIncorrectStorageAccess": false, - "failOnPopEmptyArray": false, - "failOnOutOfBoundsArrayAccess": false, - "failOnAllocateTooMuchMemory": false, - "failOnCallUninitializedVariable": false - } - }, - "propertyTesting": { - "enabled": true, - "testPrefixes": [ - "property_" - ] - }, - "optimizationTesting": { - "enabled": true, - "testPrefixes": [ - "optimize_" - ] - } - }, - "chainConfig": { - "codeSizeCheckDisabled": true, - "cheatCodes": { - "cheatCodesEnabled": true, - "enableFFI": false - } - } - }, - "compilation": { - "platform": "crytic-compile", - "platformConfig": { - "target": ".", - "solcVersion": "", - "exportDirectory": "", - "args": [] - } - }, - "logging": { - "level": "info", - "logDirectory": "", - "noColor": false - } -} \ No newline at end of file + "fuzzing": { + "workers": 10, + "workerResetLimit": 50, + "timeout": 0, + "testLimit": 0, + "callSequenceLength": 100, + "corpusDirectory": "", + "coverageEnabled": true, + "targetContracts": [], + "targetContractsBalances": [], + "constructorArgs": {}, + "deployerAddress": "0x30000", + "senderAddresses": ["0x10000", "0x20000", "0x30000"], + "blockNumberDelayMax": 60480, + "blockTimestampDelayMax": 604800, + "blockGasLimit": 125000000, + "transactionGasLimit": 12500000, + "testing": { + "stopOnFailedTest": true, + "stopOnFailedContractMatching": false, + "stopOnNoTests": true, + "testAllContracts": false, + "traceAll": false, + "assertionTesting": { + "enabled": true, + "testViewMethods": false, + "panicCodeConfig": { + "failOnCompilerInsertedPanic": false, + "failOnAssertion": true, + "failOnArithmeticUnderflow": false, + "failOnDivideByZero": false, + "failOnEnumTypeConversionOutOfBounds": false, + "failOnIncorrectStorageAccess": false, + "failOnPopEmptyArray": false, + "failOnOutOfBoundsArrayAccess": false, + "failOnAllocateTooMuchMemory": false, + "failOnCallUninitializedVariable": false + } + }, + "propertyTesting": { + "enabled": true, + "testPrefixes": ["property_"] + }, + "optimizationTesting": { + "enabled": true, + "testPrefixes": ["optimize_"] + } + }, + "chainConfig": { + "codeSizeCheckDisabled": true, + "cheatCodes": { + "cheatCodesEnabled": true, + "enableFFI": false + } + } + }, + "compilation": { + "platform": "crytic-compile", + "platformConfig": { + "target": ".", + "solcVersion": "", + "exportDirectory": "", + "args": [] + } + }, + "logging": { + "level": "info", + "logDirectory": "", + "noColor": false + } +}