L-30: Make AccountERC7579 isModuleInstalled return false for the address zero module

.changeset/fifty-owls-boil.md

@@ -0,0 +1,5 @@
+---
+'openzeppelin-solidity': patch
+---
+
+`AccountERC7579`: `isModuleInstalled` return false for address zero fallback & hook modules

.github/workflows/formal-verification.yml

@@ -24,6 +24,8 @@ jobs:
     if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification') || contains(github.event.pull_request.labels.*.name, 'formal-verification-force-all')
     steps:
       - uses: actions/checkout@v6
+        with:
+          fetch-depth: 0
       - name: Set up environment
         uses: ./.github/actions/setup
         with:

contracts/account/extensions/draft-AccountERC7579.sol

@@ -154,7 +154,10 @@ abstract contract AccountERC7579 is Account, IERC1271, IERC7579Execution, IERC75
         if (moduleTypeId == MODULE_TYPE_EXECUTOR) return _executors.contains(module);
         if (moduleTypeId == MODULE_TYPE_FALLBACK)
             // ERC-7579 requires this function to return bool, never revert. Check length to avoid out-of-bounds access.
-            return additionalContext.length > 3 && _fallbacks[bytes4(additionalContext[0:4])] == module;
+            return
+                module != address(0) &&
+                additionalContext.length > 3 &&
+                _fallbacks[bytes4(additionalContext[0:4])] == module;
         return false;
     }
 

contracts/account/extensions/draft-AccountERC7579Hooked.sol

@@ -64,7 +64,7 @@ abstract contract AccountERC7579Hooked is AccountERC7579 {
         bytes calldata data
     ) public view virtual override returns (bool) {
         return
-            (moduleTypeId == MODULE_TYPE_HOOK && module == hook()) ||
+            (moduleTypeId == MODULE_TYPE_HOOK && module != address(0) && module == hook()) ||
             super.isModuleInstalled(moduleTypeId, module, data);
     }
 

fv/specs/Account.spec

@@ -205,7 +205,13 @@ invariant absentExecutorIsNotStored(address module, uint256 index)
 */
 // This guarantees that at most one fallback module is active for a given initData (i.e. selector)
 rule fallbackModule(address module, bytes initData) {
-    assert isModuleInstalled(FALLBACK_TYPE(), module, initData) <=> (initData.length >= 4 && getFallbackHandler(getDataSelector(initData)) == module);
+    assert (
+        isModuleInstalled(FALLBACK_TYPE(), module, initData)
+    ) <=> (
+        module != 0 &&
+        initData.length >= 4 &&
+        getFallbackHandler(getDataSelector(initData)) == module
+    );
 }
 
 rule moduleManagementRule(env e, method f, calldataarg args, uint256 moduleTypeId, address module, bytes additionalContext)
@@ -265,17 +271,8 @@ rule installModuleRule(env e, uint256 moduleTypeId, address module, bytes initDa
 
     // No side effect on other modules
     assert isOtherModuleInstalledBefore != isOtherModuleInstalledAfter => (
-        (
-            moduleTypeId == otherModuleTypeId &&
-            module == otherModule
-        ) || (
-            moduleTypeId == FALLBACK_TYPE() &&
-            otherModuleTypeId == FALLBACK_TYPE() &&
-            otherModule == 0 && // when a fallback module is installed, the 0 module is "removed" for that selector
-            getDataSelector(otherInitData) == getDataSelector(initData) &&
-            isOtherModuleInstalledBefore &&
-            !isOtherModuleInstalledAfter
-        )
+        moduleTypeId == otherModuleTypeId &&
+        module == otherModule
     );
 }
 
@@ -304,17 +301,8 @@ rule uninstallModuleRule(env e, uint256 moduleTypeId, address module, bytes init
 
     // No side effect on other modules
     assert isOtherModuleInstalledBefore != isOtherModuleInstalledAfter => (
-        (
-            moduleTypeId == otherModuleTypeId &&
-            module == otherModule
-        ) || (
-            moduleTypeId == FALLBACK_TYPE() &&
-            otherModuleTypeId == FALLBACK_TYPE() &&
-            otherModule == 0 && // when a fallback module is uninstalled, the 0 module is "added" for that selector
-            getDataSelector(otherInitData) == getDataSelector(initData) &&
-            !isOtherModuleInstalledBefore &&
-            isOtherModuleInstalledAfter
-        )
+        moduleTypeId == otherModuleTypeId &&
+        module == otherModule
     );
 }
 

test/account/extensions/AccountERC7579.behavior.js

@@ -106,6 +106,16 @@ function shouldBehaveLikeAccountERC7579({ withHooks = false } = {}) {
           this.mock.isModuleInstalled(MODULE_TYPE_FALLBACK, this.modules[MODULE_TYPE_FALLBACK], '0x12345678'),
         ).to.eventually.equal(false);
       });
+
+      it('returns false for address(0) as module', async function () {
+        const moduleTypes = [MODULE_TYPE_FALLBACK, MODULE_TYPE_VALIDATOR, MODULE_TYPE_EXECUTOR];
+        withHooks && moduleTypes.push(MODULE_TYPE_HOOK);
+        for (const moduleTypeId of moduleTypes) {
+          await expect(this.mock.isModuleInstalled(moduleTypeId, ethers.ZeroAddress, '0x12345678')).to.eventually.equal(
+            false,
+          );
+        }
+      });
     });
 
     describe('module installation', function () {