Skip to content

Commit

Permalink
Merge pull request #36 from crytic/dev-medusa
Browse files Browse the repository at this point in the history
Initial medusa support for the CI
  • Loading branch information
ggrieco-tob authored May 29, 2024
2 parents 61133a7 + 4f3ca42 commit f1ff61b
Show file tree
Hide file tree
Showing 10 changed files with 615 additions and 13 deletions.
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: Test examples
name: Test examples using Echidna

on:
push:
Expand Down
117 changes: 117 additions & 0 deletions .github/workflows/medusa.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
name: Test examples using Medusa

on:
push:
branches:
- main
pull_request:
branches:
- "*"

env:
FOUNDRY_PROFILE: ci

jobs:
foundry:
name: Test Foundry examples
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v3
with:
submodules: recursive

- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1

- 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: Compile ERC20 Foundry example
working-directory: tests/ERC20/foundry
run: forge build --build-info

- name: Run Medusa for Internal ERC20 tests
working-directory: tests/ERC20/foundry
run: |
medusa fuzz --target-contracts CryticERC20InternalHarness --config medusa-config.json
- name: Run Medusa for External ERC20 tests
working-directory: tests/ERC20/foundry
run: |
medusa fuzz --target-contracts CryticERC20ExternalHarness --config medusa-config-ext.json
- name: Compile ERC4646 Foundry example
working-directory: tests/ERC4626/foundry
run: forge build --build-info

- name: Run Medusa for External ERC4626 tests
working-directory: tests/ERC4626/foundry
run: |
medusa fuzz --target-contracts CryticERC4626InternalHarness --config medusa-config.json
hardhat:
name: Test Hardhat examples
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v3
with:
submodules: recursive

- name: Set up Nodejs
uses: actions/setup-node@v3
with:
node-version: 16

- name: Install dependencies and compile ERC20 example
working-directory: tests/ERC20/hardhat
run: |
npm ci
npx hardhat compile --force
- name: Install dependencies and compile ERC4626 example
working-directory: tests/ERC4626/hardhat
run: |
npm ci
npx hardhat compile --force
- 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
working-directory: tests/ERC20/hardhat
run: |
medusa fuzz --target-contracts CryticERC20InternalHarness --config medusa-config.json
- name: Run Medusa for External ERC20 tests
working-directory: tests/ERC20/hardhat
run: |
medusa fuzz --target-contracts CryticERC20ExternalHarness --config medusa-config-ext.json
- name: Run Medusa for External ERC4626 tests
working-directory: tests/ERC4626/hardhat
run: |
medusa fuzz --target-contracts CryticERC4626Harness --config medusa-config.json
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Bug reports and feature suggestions can be submitted to our issue tracker. For b

## Questions

