[#95] Check if function handler is listed and not flagged

certora/confs/run.conf

@@ -0,0 +1,19 @@
+{
+    "files": [
+        "contracts/SafeProtocolManager.sol",
+        "contracts/SafeProtocolRegistry.sol",
+        "contracts/test/TestExecutorCertora.sol",
+        "contracts/test/TestFunctionHandlerCertora.sol"
+    ],
+ // "hashing_length_bound": "100",
+    "link": [
+        "SafeProtocolManager:registry=SafeProtocolRegistry"
+    ],
+    "loop_iter": "1",
+    "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

@@ -1,19 +1,3 @@
 #!/bin/bash
 
-params=("--send_only")
-
-if [[ -n "$CI" ]]; then
-    params=()
-fi
-
-certoraRun contracts/SafeProtocolManager.sol contracts/SafeProtocolRegistry.sol contracts/test/TestExecutorCertora.sol \
-    --verify SafeProtocolManager:certora/specs/Manager.spec \
-    --link "SafeProtocolManager:registry=SafeProtocolRegistry" \
-    --solc solc8.18 \
-    --optimistic_loop \
-    --loop_iter 1 \
-    --optimistic_hashing \
-    --hashing_length_bound 352 \
-    --rule_sanity \
-    "${params[@]}" \
-    --msg "Safe Protocol $1"
+certoraRun certora/confs/run.conf

certora/specs/Manager.spec

@@ -1,13 +1,14 @@
 using SafeProtocolRegistry as contractRegistry;
 using TestExecutorCertora as testExecutorCertora;
+using TestFunctionHandlerCertora as testFunctionHandlerCertora;
 
 methods {
     function setRegistry(address) external;
     function registry() external returns (address) 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,
@@ -28,10 +29,20 @@ methods {
         SafeProtocolManager.SafeTransaction,
         uint256,
         bytes 
-    ) external => NONDET;
+    ) external => CONSTANT;
 
-    function _.postCheck(address, bool, bytes) external => NONDET;
+    function _.preCheckRootAccess(
+        address,
+        SafeProtocolManager.SafeTransaction,
+        uint256,
+        bytes 
+    ) external => CONSTANT;
 
+    function _.postCheck(address, bool, bytes) external => CONSTANT;
+
+    function _.handle(address, address, uint256, bytes) external => DISPATCHER(true);
+
+    function testFunctionHandlerCertora.called() external returns (bool) envfree;
 }
 
 rule onlyOwnerCanSetRegistry (method f) filtered {
@@ -62,11 +73,14 @@ rule onlyEnabledAndListedPluginCanExecuteCall(){
     listedAt, flagged = contractRegistry.check(e.msg.sender);
 
     assert testExecutorCertora.called() => (listedAt > 0 && flagged == 0);
+    assert testFunctionHandlerCertora.called() => (listedAt > 0 && flagged == 0);
+
 }
 
 rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionData){
 
-    method f; env e; calldataarg args;
+    // method f;
+    env e; calldataarg args;
     storage initialStorage = lastStorage;
     executeTransaction(e, safe, transactionData);
 
@@ -76,4 +90,5 @@ rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionD
     executeTransaction@withrevert(e, safe, transactionData);
 
     assert !lastReverted;
+
 }

contracts/SafeProtocolManager.sol

@@ -84,6 +84,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(safe, transaction, 1, abi.encode(msg.sender));
         }
 

contracts/base/FunctionHandlerManager.sol

@@ -63,7 +63,7 @@ abstract contract FunctionHandlerManager is RegistryManager {
         bytes4 functionSelector = bytes4(msg.data);
 
         address functionHandler = functionHandlers[safe][functionSelector];
-
+        checkPermittedModule(functionHandler);
         // Revert if functionHandler is not set
         if (functionHandler == address(0)) {
             revert FunctionHandlerNotSet(safe, functionSelector);

contracts/test/TestFunctionHandlerCertora.sol

@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+pragma solidity ^0.8.18;
+import {ISafeProtocolFunctionHandler} from "../interfaces/Modules.sol";
+
+contract TestFunctionHandlerCertora is ISafeProtocolFunctionHandler {
+    bool public called;
+
+    function metadataProvider() external view returns (uint256 providerType, bytes memory location) {}
+
+    function supportsInterface(bytes4 interfaceId) external view override returns (bool) {}
+
+    function handle(address, address, uint256, bytes calldata) external override returns (bytes memory) {
+        called = true;
+        return "";
+    }
+}