Certora Review (aave#311)

* Certora review

* ci: Fix format

* docs: Add Certora audit

---------

Co-authored-by: Yuval Zalmenson <yuvalzalmenson@Yuvals-MacBook-Pro-3.local>

.github/workflows/certora.yml

@@ -0,0 +1,67 @@
+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: 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: Install node dependencies
+        run: |
+          npm i
+
+      - 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:
+          - verifyGhoToken.sh length_leq_max_uint160 inv_balanceOf_leq_totalSupply total_supply_eq_sumAllLevel sumAllBalance_eq_totalSupply sumAllLevel_eq_sumAllBalance inv_valid_capacity inv_valid_level address_in_set_values_iff_in_set_indexes addr_in_set_iff_in_map addr_in_set_list_iff_in_map level_leq_capacity mint_after_burn burn_after_mint level_unchanged_after_mint_followed_by_burn level_after_mint level_after_burn facilitator_in_list_after_setFacilitatorBucketCapacity getFacilitatorBucketCapacity_after_setFacilitatorBucketCapacity facilitator_in_list_after_addFacilitator facilitator_in_list_after_mint_and_burn address_not_in_list_after_removeFacilitator balance_after_mint balance_after_burn mintLimitedByFacilitatorRemainingCapacity burnLimitedByFacilitatorLevel ARRAY_IS_INVERSE_OF_MAP_Invariant addressSetInvariant address_not_in_list_after_removeFacilitator_CASE_SPLIT_zero_address
+          - verifyGhoAToken.sh noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero handleRepayment_after_transferUnderlyingTo level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
+          - verifyGhoDiscountRateStrategy.sh equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
+          - verifyFlashMinter.sh balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
+          - verifyGhoVariableDebtToken.sh discountCantExceed100Percent disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease userCantNullifyItsDebt integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation onlyMintForUserCanIncreaseUsersBalance integrityOfMint_cantDecreaseInterestWithMint integrityMint_atoken integrityOfBurn_updateDiscountRate integrityOfBurn_updateIndex integrityOfBurn_fixedIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance

README.md

@@ -40,7 +40,7 @@ You can find all audit reports under the [audits](./audits/) folder
 - [10-11-2022 - OpenZeppelin](./audits/10-11-2022-Openzeppelin-v2.pdf)
 - [24-12-2022 - Sigma Prime](./audits/24-12-2022-Sigma-Prime.pdf)
 - [02-02-2023 - ABDK](./audits/02-02-2023-ABDK.pdf)
-- Certora WIP
+- [02-28-2023 - Certora Formal Verification](./certora/reports/FormalVerificationReportForAavesGHOToken.pdf)
 
 ## Getting Started
 

certora/.gitignore

@@ -0,0 +1,5 @@
+# certora temp files
+.certora/
+.certora*
+.last_confs/
+resource_errors*

certora/Makefile

@@ -0,0 +1,24 @@
+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 $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./$(CONTRACTS_DIR)/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+

certora/applyHarness.patch

@@ -0,0 +1,74 @@
+diff -ruN ../src/.gitignore .gitignore
+--- ../src/.gitignore	1970-01-01 02:00:00.000000000 +0200
++++ .gitignore	2023-02-26 11:58:05.000000000 +0200
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
+--- ../src/contracts/gho/GhoToken.sol	2023-02-26 10:23:14.000000000 +0200
++++ contracts/gho/GhoToken.sol	2023-02-26 13:26:13.000000000 +0200
+@@ -71,11 +71,16 @@
+     uint128 bucketCapacity
+   ) external onlyOwner {
+     Facilitator storage facilitator = _facilitators[facilitatorAddress];
++    require(
++      !facilitator.isLabelNonempty,    //TODO: remove workaroun when CERT-977 is resolved
++      'FACILITATOR_ALREADY_EXISTS'
++    );
+     require(bytes(facilitator.label).length == 0, 'FACILITATOR_ALREADY_EXISTS');
+     require(bytes(facilitatorLabel).length > 0, 'INVALID_LABEL');
+
+     facilitator.label = facilitatorLabel;
+     facilitator.bucketCapacity = bucketCapacity;
++    facilitator.isLabelNonempty = true;
+
+     _facilitatorsList.add(facilitatorAddress);
+
+@@ -89,6 +94,10 @@
+   /// @inheritdoc IGhoToken
+   function removeFacilitator(address facilitatorAddress) external onlyOwner {
+     require(
++      _facilitators[facilitatorAddress].isLabelNonempty,    //TODO: remove workaroun when CERT-977 is resolved
++      'FACILITATOR_DOES_NOT_EXIST'
++    );
++    require(
+       bytes(_facilitators[facilitatorAddress].label).length > 0,
+       'FACILITATOR_DOES_NOT_EXIST'
+     );
+@@ -108,6 +117,10 @@
+     address facilitator,
+     uint128 newCapacity
+   ) external onlyOwner {
++    require(
++      _facilitators[facilitator].isLabelNonempty,    //TODO: remove workaroun when CERT-977 is resolved
++      'FACILITATOR_DOES_NOT_EXIST'
++    );
+     require(bytes(_facilitators[facilitator].label).length > 0, 'FACILITATOR_DOES_NOT_EXIST');
+
+     uint256 oldCapacity = _facilitators[facilitator].bucketCapacity;
+@@ -122,12 +135,12 @@
+   }
+
+   /// @inheritdoc IGhoToken
+-  function getFacilitatorBucket(address facilitator) external view returns (uint256, uint256) {
++  function getFacilitatorBucket(address facilitator) public view returns (uint256, uint256) {
+     return (_facilitators[facilitator].bucketCapacity, _facilitators[facilitator].bucketLevel);
+   }
+
+   /// @inheritdoc IGhoToken
+-  function getFacilitatorsList() external view returns (address[] memory) {
++  function getFacilitatorsList() public view returns (address[] memory) {
+     return _facilitatorsList.values();
+   }
+ }
+diff -ruN ../src/contracts/gho/interfaces/IGhoToken.sol contracts/gho/interfaces/IGhoToken.sol
+--- ../src/contracts/gho/interfaces/IGhoToken.sol	2023-02-26 10:23:14.000000000 +0200
++++ contracts/gho/interfaces/IGhoToken.sol	2023-02-26 11:58:05.000000000 +0200
+@@ -14,6 +14,7 @@
+     uint128 bucketCapacity;
+     uint128 bucketLevel;
+     string label;
++    bool isLabelNonempty;   //TODO: remove workaroun when https://certora.atlassian.net/browse/CERT-977 is resolved
+   }
+
+   /**

certora/harness/DummyERC20A.sol

@@ -0,0 +1,4 @@
+pragma solidity ^0.8.0;
+import './DummyERC20Impl.sol';
+
+contract DummyERC20A is DummyERC20Impl {}

certora/harness/DummyERC20B.sol

@@ -0,0 +1,4 @@
+pragma solidity ^0.8.0;
+import './DummyERC20Impl.sol';
+
+contract DummyERC20B is DummyERC20Impl {}

certora/harness/DummyERC20Impl.sol

@@ -0,0 +1,58 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+// with mint
+contract DummyERC20Impl {
+  uint256 t;
+  mapping(address => uint256) b;
+  mapping(address => mapping(address => uint256)) a;
+
+  string public name;
+  string public symbol;
+  uint public decimals;
+
+  function myAddress() public returns (address) {
+    return address(this);
+  }
+
+  function add(uint a, uint b) internal pure returns (uint256) {
+    uint c = a + b;
+    require(c >= a);
+    return c;
+  }
+
+  function sub(uint a, uint b) internal pure returns (uint256) {
+    require(a >= b);
+    return a - b;
+  }
+
+  function totalSupply() external view returns (uint256) {
+    return t;
+  }
+
+  function balanceOf(address account) external view returns (uint256) {
+    return b[account];
+  }
+
+  function transfer(address recipient, uint256 amount) external returns (bool) {
+    b[msg.sender] = sub(b[msg.sender], amount);
+    b[recipient] = add(b[recipient], amount);
+    return true;
+  }
+
+  function allowance(address owner, address spender) external view returns (uint256) {
+    return a[owner][spender];
+  }
+
+  function approve(address spender, uint256 amount) external returns (bool) {
+    a[msg.sender][spender] = amount;
+    return true;
+  }
+
+  function transferFrom(address sender, address recipient, uint256 amount) external returns (bool) {
+    b[sender] = sub(b[sender], amount);
+    b[recipient] = add(b[recipient], amount);
+    a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
+    return true;
+  }
+}

certora/harness/DummyERC20WithTimedBalanceOf.sol

@@ -0,0 +1,12 @@
+contract DummyERC20WithTimedBalanceOf {
+  function balanceOf(address user) public view virtual returns (uint256) {
+    return _balanceOfWithBlockTimestamp(user, block.timestamp);
+  }
+
+  function _balanceOfWithBlockTimestamp(
+    address user,
+    uint256 blockTs
+  ) internal view returns (uint256) {
+    return 0; // STUB! Should be summarized
+  }
+}

certora/harness/DummyPool.sol

@@ -0,0 +1,12 @@
+contract DummyPool {
+  function getReserveNormalizedVariableDebt(address asset) external view returns (uint256) {
+    return _getReserveNormalizedVariableDebtWithBlockTimestamp(asset, block.timestamp);
+  }
+
+  function _getReserveNormalizedVariableDebtWithBlockTimestamp(
+    address asset,
+    uint256 blockTs
+  ) internal view returns (uint256) {
+    return 0; // will be replaced by a sammury in the spec file
+  }
+}

certora/harness/GhoDiscountRateStrategyHarness.sol

@@ -0,0 +1,10 @@
+import {GhoDiscountRateStrategy} from '../munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol';
+import {WadRayMath} from '@aave/core-v3/contracts/protocol/libraries/math/WadRayMath.sol';
+
+contract GhoDiscountRateStrategyHarness is GhoDiscountRateStrategy {
+  using WadRayMath for uint256;
+
+  function wadMul(uint256 x, uint256 y) external view returns (uint256) {
+    return x.wadMul(y);
+  }
+}

certora/harness/GhoTokenHarness.sol

@@ -0,0 +1,82 @@
+pragma solidity ^0.8.0;
+
+import {IGhoToken} from '../munged/contracts/gho/interfaces/IGhoToken.sol';
+import '@openzeppelin/contracts/utils/structs/EnumerableSet.sol';
+import {GhoToken} from '../munged/contracts/gho/GhoToken.sol';
+
+contract GhoTokenHarness is GhoToken {
+  using EnumerableSet for EnumerableSet.AddressSet;
+
+  /**
+   * @notice Returns the backet capacity
+   * @param facilitator The address of the facilitator
+   * @return The facilitator bucket capacity
+   */
+  function getFacilitatorBucketCapacity(address facilitator) public view returns (uint256) {
+    (uint256 bucketCapacity, ) = getFacilitatorBucket(facilitator);
+    return bucketCapacity;
+  }
+
+  /**
+   * @notice Returns the backet level
+   * @param facilitator The address of the facilitator
+   * @return The facilitator bucket level
+   */
+  function getFacilitatorBucketLevel(address facilitator) public view returns (uint256) {
+    (, uint256 bucketLevel) = getFacilitatorBucket(facilitator);
+    return bucketLevel;
+  }
+
+  /**
+   * @notice Returns the length of the facilitator list
+   * @return The length of the facilitator list
+   */
+  function getFacilitatorsListLen() external view returns (uint256) {
+    address[] memory flist = getFacilitatorsList();
+    return flist.length;
+  }
+
+  /**
+   * @notice Indicator of GhoToken mapping
+   * @param addr An address of a facilitator
+   * @return True of facilitator is in GhoToken mapping
+   */
+  function is_in_facilitator_mapping(address addr) external view returns (bool) {
+    Facilitator memory facilitator = _facilitators[addr];
+    return facilitator.isLabelNonempty; //TODO: remove workaroun when CERT-977 is resolved
+    //  return (bytes(facilitator.label).length > 0);
+  }
+
+  /**
+   * @notice Indicator of AddressSet mapping
+   * @param addr An address of a facilitator
+   * @return True of facilitator is in AddressSet mapping
+   */
+  function is_in_facilitator_set_map(address addr) external view returns (bool) {
+    return _facilitatorsList.contains(addr);
+  }
+
+  /**
+   * @notice Indicator of AddressSet list
+   * @param addr An address of a facilitator
+   * @return True of facilitator is in AddressSet array
+   */
+  function is_in_facilitator_set_array(address addr) external view returns (bool) {
+    address[] memory flist = getFacilitatorsList();
+    for (uint256 i = 0; i < flist.length; ++i) {
+      if (address(flist[i]) == addr) {
+        return true;
+      }
+    }
+    return false;
+  }
+
+  /**
+   * @notice Converts address to bytes32
+   * @param value Some address
+   * @return b the value as bytes32
+   */
+  function to_bytes32(address value) external pure returns (bytes32 b) {
+    b = bytes32(uint256(uint160(value)));
+  }
+}