Questions can be submitted to the issue tracker, but you may get a faster response if you ask in our [chat room](https://slack.empirehacking.nyc/) (in the #ethereum channel).
Questions can be submitted to the issue tracker, but you may get a faster response if you ask in our [chat room](https://slack.empirehacking.nyc) (in the #ethereum channel).

## Code

Expand Down
65 changes: 54 additions & 11 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,11 @@ The goals of these properties are to:
- Ensure adherence to relevant standards
- Provide educational guidance for writing invariants

The properties can be used through unit tests or through fuzzing with [Echidna](https://github.com/crytic/echidna).
The properties can be used through unit tests or through fuzzing with [Echidna](https://github.com/crytic/echidna) or [Medusa](https://github.com/crytic/medusa).

## Testing the properties with fuzzing

1. Install [Echidna](https://github.com/crytic/echidna#installation).
1. Install [Echidna](https://github.com/crytic/echidna#installation) or [Medusa](https://github.com/crytic/medusa/blob/master/docs/src/getting_started/installation.md#installation).
2. Import the properties into to your project:

- In case of using Hardhat, use: `npm install https://github.com/crytic/properties.git` or `yarn add https://github.com/crytic/properties.git`
Expand Down Expand Up @@ -118,6 +118,8 @@ contract CryticTokenMock is MyToken, PropertiesConstants {

#### Configuration

**Echidna**

Create the following Echidna config file

```yaml
Expand All @@ -126,26 +128,67 @@ testMode: assertion
testLimit: 100000
deployer: "0x10000"
sender: ["0x10000", "0x20000", "0x30000"]
# Uncomment the following line for external testing
#allContracts: true
```

If you're using external testing, you will also need to specify:
```yaml
allContracts: true
**Medusa**

Create the following Medusa config file:

```json
{
"fuzzing": {
"testLimit": 100000,
"corpusDirectory": "tests/medusa-corpus",
"deployerAddress": "0x10000",
"senderAddresses": [
"0x10000",
"0x20000",
"0x30000"
],
"assertionTesting": {
"enabled": true
},
"propertyTesting": {
"enabled": false
},
"optimizationTesting": {
"enabled": false,
},
},
// Uncomment the following lines for external testing
// "testing": {
// "testAllContracts": true
// },
"compilation": {
"platform": "crytic-compile",
"platformConfig": {
"target": ".",
"solcVersion": "",
"exportDirectory": "",
"args": ["--foundry-compile-all"]
}
}
}
```

To perform more than one test, save the files with a descriptive path, to identify what test each file or corpus belongs to. For these examples, we use `tests/crytic/erc20/echidna-internal.yaml` and `tests/crytic/erc20/echidna-external.yaml` for the Echidna tests for ERC20. We recommended to modify the `corpusDir` for external tests accordingly.
To perform more than one test, save the files with a descriptive path, to identify what test each file or corpus belongs to. For instace, for these examples, we use `tests/crytic/erc20/echidna-internal.yaml` and `tests/crytic/erc20/echidna-external.yaml` for the Echidna tests for ERC20. We recommended to modify the corpus directory config opction for external tests accordingly.

The above configuration will start Echidna in assertion mode. Contract will be deployed from address `0x10000`, and transactions will be sent from the owner and two different users (`0x20000` and `0x30000`). There is an initial limit of `100000` tests, but depending on the token code complexity, this can be increased. Finally, once Echidna finishes the fuzzing campaign, corpus and coverage results will be available in the `tests/crytic/erc20/echidna-corpus-internal` directory.
The above configuration will start Echidna or Medusa in assertion mode. The target contract(s) will be deployed from address `0x10000`, and transactions will be sent from the owner as well as two different users (`0x20000` and `0x30000`). There is an initial limit of `100000` tests, but depending on the token code complexity, this can be increased. Finally, once our fuzzing tools finish the fuzzing campaign, corpus and coverage results will be available in the specified corpus directory.

#### Run

Run Echidna:
**Echidna**

- For internal testing: `echidna . --contract CryticERC20InternalHarness --config tests/crytic/erc20/echidna-internal.yaml`
- For external testing: `echidna . --contract CryticERC20ExternalHarness --config tests/crytic/erc20/echidna-external.yaml`

Finally, inspect the coverage report in `tests/crytic/erc20/echidna-corpus-internal` or `tests/crytic/erc20/echidna-corpus-external` when it finishes.
**Medusa**

- Go to the directory `cd tests/crytic/erc20`
- For internal testing: `medusa fuzz --target-contracts CryticERC20InternalHarness --config medusa-internal.yaml`
- For external testing: `medusa fuzz --target-contracts CryticERC20ExternalHarness --config medusa-external.yaml`

#### Example: Output for a compliant token

Expand Down Expand Up @@ -417,7 +460,7 @@ Run the test suite using `echidna . --contract CryticABDKMath64x64Harness --seq-
## Additional resources

- [Building secure contracts](https://secure-contracts.com/program-analysis/index.html)
- Our [EmpireSlacking](https://slack.empirehacking.nyc/) slack server, channel #ethereum
- Our [EmpireSlacking](https://slack.empirehacking.nyc) slack server, channel #ethereum
- Watch our [fuzzing workshop](https://www.youtube.com/watch?v=QofNQxW_K08&list=PLciHOL_J7Iwqdja9UH4ZzE8dP1IxtsBXI)

# Helper functions
Expand Down
80 changes: 80 additions & 0 deletions tests/ERC20/foundry/medusa-config-ext.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
{
"fuzzing": {
"workers": 10,
"workerResetLimit": 50,
"timeout": 0,
"testLimit": 500000,
"callSequenceLength": 100,
"corpusDirectory": "tests/medusa-corpus-ext",
"coverageEnabled": true,
"targetContracts": [],
"targetContractsBalances": [],
"constructorArgs": {},
"deployerAddress": "0x10000",
"senderAddresses": [
"0x10000",
"0x20000",
"0x30000"
],
"blockNumberDelayMax": 60480,
"blockTimestampDelayMax": 604800,
"blockGasLimit": 125000000,
"transactionGasLimit": 12500000,
"testing": {
"stopOnFailedTest": true,
"stopOnFailedContractMatching": false,
"stopOnNoTests": true,
"testAllContracts": true,
"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": false,
"testPrefixes": [
"property_"
]
},
"optimizationTesting": {
"enabled": false,
"testPrefixes": [
"optimize_"
]
}
},
"chainConfig": {
"codeSizeCheckDisabled": true,
"cheatCodes": {
"cheatCodesEnabled": true,
"enableFFI": false
}
}
},
"compilation": {
"platform": "crytic-compile",
"platformConfig": {
"target": ".",
"solcVersion": "",
"exportDirectory": "",
"args": ["--foundry-compile-all"]
}
},
"logging": {
"level": "info",
"logDirectory": "",
"noColor": false
}
}
Loading

0 comments on commit f1ff61b

Please sign in to comment.