Initial medusa support for the CI

.github/workflows/examples.yaml → .github/workflows/echidna.yaml

@@ -1,4 +1,4 @@
-name: Test examples
+name: Test examples using Echidna
 
 on:
   push:

.github/workflows/medusa.yaml

@@ -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

CONTRIBUTING.md

@@ -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
 

README.md

@@ -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`
@@ -118,6 +118,8 @@ contract CryticTokenMock is MyToken, PropertiesConstants {
 
 #### Configuration
 
+**Echidna**
+
 Create the following Echidna config file
 
 ```yaml
@@ -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
 
@@ -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

tests/ERC20/foundry/medusa-config-ext.json

@@ -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
+	}
+}