ci: Certora Review of Modular Gho Steward (#423)

aave · Sep 16, 2024 · f58767b · f58767b
1 parent c82c63b
commit f58767b
Show file tree

Hide file tree

Showing 17 changed files with 802 additions and 168 deletions.
diff --git a/.github/workflows/certora-steward.yml b/.github/workflows/certora-steward.yml
@@ -32,6 +32,10 @@ jobs:
 
       - name: Install solc
         run: |
+          cd certora/steward/
+          touch applyHarness.patch
+          make munged
+          cd ../..
           wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
           chmod +x solc-static-linux
           sudo mv solc-static-linux /usr/local/bin/solc8.10
@@ -48,4 +52,8 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - rules.conf
+          - GhoAaveSteward.conf
+          - GhoBucketSteward.conf
+          - GhoCcipSteward.conf
+          - GhoGsmSteward.conf
+
diff --git a/audits/15-09-2024_Modular_Gho_Steward_Certora.pdf b/audits/15-09-2024_Modular_Gho_Steward_Certora.pdf
diff --git a/certora/steward/Makefile b/certora/steward/Makefile
@@ -0,0 +1,28 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../../src
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	mkdir $@
+	cp -r ../../src $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	mkdir tmp
+	cp -r ../../src tmp
+	diff -ruN tmp $(MUNGED_DIR) | sed 's+tmp/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH)
+	rm -rf tmp
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+
diff --git a/certora/steward/applyHarness.patch b/certora/steward/applyHarness.patch
@@ -0,0 +1,7 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1970-01-01 02:00:00.000000000 +0200
++++ .gitignore	2024-08-12 17:28:45.843705526 +0300
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+\ No newline at end of file
diff --git a/certora/steward/conf/GhoAaveSteward.conf b/certora/steward/conf/GhoAaveSteward.conf
@@ -0,0 +1,27 @@
+{
+    "files": ["certora/steward/harness/GhoAaveSteward_Harness.sol"],
+    "packages": [
+                "@aave/core-v3/=lib/aave-v3-core",
+                "@aave/periphery-v3/=lib/aave-v3-periphery",
+                "@aave/=lib/aave-token",
+                "@openzeppelin/=lib/openzeppelin-contracts",
+                "aave-stk-v1-5/=lib/aave-stk-v1-5",
+                "ds-test/=lib/forge-std/lib/ds-test/src",
+                "forge-std/=lib/forge-std/src",
+                "aave-address-book/=lib/aave-address-book/src",
+                "aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers",
+                "aave-v3-core/=lib/aave-address-book/lib/aave-v3-core",
+                "erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests",
+                "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
+                "solidity-utils/=lib/solidity-utils/src"
+    ],
+    "build_cache": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": ["-depth 15","-mediumTimeout 1000"],
+    "smt_timeout": "2000",
+    "solc": "solc8.10",
+    "verify": "GhoAaveSteward_Harness:certora/steward/specs/GhoAaveSteward.spec",
+    "rule_sanity": "basic",
+    "msg": "GhoAaveSteward: all rules"
+}
diff --git a/certora/steward/conf/rules.conf → certora/steward/conf/GhoBucketSteward.conf b/certora/steward/conf/rules.conf → certora/steward/conf/GhoBucketSteward.conf
@@ -1,10 +1,6 @@
 {
     "files": [
-        "certora/steward/harness/GhoStewardV2_Harness.sol",
-        "src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol"
-    ],
-    "link": [
-        "GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory",
+        "src/contracts/misc/GhoBucketSteward.sol"
     ],
     "packages": [
                 "@aave/core-v3/=lib/aave-v3-core",
@@ -21,12 +17,13 @@
                 "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
                 "solidity-utils/=lib/solidity-utils/src"
     ],
+    "build_cache": true,
     "optimistic_loop": true,
     "process": "emv",
     "prover_args": ["-depth 15","-mediumTimeout 1000"],
     "smt_timeout": "2000",
     "solc": "solc8.10",
-    "verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec",
+    "verify": "GhoBucketSteward:certora/steward/specs/GhoBucketSteward.spec",
     "rule_sanity": "basic",
-    "msg": "STEWARD: all rules"
+    "msg": "GhoBucketSteward: all rules"
 }
diff --git a/certora/steward/conf/GhoCcipSteward.conf b/certora/steward/conf/GhoCcipSteward.conf
@@ -0,0 +1,27 @@
+{
+    "files": ["certora/steward/harness/GhoCcipSteward_Harness.sol"],
+    "packages": [
+                "@aave/core-v3/=lib/aave-v3-core",
+                "@aave/periphery-v3/=lib/aave-v3-periphery",
+                "@aave/=lib/aave-token",
+                "@openzeppelin/=lib/openzeppelin-contracts",
+                "aave-stk-v1-5/=lib/aave-stk-v1-5",
+                "ds-test/=lib/forge-std/lib/ds-test/src",
+                "forge-std/=lib/forge-std/src",
+                "aave-address-book/=lib/aave-address-book/src",
+                "aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers",
+                "aave-v3-core/=lib/aave-address-book/lib/aave-v3-core",
+                "erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests",
+                "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
+                "solidity-utils/=lib/solidity-utils/src"
+    ],
+    "build_cache": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": ["-depth 15","-mediumTimeout 1000"],
+    "smt_timeout": "2000",
+    "solc": "solc8.10",
+    "verify": "GhoCcipSteward_Harness:certora/steward/specs/GhoCcipSteward.spec",
+    "rule_sanity": "basic",
+    "msg": "GhoCcipSteward: all rules"
+}
diff --git a/certora/steward/conf/sanity.conf → certora/steward/conf/GhoGsmSteward.conf b/certora/steward/conf/sanity.conf → certora/steward/conf/GhoGsmSteward.conf
@@ -1,10 +1,10 @@
 {
     "files": [
-        "certora/steward/harness/GhoStewardV2_Harness.sol",
-        "src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol"
+        "certora/steward/harness/GhoGsmSteward_Harness.sol",
+        "src/contracts/facilitators/gsm/feeStrategy/FixedFeeStrategyFactory.sol"
     ],
     "link": [
-        "GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory",
+        "GhoGsmSteward_Harness:FIXED_FEE_STRATEGY_FACTORY=FixedFeeStrategyFactory",
     ],
     "packages": [
                 "@aave/core-v3/=lib/aave-v3-core",
@@ -21,13 +21,13 @@
                 "openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
                 "solidity-utils/=lib/solidity-utils/src"
     ],
+    "build_cache": true,
     "optimistic_loop": true,
-    "prover_args": ["-depth 15","-mediumTimeout 1000","-cache none"],
+    "process": "emv",
+    "prover_args": ["-depth 15","-mediumTimeout 1000"],
     "smt_timeout": "2000",
     "solc": "solc8.10",
-    "verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec",
-    "rule": ["sanity"],
-    "disable_auto_cache_key_gen" :true,
-    "cache" :"none",
-    "msg": "STEWARD::sanity"
+    "verify": "GhoGsmSteward_Harness:certora/steward/specs/GhoGsmSteward.spec",
+    "rule_sanity": "basic",
+    "msg": "GhoGsmSteward: all rules"
 }
diff --git a/certora/steward/harness/GhoAaveSteward_Harness.sol b/certora/steward/harness/GhoAaveSteward_Harness.sol
@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.10;
+
+import {GhoAaveSteward} from '../munged/src/contracts/misc/GhoAaveSteward.sol';
+
+contract GhoAaveSteward_Harness is GhoAaveSteward {
+  constructor(
+    address owner,
+    address addressesProvider,
+    address poolDataProvider,
+    address ghoToken,
+    address riskCouncil,
+    BorrowRateConfig memory borrowRateConfig
+  )
+    GhoAaveSteward(
+      owner,
+      addressesProvider,
+      poolDataProvider,
+      ghoToken,
+      riskCouncil,
+      borrowRateConfig
+    )
+  {}
+}
diff --git a/certora/steward/harness/GhoCcipSteward_Harness.sol b/certora/steward/harness/GhoCcipSteward_Harness.sol
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.10;
+
+import {GhoCcipSteward} from '../../../src/contracts/misc/GhoCcipSteward.sol';
+
+contract GhoCcipSteward_Harness is GhoCcipSteward {
+  constructor(
+    address ghoToken,
+    address ghoTokenPool,
+    address riskCouncil,
+    bool bridgeLimitEnabled
+  ) GhoCcipSteward(ghoToken, ghoTokenPool, riskCouncil, bridgeLimitEnabled) {}
+
+  function getCcipTimelocks() external view returns (CcipDebounce memory) {
+    return _ccipTimelocks;
+  }
+
+
+}
diff --git a/certora/steward/harness/GhoGsmSteward_Harness.sol b/certora/steward/harness/GhoGsmSteward_Harness.sol
@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.10;
+
+import {GhoGsmSteward} from '../../../src/contracts/misc/GhoGsmSteward.sol';
+
+contract GhoGsmSteward_Harness is GhoGsmSteward {
+  constructor(
+    address fixedRateStrategyFactory,
+    address riskCouncil
+  ) GhoGsmSteward(fixedRateStrategyFactory, riskCouncil) {}
+}
diff --git a/certora/steward/harness/GhoStewardV2_Harness.sol b/certora/steward/harness/GhoStewardV2_Harness.sol
@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.10;
+
+import {GhoStewardV2} from '../../../src/contracts/misc/GhoStewardV2.sol';
+
+contract GhoStewardV2_Harness is GhoStewardV2 {
+  constructor(
+    address owner,
+    address addressesProvider,
+    address ghoToken,
+    address fixedRateStrategyFactory,
+    address riskCouncil
+  ) GhoStewardV2(owner, addressesProvider, ghoToken, fixedRateStrategyFactory, riskCouncil) {}
+
+  function get_gsmFeeStrategiesByRates(
+    uint256 buyFee,
+    uint256 sellFee
+  ) external view returns (address) {
+    return _gsmFeeStrategiesByRates[buyFee][sellFee];
+  }
+}
diff --git a/certora/steward/munged/.gitignore b/certora/steward/munged/.gitignore
@@ -0,0 +1,2 @@
+*
+!.gitignore