feat: Add Certora Review and FV CI (#88)

* Certora Review (#87) Co-authored-by: Michael M <[email protected]> * docs: Add Certora audit to README * docs: Update Certora audit report * fix: Remove remaining comments from previous iterations of specs * docs: Update audit report of Certora --------- Co-authored-by: Nissan Levi <[email protected]> Co-authored-by: Michael M <[email protected]>
aave · Jun 29, 2023 · 028d769 · 028d769
1 parent 23366cc
commit 028d769
Show file tree

Hide file tree

Showing 49 changed files with 3,169 additions and 0 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -0,0 +1,72 @@
+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: Check key
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+        run: echo "key length" ${#CERTORAKEY}
+
+      - 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==3.6.8.post3
+
+      - 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: |
+          cd certora
+          touch applyHarness.patch
+          make munged
+          cd ..
+          echo "key length" ${#CERTORAKEY}
+          certoraRun certora/conf/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - changeInContractBalanceShouldCauseAccrual.conf
+          - erc4626-previewOPERATIONS.conf
+          - fees_LEQ_ATokenBal.conf
+          - lastVaultBalance_LEQ_ATokenBalThis.conf
+          - positiveSupply_imply_positiveAssets-deposit.conf
+          - positiveSupply_imply_positiveAssets-mint.conf
+          - positiveSupply_imply_positiveAssets-other.conf
+          - positiveSupply_imply_positiveAssets-redeem.conf
+          - positiveSupply_imply_positiveAssets-withdraw.conf
+          - rayMul_rayDiv_mulDiv_properties.conf
+          - totalSupply_EQ_sumAllBal.conf
+          - accrueYieldCheck.conf
+
diff --git a/README.md b/README.md
@@ -63,6 +63,7 @@ You can find all audit reports under the audits folder
 
 - [01-03-2023 OpenZeppelin](./audits/01-03-2023_OpenZeppelin_Wrapped_AToken_Vault.pdf)
 - [03-03-2023 PeckShield](./audits/03-03-2023_Peckshield_Wrapped_AToken_Vault.pdf)
+- [18-06-2023 Certora](./certora/report/Aave-Vault-Formal-Verification.pdf)
 
 
 ## License

diff --git a/certora/Makefile b/certora/Makefile
@@ -0,0 +1,30 @@
+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 ../lib $@
+	cp -r ../src $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	mkdir tmp
+	cp -r ../lib 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,37 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1970-01-01 01:00:00.000000000 +0100
++++ .gitignore	2023-04-13 11:36:09.000000000 +0100
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+\ No newline at end of file
+diff -ruN lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol
+--- lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol	2023-04-16 05:13:16.000000000 +0100
++++ lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol	2023-04-11 14:54:24.000000000 +0100
+@@ -71,16 +71,16 @@
+
+     _domainSeparator = _calculateDomainSeparator();
+
+-    emit Initialized(
+-      underlyingAsset,
+-      address(POOL),
+-      treasury,
+-      address(incentivesController),
+-      aTokenDecimals,
+-      aTokenName,
+-      aTokenSymbol,
+-      params
+-    );
++    // emit Initialized(
++    //   underlyingAsset,
++    //   address(POOL),
++    //   treasury,
++    //   address(incentivesController),
++    //   aTokenDecimals,
++    //   aTokenName,
++    //   aTokenSymbol,
++    //   params
++    // );
+   }
+
+   /// @inheritdoc IAToken
diff --git a/certora/conf/accrueYieldCheck.conf b/certora/conf/accrueYieldCheck.conf
@@ -0,0 +1,42 @@
+{
+    "files": [
+        "certora/harness/ATokenVaultHarness.sol",
+        "certora/harness/DummyContract.sol",
+        "certora/harness/pool/SymbolicLendingPoolL1.sol",
+        "certora/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+        "certora/munged/lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol"
+    ],
+    "link": [
+        "AToken:POOL=SymbolicLendingPoolL1",
+        "AToken:_underlyingAsset=DummyERC20_aTokenUnderlying",
+        "ATokenVaultHarness:AAVE_POOL=SymbolicLendingPoolL1",
+        "ATokenVaultHarness:ATOKEN=AToken",
+        "ATokenVaultHarness:DUMMY=DummyContract",
+        "ATokenVaultHarness:UNDERLYING=DummyERC20_aTokenUnderlying",
+        "SymbolicLendingPoolL1:aToken=AToken",
+        "SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
+    ],
+    "packages": [
+        "@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
+        "@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
+        "@aave/core-v3=certora/munged/lib/aave-v3-core",
+        "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
+        "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
+    ],
+    "verify": ["ATokenVaultHarness:certora/specs/accrueYieldCheck.spec"],
+    "rule": ["accrueYieldCheck"],
+    "optimistic_loop": true,
+    "process": "emv",
+    "rule_sanity": "basic",
+    "settings": [
+        "-assumeUnwindCond",
+        "-depth=15",
+        "-mediumTimeout=1000",
+        "-ruleSanityChecks=basic",
+        "-t=2000"
+    ],
+    "smt_timeout": "2000",
+    "solc": "solc8.10",
+    "cloud": "" ,
+    "msg": "accrueYieldCheck"
+}
diff --git a/certora/conf/changeInContractBalanceShouldCauseAccrual.conf b/certora/conf/changeInContractBalanceShouldCauseAccrual.conf
@@ -0,0 +1,47 @@
+{
+    "files": [
+        "certora/harness/ATokenVaultHarness.sol",
+        "certora/harness/DummyContract.sol",
+        "certora/harness/pool/SymbolicLendingPoolL1.sol",
+        "certora/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+        "certora/munged/lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol"
+    ],
+    "link": [
+        "AToken:POOL=SymbolicLendingPoolL1",
+        "AToken:_underlyingAsset=DummyERC20_aTokenUnderlying",
+        "ATokenVaultHarness:AAVE_POOL=SymbolicLendingPoolL1",
+        "ATokenVaultHarness:ATOKEN=AToken",
+        "ATokenVaultHarness:DUMMY=DummyContract",
+        "ATokenVaultHarness:UNDERLYING=DummyERC20_aTokenUnderlying",
+        "SymbolicLendingPoolL1:aToken=AToken",
+        "SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
+    ],
+    "msg": "changeInContractBalanceShouldCauseAccrual",
+    "optimistic_loop": true,
+    "packages": [
+        "@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
+        "@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
+        "@aave/core-v3=certora/munged/lib/aave-v3-core",
+        "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
+        "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
+    ],
+    "process": "emv",
+    "rule": [
+        "changeInContractBalanceShouldCauseAccrual"
+    ],
+    "rule_sanity": "basic",
+    "settings": [
+        "-assumeUnwindCond",
+        "-depth=15",
+        "-mediumTimeout=1000",
+        "-rule=changeInContractBalanceShouldCauseAccrual",
+        "-ruleSanityChecks=basic",
+        "-t=2000"
+    ],
+    "smt_timeout": "2000",
+    "solc": "solc8.10",
+    "cloud": "" ,
+    "verify": [
+        "ATokenVaultHarness:certora/specs/changeInContractBalanceShouldCauseAccrual.spec"
+    ]
+}
diff --git a/certora/conf/erc4626-previewOPERATIONS.conf b/certora/conf/erc4626-previewOPERATIONS.conf
@@ -0,0 +1,44 @@
+{
+  "files": [
+    "certora/harness/ATokenVaultHarness.sol",
+    "certora/harness/DummyContract.sol",
+    "certora/harness/pool/SymbolicLendingPoolL1.sol",
+    "certora/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+    "certora/munged/lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol"
+  ],
+  "link": [
+    "AToken:POOL=SymbolicLendingPoolL1",
+    "AToken:_underlyingAsset=DummyERC20_aTokenUnderlying",
+    "ATokenVaultHarness:AAVE_POOL=SymbolicLendingPoolL1",
+    "ATokenVaultHarness:ATOKEN=AToken",
+    "ATokenVaultHarness:DUMMY=DummyContract",
+    "ATokenVaultHarness:UNDERLYING=DummyERC20_aTokenUnderlying",
+    "SymbolicLendingPoolL1:aToken=AToken",
+    "SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
+  ],
+  "optimistic_loop": true,
+  "packages": [
+    "@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
+    "@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
+    "@aave/core-v3=certora/munged/lib/aave-v3-core",
+    "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
+    "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
+  ],
+  "process": "emv",
+  "rule": [
+    "previewMint_amount_check","previewDeposit_amount_check","previewWithdraw_amount_check","previewRedeem_amount_check"
+  ],
+  "settings": [
+    "-assumeUnwindCond",
+    "-depth=15",
+    "-mediumTimeout=1000",
+    "-t=2000"
+  ],
+  "smt_timeout": "2000",
+  "solc": "solc8.10",
+  "cloud": "" ,
+  "verify": [
+    "ATokenVaultHarness:certora/specs/erc4626.spec"
+  ],
+  "msg": "previewOPERATION_amount_check"
+}
diff --git a/certora/conf/fees_LEQ_ATokenBal.conf b/certora/conf/fees_LEQ_ATokenBal.conf
@@ -0,0 +1,40 @@
+{
+    "files": [
+        "certora/harness/ATokenVaultHarness.sol",
+        "certora/harness/DummyContract.sol",
+        "certora/harness/pool/SymbolicLendingPoolL1.sol",
+        "certora/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+        "certora/munged/lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol"
+    ],
+    "link": [
+        "AToken:POOL=SymbolicLendingPoolL1",
+        "AToken:_underlyingAsset=DummyERC20_aTokenUnderlying",
+        "ATokenVaultHarness:AAVE_POOL=SymbolicLendingPoolL1",
+        "ATokenVaultHarness:ATOKEN=AToken",
+        "ATokenVaultHarness:DUMMY=DummyContract",
+        "ATokenVaultHarness:UNDERLYING=DummyERC20_aTokenUnderlying",
+        "SymbolicLendingPoolL1:aToken=AToken",
+        "SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
+    ],
+    "packages": [
+        "@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
+        "@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
+        "@aave/core-v3=certora/munged/lib/aave-v3-core",
+        "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
+        "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
+    ],
+    "cloud": "",
+    "optimistic_loop": true,
+    "process": "emv",
+    "settings": [
+        "-assumeUnwindCond",
+        "-depth=15",
+        "-mediumTimeout=1000",
+        "-t=2000"
+    ],
+    "smt_timeout": "2000",
+    "solc": "solc8.10",
+    "verify": ["ATokenVaultHarness:certora/specs/fees_LEQ_ATokenBal.spec"],
+    "rule": ["getCLMFees_LEQ_ATokenBAL_DM_other","getCLMFees_LEQ_ATokenBAL_RW"],
+    "msg": "getclaimablefees LEQ Atoken.Balanceof[Vault]"
+}
diff --git a/certora/conf/lastVaultBalance_LEQ_ATokenBalThis.conf b/certora/conf/lastVaultBalance_LEQ_ATokenBalThis.conf
@@ -0,0 +1,43 @@
+{
+  "disable_auto_cache_key_gen": true,
+  "files": [
+    "certora/harness/ATokenVaultHarness.sol",
+    "certora/harness/DummyContract.sol",
+    "certora/harness/pool/SymbolicLendingPoolL1.sol",
+    "certora/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+    "certora/munged/lib/aave-v3-core/contracts/protocol/tokenization/AToken.sol"
+  ],
+  "link": [
+    "AToken:POOL=SymbolicLendingPoolL1",
+    "AToken:_underlyingAsset=DummyERC20_aTokenUnderlying",
+    "ATokenVaultHarness:AAVE_POOL=SymbolicLendingPoolL1",
+    "ATokenVaultHarness:ATOKEN=AToken",
+    "ATokenVaultHarness:DUMMY=DummyContract",
+    "ATokenVaultHarness:UNDERLYING=DummyERC20_aTokenUnderlying",
+    "SymbolicLendingPoolL1:aToken=AToken",
+    "SymbolicLendingPoolL1:underlyingToken=DummyERC20_aTokenUnderlying"
+  ],
+  "packages": [
+    "@aave-v3-core=certora/munged/lib/aave-v3-core/contracts",
+    "@aave-v3-periphery=certora/munged/lib/aave-v3-periphery/contracts",
+    "@aave/core-v3=certora/munged/lib/aave-v3-core",
+    "@openzeppelin-upgradeable=certora/munged/lib/openzeppelin-contracts-upgradeable/contracts",
+    "@openzeppelin=certora/munged/lib/openzeppelin-contracts/contracts"
+  ],
+  "process": "emv",
+  "optimistic_loop": true,
+  "settings": [
+    "-assumeUnwindCond",
+    "-depth=15",
+    "-mediumTimeout=1000",
+    "-rule=lastVaultBalance_LEQ_ATokenBalThis",
+    "-t=2000"
+  ],
+  "smt_timeout": "2000",
+  "solc": "solc8.10",
+  "cloud": "" ,
+  "verify": ["ATokenVaultHarness:certora/specs/lastVaultBal_LEQ_ATokenBalThis.spec"],
+  "disableLocalTypeChecking": false,
+  "rule": ["lastVaultBalance_LEQ_ATokenBalThis"],
+  "msg": "_s.lastVaultBalance LEQ AToken.balance[this] accurate assertion"
+}