Certora + Community Formal Verification

.github/workflows/certora-erc20.yml

@@ -0,0 +1,58 @@
+name: certora-erc20
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+
+      - 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: pip install certora-cli
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.13/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.13
+      
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          cd certora
+          touch applyHarness.patch
+          make munged
+          cd ..
+          echo "key length" ${#CERTORAKEY}
+          sh certora/scripts/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - erc20.sh

.github/workflows/certora.yml

@@ -0,0 +1,60 @@
+name: certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+
+      - 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: pip install certora-cli
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.13/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.13
+      
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          cd certora
+          touch applyHarness.patch
+          make munged
+          cd ..
+          echo "key length" ${#CERTORAKEY}
+          sh certora/scripts/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - verifyGeneral.sh
+          - verifyDelegate.sh
+          - verifyCommunity.sh

.gitignore

@@ -4,3 +4,10 @@ out/
 node_modules
 package-lock.json
 .env
+
+# Certora
+.certora_config/
+.last_confs/
+.certora_*
+certora/munged
+resource_errors.json

certora/.gitignore

@@ -0,0 +1,5 @@
+# certora
+.certora*
+.certora*.json
+**.last_conf*
+certora-logs

certora/Makefile

@@ -0,0 +1,26 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../src
+LIB_DIR 	  = ../lib
+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 $@
+	cp -r $(CONTRACTS_DIR) $@
+	cp -r $(LIB_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -uN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+$(CONTRACTS_DIR)/++g' | sed 's+$(MUNGED_DIR)++g' > $(PATCH)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+

certora/README.md

@@ -0,0 +1,42 @@
+## Verification Overview
+The current directory contains Certora's formal verification of AAVE's V3 token.
+In this directory you will find three subdirectories:
+
+1. specs - Contains all the specification files that were written by Certora for the token code. We have created two spec files, `base.spec`, `delegate.spec`, `erc20.spec` and `general.spec`.
+- `base.spec` contains method declarations, CVL functions and definitions used by the main specification files
+- `delegate.spec` contains rules that prove various delegation properties
+- `erc20.spec` contains rules that prove ERC20 general rules, e.g. correctness of transfer and others
+- `general.spec` contains general delegation invariants, e.g. sum of delegated and undelegated balances equals to 
+total supply  
+
+2. scripts - Contains all the necessary run scripts to execute the spec files on the Certora Prover. These scripts composed of a run command of Certora Prover, contracts to take into account in the verification context, declaration of the compiler and a set of additional settings. 
+- `verifyDelegate.sh` is a script for running `delegate.spec`
+- `verifyGeneral.sh` is a script for running `general.spec`
+- `erc20.sh` is a script for running `erc20.spec`
+
+3. harness - Contains all the inheriting contracts that add/simplify functionalities to the original contract.
+We use two harnesses:
+- `AaveTokenV3Harness.sol` used by `erc20.sh` and `delegate.sh`. It inherits from the original AaveV3Token 
+contract and adds a few getter functions.
+
+- `AaveTokenV3HarnessStorage.sol` used by `general.sh`. It uses a modified a version of AaveV3Token contract
+where the `delegationState` field of the `_balances` struct is refactored to be of type uint8 instead of
+`DelegationState` enum. This is done in order to bypass a current limitation of the tool and write a hook
+on the `delegationState` field (hooks don't support enum fields at the moment)
+
+
+</br>
+
+---
+
+## Running Instructions
+To run a verification job:
+
+1. Open terminal and `cd` your way to the main aave-token-v3 directory
+
+2. Run the script you'd like to get results for:
+    ```
+    sh certora/scripts/verifyDelegate.sh
+    sh certora/scripts/verifyGeneral.sh
+    sh certora/scripts/erc20.sh
+    ```

certora/applyHarness.patch

@@ -0,0 +1,79 @@
+diff -uN AaveTokenV3.sol /AaveTokenV3.sol
+--- AaveTokenV3.sol	2022-10-11 16:03:49.000000000 +0300
++++ /AaveTokenV3.sol	2022-10-11 16:13:48.000000000 +0300
+@@ -210,7 +210,7 @@
+         fromBalanceAfter = fromUserState.balance - uint104(amount);
+       }
+       _balances[from].balance = fromBalanceAfter;
+-      if (fromUserState.delegationState != DelegationState.NO_DELEGATION) {
++      if (fromUserState.delegationState != uint8(DelegationState.NO_DELEGATION)) {
+         _governancePowerTransferByType(
+           fromUserState.balance,
+           fromBalanceAfter,
+@@ -232,7 +232,7 @@
+       toUserState.balance = toBalanceBefore + uint104(amount);
+       _balances[to] = toUserState;
+
+-      if (toUserState.delegationState != DelegationState.NO_DELEGATION) {
++      if (toUserState.delegationState != uint8(DelegationState.NO_DELEGATION)) {
+         _governancePowerTransferByType(
+           toBalanceBefore,
+           toUserState.balance,
+@@ -288,7 +288,7 @@
+           : address(0);
+     }
+     return
+-      userState.delegationState >= DelegationState.PROPOSITION_DELEGATED
++      userState.delegationState >= uint8(DelegationState.PROPOSITION_DELEGATED)
+         ? _propositionDelegateeV2[delegator]
+         : address(0);
+   }
+@@ -325,16 +325,12 @@
+   ) internal pure returns (DelegationAwareBalance memory) {
+     if (willDelegate) {
+       // Because GovernancePowerType starts from 0, we should add 1 first, then we apply bitwise OR
+-      userState.delegationState = DelegationState(
+-        uint8(userState.delegationState) | (uint8(delegationType) + 1)
+-      );
++      userState.delegationState = userState.delegationState | (uint8(delegationType) + 1);
+     } else {
+       // First bitwise NEGATION, ie was 01, after XOR with 11 will be 10,
+       // then bitwise AND, which means it will keep only another delegation type if it exists
+-      userState.delegationState = DelegationState(
+-        uint8(userState.delegationState) &
+-          ((uint8(delegationType) + 1) ^ uint8(DelegationState.FULL_POWER_DELEGATED))
+-      );
++      userState.delegationState = userState.delegationState &
++          ((uint8(delegationType) + 1) ^ uint8(DelegationState.FULL_POWER_DELEGATED));
+     }
+     return userState;
+   }
+diff -uN BaseAaveToken.sol /BaseAaveToken.sol
+--- BaseAaveToken.sol	2022-10-11 17:36:35.000000000 +0300
++++ /BaseAaveToken.sol	2022-10-11 16:20:40.000000000 +0300
+@@ -1,9 +1,9 @@
+ // SPDX-License-Identifier: MIT
+ pragma solidity ^0.8.0;
+
+-import {Context} from '../lib/openzeppelin-contracts/contracts/utils/Context.sol';
+-import {IERC20} from '../lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol';
+-import {IERC20Metadata} from '../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol';
++import {Context} from './lib/openzeppelin-contracts/contracts/utils/Context.sol';
++import {IERC20} from './lib/openzeppelin-contracts/contracts/token/ERC20/IERC20.sol';
++import {IERC20Metadata} from './lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol';
+
+ // Inspired by OpenZeppelin Contracts (last updated v4.5.0) (token/ERC20/ERC20.sol)
+ abstract contract BaseAaveToken is Context, IERC20Metadata {
+@@ -18,7 +18,7 @@
+     uint104 balance;
+     uint72 delegatedPropositionBalance;
+     uint72 delegatedVotingBalance;
+-    DelegationState delegationState;
++    uint8 delegationState; // refactored from enum
+   }
+
+   mapping(address => DelegationAwareBalance) internal _balances;
+Common subdirectories: interfaces and /interfaces
+Common subdirectories: lib and /lib
+Common subdirectories: test and /test
+Common subdirectories: utils and /utils

certora/harness/AaveTokenV3Harness.sol

@@ -0,0 +1,55 @@
+// SPDX-License-Identifier: MIT
+
+/**
+
+  This is an extension of the AaveTokenV3 with added getters on the _balances fields
+
+ */
+
+pragma solidity ^0.8.0;
+
+import {AaveTokenV3} from "../../src/AaveTokenV3.sol";
+
+contract AaveTokenV3Harness is AaveTokenV3 {
+
+    // returns user's token balance, used in some community rules
+    function getBalance(address user) view public returns (uint104) {
+    return _balances[user].balance;
+   }
+   // returns user's delegated proposition balance
+   function getDelegatedPropositionBalance(address user) view public returns (uint72) {
+    return _balances[user].delegatedPropositionBalance;
+   }
+
+   // returns user's delegated voting balance
+   function getDelegatedVotingBalance(address user) view public returns (uint72) {
+    return _balances[user].delegatedVotingBalance;
+   }
+
+   //returns user's delegating proposition status
+   function getDelegatingProposition(address user) view public returns (bool) {
+    return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
+        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+   }
+
+   // returns user's delegating voting status
+   function getDelegatingVoting(address user) view public returns (bool) {
+     return _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
+        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+   }
+
+   // returns user's voting delegate
+   function getVotingDelegate(address user) view public returns (address) {
+    return _votingDelegateeV2[user];
+   }
+
+   // returns user's proposition delegate
+   function getPropositionDelegate(address user) view public returns (address) {
+    return _propositionDelegateeV2[user];
+   }
+
+   // returns user's delegation state
+   function getDelegationState(address user) view public returns (DelegationState) {
+    return _balances[user].delegationState;
+   }
+}