Smart Vault: Implement prover rules (#103)

Co-authored-by: Facu Spagnuolo <[email protected]>

.github/workflows/prover-authorizer.yml

@@ -1,4 +1,4 @@
-name: Prover
+name: Prover Authorizer
 
 env:
   CI: true

.github/workflows/prover-smart-vault.yml

@@ -0,0 +1,23 @@
+name: Prover Smart Vault
+
+env:
+  CI: true
+
+on:
+  pull_request:
+    branches: "*"
+    paths:
+      - packages/smart-vault/**
+
+jobs:
+  prove:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Prove
+        uses: ./.github/actions/certora
+        with:
+          workspace: '@mimic-fi/v3-smart-vault'
+          certora-key: ${{ secrets.CERTORA_KEY }}
+          github-token: ${{ secrets.GITHUB_TOKEN }}

packages/smart-vault/certora/conf/smart-vault.conf

@@ -0,0 +1,38 @@
+{
+  "files": [
+    "contracts/SmartVault.sol",
+    "../../packages/authorizer/contracts/Authorizer.sol",
+    "../../packages/fee-controller/contracts/FeeController.sol",
+    "../../packages/helpers/contracts/mocks/WrappedNativeTokenMock.sol",
+    "../../packages/registry/contracts/Registry.sol",
+    "certora/helpers/Helpers.sol"
+  ],
+  "verify": "SmartVault:certora/specs/SmartVault.spec",
+  "link": [
+    "SmartVault:authorizer=Authorizer",
+    "SmartVault:registry=Registry",
+    "SmartVault:feeController=FeeController",
+    "SmartVault:wrappedNativeToken=WrappedNativeTokenMock"
+  ],
+  "loop_iter": "4",
+  "rule_sanity": "basic",
+  "send_only": true,
+  "optimistic_hashing": true,
+  "prover_args": [
+    "-copyLoopUnroll 8",
+    "-optimisticFallback true"
+  ],
+  "optimistic_loop": true,
+  "packages": [
+    "@mimic-fi/v3-authorizer=../../node_modules/@mimic-fi/v3-authorizer",
+    "@mimic-fi/v3-fee-controller=../../node_modules/@mimic-fi/v3-fee-controller",
+    "@mimic-fi/v3-helpers=../../node_modules/@mimic-fi/v3-helpers",
+    "@mimic-fi/v3-price-oracle=../../node_modules/@mimic-fi/v3-price-oracle",
+    "@mimic-fi/v3-registry=../../node_modules/@mimic-fi/v3-registry",
+    "@openzeppelin=../../node_modules/@openzeppelin",
+    "solmate=../../node_modules/solmate"
+  ],
+  "solc_allow_path": ".",
+  "process": "emv",
+  "msg": "SmartVault"
+}

packages/smart-vault/certora/helpers/Helpers.sol

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: GPL-3.0-or-later
+
+pragma solidity ^0.8.0;
+
+import '@mimic-fi/v3-authorizer/contracts/interfaces/IAuthorizer.sol';
+import '@mimic-fi/v3-helpers/contracts/utils/Denominations.sol';
+import '@mimic-fi/v3-helpers/contracts/utils/ERC20Helpers.sol';
+
+contract Helpers {
+    function NATIVE_TOKEN() external pure returns (address) {
+        return Denominations.NATIVE_TOKEN;
+    }
+
+    function balanceOf(address token, address account) external view returns (uint256) {
+        return ERC20Helpers.balanceOf(token, account);
+    }
+
+    function authParams(address p1, address p2, uint256 p3) external pure returns (uint256[] memory r) {
+        r = new uint256[](3);
+        r[0] = uint256(uint160(p1));
+        r[1] = uint256(uint160(p2));
+        r[2] = p3;
+    }
+
+    function authParams(address p1) external pure returns (uint256[] memory r) {
+        r = new uint256[](1);
+        r[0] = uint256(uint160(p1));
+    }
+
+    function getPermissionParamsLength(address authorizer, address who, address where, bytes4 what)
+        external
+        view
+        returns (uint256)
+    {
+        IAuthorizer.Param[] memory permissionParams = IAuthorizer(authorizer).getPermissionParams(who, where, what);
+        return permissionParams.length;
+    }
+}

packages/smart-vault/certora/specs/General.spec

@@ -0,0 +1,34 @@
+// SANITY
+
+rule sanity(method f) good_description "Sanity" {
+    env e;
+    calldataarg args;
+    f(e, args);
+    assert false;
+}
+
+// REENTRANCY GUARD
+
+ghost uint256 ghostReentrancyStatus;
+
+ghost mathint ghostReentrancyChangedTimes;
+
+hook Sload uint256 status currentContract._status STORAGE {
+    require ghostReentrancyStatus == status;
+}
+
+hook Sstore currentContract._status uint256 newStatus STORAGE {
+    ghostReentrancyChangedTimes = ghostReentrancyChangedTimes + 1;
+}
+
+rule 
+    reentrancyGuard(env e, method f, calldataarg args) filtered { f -> !f.isView } 
+    good_description "Ensure external methods cannot be reentered"
+{
+    require ghostReentrancyChangedTimes == 0;
+
+    f(e, args);
+
+    bool hasChangedTwice = ghostReentrancyChangedTimes == 2;
+    assert hasChangedTwice;
+}