Setup certora workflow

.github/workflows/certora.yml

@@ -0,0 +1,49 @@
+name: certora
+
+on:
+    push:
+        branches:
+            - main
+    pull_request:
+        branches:
+            - main
+
+    workflow_dispatch:
+
+jobs:
+    verify:
+        runs-on: ubuntu-latest
+        strategy:
+            matrix:
+                rule: ["verifyManager.sh"]
+
+        steps:
+            - uses: actions/checkout@v3
+
+            - name: Install python
+              uses: actions/setup-python@v4
+              with: { python-version: 3.11 }
+
+            - name: Install java
+              uses: actions/setup-java@v3
+              with: { java-version: "17", java-package: jre, distribution: semeru }
+
+            - name: Install certora cli
+              run: pip install -Iv certora-cli
+
+            - name: Install solc
+              run: |
+                  wget https://github.com/ethereum/solidity/releases/download/v0.8.18/solc-static-linux
+                  chmod +x solc-static-linux
+                  sudo mv solc-static-linux /usr/local/bin/solc8.18
+
+            - name: Install dependencies
+              run: yarn --frozen-lockfile
+
+            - name: Verify rule ${{ matrix.rule }}
+              run: |
+                  echo "key length" ${#CERTORAKEY}
+                  chmod +x ./certora/scripts/${{ matrix.rule }}
+                  ./certora/scripts/${{ matrix.rule }}
+              env:
+                  CERTORAKEY: ${{ secrets.CERTORA_KEY }}

.gitignore

@@ -11,3 +11,8 @@ artifacts
 
 deployments/
 dist/
+
+# Certora Formal Verification related files
+.certora_internal
+.certora_recent_jobs.json
+.zip-output-url.txt

README.md

@@ -117,13 +117,13 @@ yarn
 ### Compile
 
 ```bash
-npx hardhat compile
+yarn hardhat compile
 ```
 
 ### Test
 
 ```bash
-npx hardhat test
+yarn hardhat test
 ```
 
 ### Deploy

certora/README.md

@@ -0,0 +1,11 @@
+# Formal verification of Safe{Core} Protocol contracts
+
+## Setup
+
+- Install certora
+- Setup key
+- Execute
+
+```bash
+sh certora/scripts/verifyManager.sh
+```

certora/confs/run.conf

@@ -0,0 +1,24 @@
+{
+    "files": [
+        "contracts/SafeProtocolManager.sol",
+        "contracts/SafeProtocolRegistry.sol",
+        "contracts/test/TestExecutorCertora.sol",
+        "contracts/test/certora/TestExecutorCertoraOther.sol",
+        "contracts/test/TestFunctionHandlerCertora.sol",
+        "contracts/test/certora/TestHooksCertora.sol",
+        "contracts/test/TestPlugin.sol"
+
+    ],
+    "hashing_length_bound": "320",
+    "link": [
+        "SafeProtocolManager:registry=SafeProtocolRegistry"
+    ],
+    "loop_iter": "1",
+    "prover_args" : ["-copyLoopUnroll 11"],
+    "msg": "Safe Protocol Manager",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "rule_sanity": "basic",
+//  "send_only": true,
+    "verify": "SafeProtocolManager:certora/specs/Manager.spec"
+}

certora/scripts/verifyManager.sh

@@ -0,0 +1,3 @@
+#!/bin/bash
+
+certoraRun certora/confs/run.conf --solc solc8.18

certora/specs/Manager.spec

@@ -0,0 +1,155 @@
+using SafeProtocolRegistry as contractRegistry;
+using TestExecutorCertora as testExecutorCertora;
+using TestFunctionHandlerCertora as testFunctionHandlerCertora;
+using TestHooksCertora as testHooksCertora;
+using TestExecutorCertoraOther as testExecutorCertoraOther;
+using TestPlugin as testPlugin;
+
+methods {
+    function setRegistry(address) external;
+    function registry() external returns (address) envfree;
+    function tempHooksData(address) external returns (address, bytes) envfree;
+
+    function _.supportsInterface(bytes4) external => DISPATCHER(true);
+    function testExecutorCertora.called() external returns (bool) envfree;
+
+    function contractRegistry.check(address module) external returns (uint64, uint64) envfree;
+    function _.execTransactionFromModule(
+        address,
+        uint256,
+        bytes,
+        uint8 
+    ) external => DISPATCHER(true);
+
+    function _.execTransactionFromModuleReturnData(
+        address,
+        uint256,
+        bytes,
+        uint8 
+    )  external => DISPATCHER(true);
+
+    function _.preCheck(
+        address,
+        SafeProtocolManager.SafeTransaction,
+        uint256,
+        bytes 
+    ) external => DISPATCHER(true);
+
+    function _.preCheckRootAccess(
+        address,
+        SafeProtocolManager.SafeRootAccess,
+        uint256,
+        bytes
+    ) external => DISPATCHER(true);
+
+    function _.postCheck(address, bool, bytes) external => DISPATCHER(true);
+
+    function _.handle(address, address, uint256, bytes) external => DISPATCHER(true);
+
+    function testFunctionHandlerCertora.called() external returns (bool) envfree;
+
+    function testHooksCertora.called() external returns (bool) envfree;
+
+    function _.requiresPermissions() external => DISPATCHER(true);
+}
+
+rule onlyOwnerCanSetRegistry (method f) filtered {
+    f -> f.selector != sig:setRegistry(address).selector
+}
+{
+    address registryBefore = registry();
+
+    calldataarg args; env e;
+    f(e, args);
+
+    address registryAfter = registry();
+
+    assert registryBefore == registryAfter;
+
+}
+
+rule onlyEnabledAndListedPluginCanExecuteCall(method f) filtered {
+    f -> f.selector == sig:executeTransaction(address,SafeProtocolManager.SafeTransaction).selector || f.selector == sig:executeRootAccess(address,SafeProtocolManager.SafeRootAccess).selector 
+} {
+
+    env e; calldataarg args;
+
+    requireInvariant tempHooksStorage(e.msg.sender);
+
+    require(testExecutorCertora.called() == false);
+    require(testFunctionHandlerCertora.called() == false);
+    require(testHooksCertora.called() == false);
+
+    f(e, args);
+
+    uint64 listedAt;
+    uint64 flagged;
+
+    listedAt, flagged = contractRegistry.check(e.msg.sender);
+
+    assert testExecutorCertora.called() => (listedAt > 0 && flagged == 0);
+
+    uint64 listedAtHandler;
+    uint64 flaggedHandler;
+
+    listedAtHandler, flaggedHandler = contractRegistry.check(testFunctionHandlerCertora);
+
+    assert testFunctionHandlerCertora.called() => (listedAtHandler > 0 && flaggedHandler == 0);
+
+
+    uint64 listedAtHooks;
+    uint64 flaggedHooks;
+
+    listedAtHooks, flaggedHooks = contractRegistry.check(testHooksCertora);
+
+    assert testHooksCertora.called() => (listedAtHooks > 0 && flaggedHooks == 0);
+
+}
+
+rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionData){
+
+    // method f;
+    env e; calldataarg args;
+    storage initialStorage = lastStorage;
+    executeTransaction(e, safe, transactionData);
+
+    env e2;
+    setHooks(e2, 0) at initialStorage;
+
+    executeTransaction@withrevert(e, safe, transactionData);
+
+    assert !lastReverted;
+
+}
+
+function checkListedAndNotFlagged(address module) returns bool {
+    uint64 listedAtHooks;
+    uint64 flaggedHooks;
+    listedAtHooks, flaggedHooks = contractRegistry.check(module);
+    return (listedAtHooks > 0 && flaggedHooks == 0);
+}
+
+function getTempHooksData(address account) returns address {
+    address hooksAddress;
+    bytes hooksData;
+    hooksAddress, hooksData = tempHooksData(account);
+    return hooksAddress;
+}
+
+invariant tempHooksStorage(address plugin) 
+    getTempHooksData(plugin) != 0 => checkListedAndNotFlagged(getTempHooksData(plugin))
+    filtered { f -> f.selector != sig:checkModuleTransaction(address,uint256,bytes,Enum.Operation,address).selector}
+
+invariant tempHooksStorageIsAlwaysEmpty(address plugin) 
+    getTempHooksData(plugin) == 0
+    filtered { f -> f.selector != sig:checkModuleTransaction(address,uint256,bytes,Enum.Operation,address).selector}
+
+
+rule onlyOneStorageUpdates{
+    storage before = lastStorage;
+    method f; env e; calldataarg args;
+    f(e, args);
+    storage after = lastStorage;
+    // Either storage of testExecutorCertora is updated or storage of testExecutorCertoraOther is updated
+    assert (before[testExecutorCertora] == after[testExecutorCertora]) || (before[testExecutorCertoraOther] == after[testExecutorCertoraOther]);
+}

