for PR (aave-dao#7) (aave-dao#8)

Co-authored-by: Nissan Levi <[email protected]>
bgd-labs · Sep 19, 2024 · 7b520b5 · 7b520b5
1 parent 6ca003d
commit 7b520b5
Show file tree

Hide file tree

Showing 10 changed files with 410 additions and 1 deletion.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -0,0 +1,54 @@
+name: certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: "11", java-package: jre }
+
+      - name: Install certora cli
+        run: pip3 install certora-cli==7.6.3
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.19
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          cd certora
+          touch applyHarness.patch
+          make munged
+          cd ..
+          certoraRun certora/confs/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - rules.conf
diff --git a/README.md b/README.md
@@ -68,7 +68,7 @@ Some assets/oracles can also be restricted on the RiskStewards by calling the `s
 
 ## Security
 
-- Certora security review: [TBA](./)
+- Certora security review: [2024-07-10](./audits/10-07-2024_Certora_AaveV3-Risk-Steward.pdf)
 
 <br>
 

diff --git a/audits/10-07-2024_Certora_AaveV3-Risk-Steward.pdf b/audits/10-07-2024_Certora_AaveV3-Risk-Steward.pdf
diff --git a/certora/Makefile b/certora/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/applyHarness.patch b/certora/applyHarness.patch
@@ -0,0 +1,19 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1970-01-01 02:00:00.000000000 +0200
++++ .gitignore	2024-06-17 10:50:45.283021293 +0300
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+\ No newline at end of file
+diff -ruN src/contracts/RiskSteward.sol src/contracts/RiskSteward.sol
+--- src/contracts/RiskSteward.sol	2024-06-17 10:54:27.077860868 +0300
++++ src/contracts/RiskSteward.sol	2024-06-17 10:52:52.726709896 +0300
+@@ -110,7 +110,7 @@
+   /// @inheritdoc IRiskSteward
+   function setRiskConfig(Config calldata riskConfig) external onlyOwner {
+     _riskConfig = riskConfig;
+-    emit RiskConfigSet(riskConfig);
++    //    emit RiskConfigSet(riskConfig);
+   }
+
+   /// @inheritdoc IRiskSteward
diff --git a/certora/confs/rules.conf b/certora/confs/rules.conf
@@ -0,0 +1,35 @@
+{
+    "files": [
+        "certora/munged/src/contracts/RiskSteward.sol",
+        "lib/protocol-v3.1-upgrade/lib/aave-v3-origin/src/periphery/contracts/v3-config-engine/AaveV3ConfigEngine.sol",
+    ],
+    "link": [
+        "RiskSteward:CONFIG_ENGINE=AaveV3ConfigEngine",
+    ],
+    "packages": [
+                "ds-test=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/forge-std/lib/ds-test/src",
+                "forge-std=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/forge-std/src",
+                "aave-v3-origin=lib/protocol-v3.1-upgrade/lib/aave-v3-origin/src",
+                "aave-helpers=lib/protocol-v3.1-upgrade/lib/aave-helpers/src",
+                "aave-address-book=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/src",
+                "solidity-utils=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/solidity-utils/src",
+                "lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book:aave-v3-core=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-core",
+                "lib/aave-helpers/lib/aave-address-book:aave-v3-core=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-core",
+                "aave-capo=lib/aave-capo/src",
+                "lib/aave-capo:cl-synchronicity-price-adapter=lib/aave-capo/lib/cl-synchronicity-price-adapter/src",
+                "@aave/core-v3=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-core",
+                "@aave/periphery-v3=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-periphery",
+                "aave-v3-core=lib/protocol-v3.1-upgrade/lib/aave-v3-origin/src/core",
+                "aave-v3-periphery=lib/protocol-v3.1-upgrade/lib/aave-v3-origin/src/periphery",
+                "protocol-v3.1-upgrade=lib/protocol-v3.1-upgrade"
+                ],
+   "optimistic_loop": true,
+   "loop_iter": "2",
+   "rule_sanity": "basic",
+   "prover_args": ["-depth 15","-mediumTimeout 1000"],
+   "smt_timeout": "2000",
+   "solc": "solc8.19",
+   "verify": "RiskSteward:certora/specs/rules.spec",
+   "cache" :"none",
+   "msg": "RISK-STEWARD::rules"
+}
diff --git a/certora/confs/sanity.conf b/certora/confs/sanity.conf
@@ -0,0 +1,29 @@
+{
+    "files": [
+        "certora/munged/src/contracts/RiskSteward.sol",
+    ],
+    "packages": [
+                "ds-test=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/forge-std/lib/ds-test/src",
+                "forge-std=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/forge-std/src",
+                "aave-v3-origin=lib/protocol-v3.1-upgrade/lib/aave-v3-origin/src",
+                "aave-helpers=lib/protocol-v3.1-upgrade/lib/aave-helpers/src",
+                "aave-address-book=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/src",
+                "solidity-utils=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/solidity-utils/src",
+                "lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book:aave-v3-core=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-core",
+                "lib/aave-helpers/lib/aave-address-book:aave-v3-core=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-core",
+                "aave-capo=lib/aave-capo/src",
+                "lib/aave-capo:cl-synchronicity-price-adapter=lib/aave-capo/lib/cl-synchronicity-price-adapter/src",
+                "@aave/core-v3=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-core",
+                "@aave/periphery-v3=lib/protocol-v3.1-upgrade/lib/aave-helpers/lib/aave-address-book/lib/aave-v3-periphery",
+                "aave-v3-core=lib/protocol-v3.1-upgrade/lib/aave-v3-origin/src/core",
+                "aave-v3-periphery=lib/protocol-v3.1-upgrade/lib/aave-v3-origin/src/periphery",
+                "protocol-v3.1-upgrade=lib/protocol-v3.1-upgrade"
+                ],
+    "optimistic_loop": true,
+   "prover_args": ["-depth 15","-mediumTimeout 1000"],
+    "smt_timeout": "2000",
+    "solc": "solc8.19",
+    "verify": "RiskSteward:certora/specs/sanity.spec",
+    "cache" :"none",
+    "msg": "RISK-STEWARD::sanity"
+}
diff --git a/certora/munged/.gitignore b/certora/munged/.gitignore
@@ -0,0 +1,2 @@
+*
+!.gitignore