feat: Add Certora formal verification for GhoStewardV2 (#395)

* feat: Add Certora formal verification for GhoStewardV2 * fix: Fix format * docs: Add audit report for GhoStewardV2 * fix: Fix typo in certora files --------- Co-authored-by: Nissan Levi <[email protected]>
aave · Mar 20, 2024 · f02f874 · f02f874
1 parent eca2e77
commit f02f874
Show file tree

Hide file tree

Showing 22 changed files with 3,276 additions and 2 deletions.
diff --git a/.github/workflows/certora-steward.yml b/.github/workflows/certora-steward.yml
@@ -0,0 +1,51 @@
+name: certora-steward
+
+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: pip install certora-cli
+
+      - name: Install solc
+        run: |
+          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
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          echo "key length" ${#CERTORAKEY}
+          certoraRun certora/steward/conf/${{ 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
@@ -45,6 +45,7 @@ You can find all audit reports under the [audits](./audits/) folder
 - [2023-09-20 - Emanuele Ricci @Stermi (GHO Stability Module)](./audits/2023-09-20_GSM_Stermi.pdf)
 - [2023-10-23 - Sigma Prime (GHO Stability Module)](./audits/2023-10-23_GSM_SigmaPrime.pdf)
 - [2023-12-07 - Certora Formal Verification (GHO Stability Module)](./certora/reports/Formal_Verification_Report_of_GHO_Stability_Module.pdf)
+- [2024-03-14 - Certora Formal Verification (GhoStewardV2)](./audits/2024-03-14_GhoStewardV2_Certora.pdf)
 
 ## Getting Started
 

diff --git a/audits/2024-03-14_GhoStewardV2_Certora.pdf b/audits/2024-03-14_GhoStewardV2_Certora.pdf
diff --git a/certora/GSM/harness/FixedPriceStrategyHarness.sol b/certora/GSM/harness/FixedPriceStrategyHarness.sol
@@ -13,7 +13,7 @@ contract FixedPriceStrategyHarness is FixedPriceStrategy {
     return _underlyingAssetUnits;
   }
 
-  function getUnderlyginAssetDecimals() external view returns (uint256) {
+  function getUnderlyingAssetDecimals() external view returns (uint256) {
     return UNDERLYING_ASSET_DECIMALS;
   }