contracts/SafeProtocolManager.sol

@@ -83,6 +83,8 @@ contract SafeProtocolManager is ISafeProtocolManager, RegistryManager, HooksMana
         if (areHooksEnabled) {
             // execution metadata for transaction execution through plugin is encoded address of the plugin i.e. msg.sender.
             // executionType = 1 for plugin flow
+            // should check below exist here?
+            checkPermittedModule(hooksAddress);
             preCheckData = ISafeProtocolHooks(hooksAddress).preCheck(account, transaction, 1, abi.encode(msg.sender));
         }
 
@@ -140,6 +142,8 @@ contract SafeProtocolManager is ISafeProtocolManager, RegistryManager, HooksMana
         if (areHooksEnabled) {
             // execution metadata for transaction execution through plugin is encoded address of the plugin i.e. msg.sender.
             // executionType = 1 for plugin flow
+            // should check below exist here?
+            checkPermittedModule(hooksAddress);
             preCheckData = ISafeProtocolHooks(hooksAddress).preCheckRootAccess(account, rootAccess, 1, abi.encode(msg.sender));
         }
 

contracts/base/FunctionHandlerManager.sol

@@ -69,6 +69,8 @@ abstract contract FunctionHandlerManager is RegistryManager {
             revert FunctionHandlerNotSet(account, functionSelector);
         }
 
+        checkPermittedModule(functionHandler);
+
         address sender;
         // solhint-disable-next-line no-inline-assembly
         assembly {