[#95] Add rules

5afe · Sep 25, 2023 · 4b3db3c · 4b3db3c
1 parent ef786a7
commit 4b3db3c
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 6 deletions.
diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec
@@ -68,10 +68,11 @@ rule onlyOwnerCanSetRegistry (method f) filtered {
 
 }
 
-rule onlyEnabledAndListedPluginCanExecuteCall() {
+rule onlyEnabledAndListedPluginCanExecuteCall(method f) filtered {
+    f -> f.selector == sig:executeTransaction(address,SafeProtocolManager.SafeTransaction).selector || f.selector == sig:executeRootAccess(address,SafeProtocolManager.SafeRootAccess).selector 
+} {
 
-
-    method f; env e; calldataarg args;
+    env e; calldataarg args;
 
     requireInvariant tempHooksStorage(e.msg.sender);
 
@@ -136,7 +137,13 @@ function getTempHooksData(address account) returns address {
 }
 
 invariant tempHooksStorage(address plugin) 
-    getTempHooksData(plugin) != 0 => checkListedAndNotFlagged(getTempHooksData(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;
@@ -145,4 +152,4 @@ rule onlyOneStorageUpdates{
     storage after = lastStorage;
     // Either storage of testExecutorCertora is updated or storage of testExecutorCertoraOther is updated
     assert (before[testExecutorCertora] == after[testExecutorCertora]) || (before[testExecutorCertoraOther] == after[testExecutorCertoraOther]);
-}
+}
diff --git a/contracts/SafeProtocolManager.sol b/contracts/SafeProtocolManager.sol
@@ -142,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));
         }
 

diff --git a/contracts/base/FunctionHandlerManager.sol b/contracts/base/FunctionHandlerManager.sol
@@ -63,13 +63,14 @@ abstract contract FunctionHandlerManager is RegistryManager {
         bytes4 functionSelector = bytes4(msg.data);
 
         address functionHandler = functionHandlers[account][functionSelector];
-        checkPermittedModule(functionHandler);
 
         // Revert if functionHandler is not set
         if (functionHandler == address(0)) {
             revert FunctionHandlerNotSet(account, functionSelector);
         }
 
+        checkPermittedModule(functionHandler);
+
         address sender;
         // solhint-disable-next-line no-inline-assembly
         assembly {