From 6273cb9d485cdc84758f8a732cd2e2c406a32a01 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Sun, 6 Jul 2025 18:29:39 +0200 Subject: [PATCH 1/8] Formal verification of Account (7702+7579) --- certora/harnesses/AccountHarness.sol | 13 ++++ certora/run.js | 2 +- certora/specs.json | 6 ++ certora/specs/Account.spec | 109 +++++++++++++++++++++++++++ certora/specs/methods/IAccount.spec | 37 +++++++++ fv-requirements.txt | 2 +- 6 files changed, 167 insertions(+), 2 deletions(-) create mode 100644 certora/harnesses/AccountHarness.sol create mode 100644 certora/specs/Account.spec create mode 100644 certora/specs/methods/IAccount.spec diff --git a/certora/harnesses/AccountHarness.sol b/certora/harnesses/AccountHarness.sol new file mode 100644 index 00000000000..fd1bdc681b8 --- /dev/null +++ b/certora/harnesses/AccountHarness.sol @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.26; + +import {AccountERC7702WithModulesMock} from "../patched/mocks/account/AccountMock.sol"; +import {EIP712} from "../patched/utils/cryptography/EIP712.sol"; + +contract AccountHarness is AccountERC7702WithModulesMock { + constructor(string memory name, string memory version) EIP712(name, version) {} + + function getFallbackHandler(uint32 selector) external view returns (address) { + return _fallbackHandler(bytes4(selector)); + } +} diff --git a/certora/run.js b/certora/run.js index 91f4a6aece1..95003601bff 100755 --- a/certora/run.js +++ b/certora/run.js @@ -14,7 +14,7 @@ import path from 'path'; import yargs from 'yargs'; import { hideBin } from 'yargs/helpers'; import pLimit from 'p-limit'; -import fs from 'fs/promises'; +import fs from 'fs'; const argv = yargs(hideBin(process.argv)) .env('') diff --git a/certora/specs.json b/certora/specs.json index a894190924f..0f58c808e21 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -106,5 +106,11 @@ "spec": "Nonces", "contract": "NoncesHarness", "files": ["certora/harnesses/NoncesHarness.sol"] + }, + { + "spec": "Account", + "contract": "AccountHarness", + "files": ["certora/harnesses/AccountHarness.sol"], + "options": ["--optimistic_loop"] } ] diff --git a/certora/specs/Account.spec b/certora/specs/Account.spec new file mode 100644 index 00000000000..51bac751d5b --- /dev/null +++ b/certora/specs/Account.spec @@ -0,0 +1,109 @@ +import "helpers/helpers.spec"; +import "methods/IAccount.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Module management │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule moduleManagementRule( + env e, + method f, + calldataarg args, + uint256 moduleTypeId, + address module, + bytes additionalContext +) { + bytes context; + require context.length == 0; + + bool isEntryPoint = e.msg.sender == entryPoint(); + bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract; + bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context); + + bool isModuleInstalledBefore = isModuleInstalled(moduleTypeId, module, additionalContext); + f(e, args); + bool isModuleInstalledAfter = isModuleInstalled(moduleTypeId, module, additionalContext); + + assert ( + isModuleInstalledBefore != isModuleInstalledAfter + ) => ( + ( + f.selector == sig:execute(bytes32,bytes).selector && + isEntryPointOrSelf + ) || ( + f.selector == sig:executeFromExecutor(bytes32,bytes).selector && + isExecutionModule + ) || ( + f.selector == sig:installModule(uint256,address,bytes).selector && + isEntryPointOrSelf + ) || ( + f.selector == sig:uninstallModule(uint256,address,bytes).selector && + isEntryPointOrSelf + ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ CALL OPCODE │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost bool call; +ghost address call_target; +ghost uint256 call_value; +ghost uint256 call_argsLength; + +hook CALL(uint256 gas, address target, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + call = true; + call_target = target; + call_value = value; + call_argsLength = argsLength; +} + +rule callOpcodeRule( + env e, + method f, + calldataarg args +) { + require !call; + + bytes context; + require context.length == 0; + + bool isEntryPoint = e.msg.sender == entryPoint(); + bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract; + bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context); + address fallbackHandler = getFallbackHandler(f.selector); + + f(e, args); + + assert call => ( + ( + f.selector == sig:execute(bytes32,bytes).selector && + isEntryPointOrSelf + ) || ( + f.selector == sig:executeFromExecutor(bytes32,bytes).selector && + isExecutionModule + ) || ( + f.selector == sig:installModule(uint256,address,bytes).selector && + isEntryPointOrSelf + ) || ( + f.selector == sig:uninstallModule(uint256,address,bytes).selector && + isEntryPointOrSelf + ) || ( + f.selector == sig:validateUserOp(Account.PackedUserOperation,bytes32,uint256).selector && + isEntryPoint && + ( + // payPrefund (target is entryPoint and argsLength is 0) + (call_target == entryPoint() && call_argsLength == 0 && call_value > 0) + || + // isValidSignatureWithSender (target is as validation module) + (isModuleInstalled(1, call_target, context)) + ) + ) || ( + fallbackHandler != 0 && + call_target == fallbackHandler + ) + ); +} diff --git a/certora/specs/methods/IAccount.spec b/certora/specs/methods/IAccount.spec new file mode 100644 index 00000000000..7afd698e683 --- /dev/null +++ b/certora/specs/methods/IAccount.spec @@ -0,0 +1,37 @@ +methods { + // Account + function entryPoint() external returns (address) envfree; + function getNonce() external returns (uint256) envfree; + function getNonce(uint192) external returns (uint256) envfree; + function validateUserOp(Account.PackedUserOperation,bytes32,uint256) external returns (uint256); + + // IERC1271 + function isValidSignature(bytes32,bytes) external returns (bytes4); + + // IERC7579AccountConfig + function accountId() external returns (string) envfree; + function supportsExecutionMode(bytes32) external returns (bool) envfree; + function supportsModule(uint256) external returns (bool) envfree; + + // IERC7579ModuleConfig + function installModule(uint256,address,bytes) external; + function uninstallModule(uint256,address,bytes) external; + function isModuleInstalled(uint256,address,bytes) external returns (bool) envfree; + + // IERC7579Execution + function execute(bytes32,bytes) external; + function executeFromExecutor(bytes32,bytes) external returns (bytes[]); + + // IERC721Receiver + function onERC721Received(address,address,uint256,bytes) external returns (bytes4) envfree; + + // IERC1155Receiver + function onERC1155Received(address,address,uint256,uint256,bytes) external returns (bytes4) envfree; + function onERC1155BatchReceived(address,address,uint256[],uint256[],bytes) external returns (bytes4) envfree; + + // IERC165 + function supportsInterface(bytes4) external returns (bool) envfree; + + // Harness + function getFallbackHandler(uint32) external returns (address) envfree; +} diff --git a/fv-requirements.txt b/fv-requirements.txt index 788adf384a1..27ef60a5f2b 100644 --- a/fv-requirements.txt +++ b/fv-requirements.txt @@ -1,4 +1,4 @@ -certora-cli==4.13.1 +certora-cli==7.31.0 # File uses a custom name (fv-requirements.txt) so that it isn't picked by Netlify's build # whose latest Python version is 0.3.8, incompatible with most recent versions of Halmos halmos==0.3.0 From ec0e4e848f412376d611a2a7eb0853d557609e5b Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Sun, 6 Jul 2025 18:59:21 +0200 Subject: [PATCH 2/8] fix script --- certora/run.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/run.js b/certora/run.js index 95003601bff..37c26973eb3 100755 --- a/certora/run.js +++ b/certora/run.js @@ -123,7 +123,7 @@ async function runCertora(spec, contract, files, options = []) { stream.end(); // write results in markdown format - writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]); + writeEntry(spec, contract, !(code || signal), (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]); // write all details console.error(`+ certoraRun ${args.join(' ')}\n` + (await output)); From 9b38876859589181553678d0d1a0a20df211ec57 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Sun, 6 Jul 2025 19:20:07 +0200 Subject: [PATCH 3/8] check value passed --- certora/specs/Account.spec | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/certora/specs/Account.spec b/certora/specs/Account.spec index 51bac751d5b..051ac4a00e7 100644 --- a/certora/specs/Account.spec +++ b/certora/specs/Account.spec @@ -87,23 +87,31 @@ rule callOpcodeRule( isExecutionModule ) || ( f.selector == sig:installModule(uint256,address,bytes).selector && - isEntryPointOrSelf + isEntryPointOrSelf && + call_value == 0 ) || ( f.selector == sig:uninstallModule(uint256,address,bytes).selector && - isEntryPointOrSelf + isEntryPointOrSelf && + call_value == 0 ) || ( f.selector == sig:validateUserOp(Account.PackedUserOperation,bytes32,uint256).selector && isEntryPoint && ( - // payPrefund (target is entryPoint and argsLength is 0) - (call_target == entryPoint() && call_argsLength == 0 && call_value > 0) - || - // isValidSignatureWithSender (target is as validation module) - (isModuleInstalled(1, call_target, context)) + ( + // payPrefund (target is entryPoint and argsLength is 0) + call_target == entryPoint() && + call_value > 0 && + call_argsLength == 0 + ) || ( + // isValidSignatureWithSender (target is as validation module) + isModuleInstalled(1, call_target, context) && + call_value == 0 + ) ) ) || ( fallbackHandler != 0 && - call_target == fallbackHandler + call_target == fallbackHandler && + call_value == e.msg.value ) ); } From 3c0c43dec5a75498233bc42f897ba4c03e9e6f4e Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Mon, 7 Jul 2025 12:21:56 +0200 Subject: [PATCH 4/8] up --- certora/harnesses/AccountHarness.sol | 4 ++-- certora/specs/Account.spec | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/harnesses/AccountHarness.sol b/certora/harnesses/AccountHarness.sol index fd1bdc681b8..b921de86b17 100644 --- a/certora/harnesses/AccountHarness.sol +++ b/certora/harnesses/AccountHarness.sol @@ -7,7 +7,7 @@ import {EIP712} from "../patched/utils/cryptography/EIP712.sol"; contract AccountHarness is AccountERC7702WithModulesMock { constructor(string memory name, string memory version) EIP712(name, version) {} - function getFallbackHandler(uint32 selector) external view returns (address) { - return _fallbackHandler(bytes4(selector)); + function getFallbackHandler(bytes4 selector) external view returns (address) { + return _fallbackHandler(selector); } } diff --git a/certora/specs/Account.spec b/certora/specs/Account.spec index 051ac4a00e7..356d9e3832e 100644 --- a/certora/specs/Account.spec +++ b/certora/specs/Account.spec @@ -74,7 +74,7 @@ rule callOpcodeRule( bool isEntryPoint = e.msg.sender == entryPoint(); bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract; bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context); - address fallbackHandler = getFallbackHandler(f.selector); + address fallbackHandler = getFallbackHandler(to_bytes4(f.selector)); f(e, args); From 139373f14aabc1ebf743cd808bb040e89dc7e2f7 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 8 Jul 2025 17:34:30 +0200 Subject: [PATCH 5/8] up --- certora/specs/Account.spec | 56 +++++++++++++++++++++++++++-- certora/specs/methods/IAccount.spec | 3 -- 2 files changed, 53 insertions(+), 6 deletions(-) diff --git a/certora/specs/Account.spec b/certora/specs/Account.spec index 356d9e3832e..47d4f2d9e22 100644 --- a/certora/specs/Account.spec +++ b/certora/specs/Account.spec @@ -1,6 +1,11 @@ import "helpers/helpers.spec"; import "methods/IAccount.spec"; +// Harness +methods { + function getFallbackHandler(bytes4) external returns (address) envfree; +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Module management │ @@ -74,7 +79,9 @@ rule callOpcodeRule( bool isEntryPoint = e.msg.sender == entryPoint(); bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract; bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context); - address fallbackHandler = getFallbackHandler(to_bytes4(f.selector)); + + // For some reason, f.selector does not effectivelly match the msg.sig when f.isFallback + // address fallbackHandler = getFallbackHandler(to_bytes4(f.selector)); f(e, args); @@ -109,9 +116,52 @@ rule callOpcodeRule( ) ) ) || ( - fallbackHandler != 0 && - call_target == fallbackHandler && + f.isFallback && + // fallbackHandler != 0 && + // call_target == fallbackHandler && call_value == e.msg.value ) ); } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ DELEGATECALL OPCODE │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost bool delegatecall; +ghost address delegatecall_target; +ghost uint256 delegatecall_argsLength; + +hook DELEGATECALL(uint256 gas, address target, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + delegatecall = true; + delegatecall_target = target; + delegatecall_argsLength = argsLength; +} + +rule delegatecallOpcodeRule( + env e, + method f, + calldataarg args +) { + require !delegatecall; + + bytes context; + require context.length == 0; + + bool isEntryPoint = e.msg.sender == entryPoint(); + bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract; + bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context); + + f(e, args); + + assert delegatecall => ( + ( + f.selector == sig:execute(bytes32,bytes).selector && + isEntryPointOrSelf + ) || ( + f.selector == sig:executeFromExecutor(bytes32,bytes).selector && + isExecutionModule + ) + ); +} diff --git a/certora/specs/methods/IAccount.spec b/certora/specs/methods/IAccount.spec index 7afd698e683..fd00615e81c 100644 --- a/certora/specs/methods/IAccount.spec +++ b/certora/specs/methods/IAccount.spec @@ -31,7 +31,4 @@ methods { // IERC165 function supportsInterface(bytes4) external returns (bool) envfree; - - // Harness - function getFallbackHandler(uint32) external returns (address) envfree; } From 3a7078b051effa2efb3a7d8d6a6cf2e2c2d9deb6 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 8 Jul 2025 18:14:44 +0200 Subject: [PATCH 6/8] up --- certora/harnesses/AccountHarness.sol | 4 --- certora/specs/Account.spec | 53 ++++++++++++++++------------ 2 files changed, 31 insertions(+), 26 deletions(-) diff --git a/certora/harnesses/AccountHarness.sol b/certora/harnesses/AccountHarness.sol index b921de86b17..22a12cfcb01 100644 --- a/certora/harnesses/AccountHarness.sol +++ b/certora/harnesses/AccountHarness.sol @@ -6,8 +6,4 @@ import {EIP712} from "../patched/utils/cryptography/EIP712.sol"; contract AccountHarness is AccountERC7702WithModulesMock { constructor(string memory name, string memory version) EIP712(name, version) {} - - function getFallbackHandler(bytes4 selector) external view returns (address) { - return _fallbackHandler(selector); - } } diff --git a/certora/specs/Account.spec b/certora/specs/Account.spec index 47d4f2d9e22..42f35302f84 100644 --- a/certora/specs/Account.spec +++ b/certora/specs/Account.spec @@ -1,11 +1,6 @@ import "helpers/helpers.spec"; import "methods/IAccount.spec"; -// Harness -methods { - function getFallbackHandler(bytes4) external returns (address) envfree; -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Module management │ @@ -60,17 +55,15 @@ ghost uint256 call_value; ghost uint256 call_argsLength; hook CALL(uint256 gas, address target, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { - call = true; - call_target = target; - call_value = value; - call_argsLength = argsLength; + if (executingContract == currentContract) { + call = true; + call_target = target; + call_value = value; + call_argsLength = argsLength; + } } -rule callOpcodeRule( - env e, - method f, - calldataarg args -) { +rule callOpcodeRule(env e, method f, calldataarg args) { require !call; bytes context; @@ -80,9 +73,6 @@ rule callOpcodeRule( bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract; bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context); - // For some reason, f.selector does not effectivelly match the msg.sig when f.isFallback - // address fallbackHandler = getFallbackHandler(to_bytes4(f.selector)); - f(e, args); assert call => ( @@ -93,10 +83,12 @@ rule callOpcodeRule( f.selector == sig:executeFromExecutor(bytes32,bytes).selector && isExecutionModule ) || ( + // Note: rule callInstallModule checks that the call target is the module being installed f.selector == sig:installModule(uint256,address,bytes).selector && isEntryPointOrSelf && call_value == 0 ) || ( + // Note: rule callUninstallModule checks that the call target is the module being uninstalled f.selector == sig:uninstallModule(uint256,address,bytes).selector && isEntryPointOrSelf && call_value == 0 @@ -116,14 +108,29 @@ rule callOpcodeRule( ) ) ) || ( + // TODO: check target of call is fallbackHandler f.isFallback && - // fallbackHandler != 0 && - // call_target == fallbackHandler && call_value == e.msg.value ) ); } +rule callInstallModule(env e, uint256 moduleTypeId, address module, bytes initData) { + installModule(e, moduleTypeId, module, initData); + + assert call == true; + assert call_target == module; + assert call_value == 0; +} + +rule callUninstallModule(env e, uint256 moduleTypeId, address module, bytes deInitData) { + uninstallModule(e, moduleTypeId, module, deInitData); + + assert call == true; + assert call_target == module; + assert call_value == 0; +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ DELEGATECALL OPCODE │ @@ -134,9 +141,11 @@ ghost address delegatecall_target; ghost uint256 delegatecall_argsLength; hook DELEGATECALL(uint256 gas, address target, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { - delegatecall = true; - delegatecall_target = target; - delegatecall_argsLength = argsLength; + if (executingContract == currentContract) { + delegatecall = true; + delegatecall_target = target; + delegatecall_argsLength = argsLength; + } } rule delegatecallOpcodeRule( From cd8d1e8c0b5303e8c417b6376c27f8de05bb683f Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 8 Jul 2025 18:56:12 +0200 Subject: [PATCH 7/8] finally a solution for the fallback issue (needs patch) --- .../access_manager_AccessManager.sol.patch | 32 +++++++++---------- ..._extensions_draft-AccountERC7579.sol.patch | 14 ++++++++ certora/harnesses/AccountHarness.sol | 4 +++ certora/specs/Account.spec | 14 +++++--- 4 files changed, 44 insertions(+), 20 deletions(-) create mode 100644 certora/diff/account_extensions_draft-AccountERC7579.sol.patch diff --git a/certora/diff/access_manager_AccessManager.sol.patch b/certora/diff/access_manager_AccessManager.sol.patch index cfb6cdf2f06..e0d52931b43 100644 --- a/certora/diff/access_manager_AccessManager.sol.patch +++ b/certora/diff/access_manager_AccessManager.sol.patch @@ -1,6 +1,6 @@ ---- access/manager/AccessManager.sol 2023-10-05 12:17:09.694051809 -0300 -+++ access/manager/AccessManager.sol 2023-10-05 12:26:18.498688718 -0300 -@@ -6,7 +6,6 @@ +--- access/manager/AccessManager.sol 2025-07-07 12:07:21.810735995 +0200 ++++ access/manager/AccessManager.sol 2025-07-08 18:40:55.443277009 +0200 +@@ -7,7 +7,6 @@ import {IAccessManaged} from "./IAccessManaged.sol"; import {Address} from "../../utils/Address.sol"; import {Context} from "../../utils/Context.sol"; @@ -8,9 +8,9 @@ import {Math} from "../../utils/math/Math.sol"; import {Time} from "../../utils/types/Time.sol"; -@@ -57,7 +56,8 @@ - * mindful of the danger associated with functions such as {{Ownable-renounceOwnership}} or - * {{AccessControl-renounceRole}}. +@@ -58,7 +57,8 @@ + * mindful of the danger associated with functions such as {Ownable-renounceOwnership} or + * {AccessControl-renounceRole}. */ -contract AccessManager is Context, Multicall, IAccessManager { +// NOTE: The FV version of this contract doesn't include Multicall because CVL HAVOCs on any `delegatecall`. @@ -18,7 +18,7 @@ using Time for *; // Structure that stores the details for a target contract. -@@ -105,7 +105,7 @@ +@@ -114,7 +114,7 @@ // Used to identify operations that are currently being executed via {execute}. // This should be transient storage when supported by the EVM. @@ -26,8 +26,8 @@ + bytes32 internal _executionId; // private → internal for FV /** - * @dev Check that the caller is authorized to perform the operation, following the restrictions encoded in -@@ -253,6 +253,11 @@ + * @dev Check that the caller is authorized to perform the operation. +@@ -262,6 +262,11 @@ _setGrantDelay(roleId, newDelay); } @@ -39,7 +39,7 @@ /** * @dev Internal version of {grantRole} without access control. Returns true if the role was newly granted. * -@@ -287,6 +292,11 @@ +@@ -296,6 +301,11 @@ return newMember; } @@ -51,16 +51,16 @@ /** * @dev Internal version of {revokeRole} without access control. This logic is also used by {renounceRole}. * Returns true if the role was previously granted. -@@ -586,7 +596,7 @@ - /** - * @dev Check if the current call is authorized according to admin logic. +@@ -595,7 +605,7 @@ + * + * WARNING: Carefully review the considerations of {AccessManaged-restricted} since they apply to this modifier. */ - function _checkAuthorized() private { + function _checkAuthorized() internal virtual { // private → internal virtual for FV address caller = _msgSender(); (bool immediate, uint32 delay) = _canCallSelf(caller, _msgData()); if (!immediate) { -@@ -609,7 +619,7 @@ +@@ -618,7 +628,7 @@ */ function _getAdminRestrictions( bytes calldata data @@ -69,7 +69,7 @@ if (data.length < 4) { return (false, 0, 0); } -@@ -662,7 +672,7 @@ +@@ -671,7 +681,7 @@ address caller, address target, bytes calldata data @@ -78,7 +78,7 @@ if (target == address(this)) { return _canCallSelf(caller, data); } else { -@@ -716,14 +726,14 @@ +@@ -727,14 +737,14 @@ /** * @dev Extracts the selector from calldata. Panics if data is not at least 4 bytes */ diff --git a/certora/diff/account_extensions_draft-AccountERC7579.sol.patch b/certora/diff/account_extensions_draft-AccountERC7579.sol.patch new file mode 100644 index 00000000000..00a9c26837c --- /dev/null +++ b/certora/diff/account_extensions_draft-AccountERC7579.sol.patch @@ -0,0 +1,14 @@ +--- account/extensions/draft-AccountERC7579.sol 2025-07-07 12:07:22.042739166 +0200 ++++ account/extensions/draft-AccountERC7579.sol 2025-07-08 18:43:59.413714889 +0200 +@@ -308,8 +308,9 @@ + * the ERC-2771 format. + */ + function _fallback() internal virtual returns (bytes memory) { +- address handler = _fallbackHandler(msg.sig); +- require(handler != address(0), ERC7579MissingFallbackHandler(msg.sig)); ++ bytes4 selector = bytes4(msg.data[0:4]); ++ address handler = _fallbackHandler(selector); ++ require(handler != address(0), ERC7579MissingFallbackHandler(selector)); + + // From https://eips.ethereum.org/EIPS/eip-7579#fallback[ERC-7579 specifications]: + // - MUST utilize ERC-2771 to add the original msg.sender to the calldata sent to the fallback handler diff --git a/certora/harnesses/AccountHarness.sol b/certora/harnesses/AccountHarness.sol index 22a12cfcb01..b921de86b17 100644 --- a/certora/harnesses/AccountHarness.sol +++ b/certora/harnesses/AccountHarness.sol @@ -6,4 +6,8 @@ import {EIP712} from "../patched/utils/cryptography/EIP712.sol"; contract AccountHarness is AccountERC7702WithModulesMock { constructor(string memory name, string memory version) EIP712(name, version) {} + + function getFallbackHandler(bytes4 selector) external view returns (address) { + return _fallbackHandler(selector); + } } diff --git a/certora/specs/Account.spec b/certora/specs/Account.spec index 42f35302f84..84516404746 100644 --- a/certora/specs/Account.spec +++ b/certora/specs/Account.spec @@ -1,6 +1,10 @@ import "helpers/helpers.spec"; import "methods/IAccount.spec"; +methods { + function getFallbackHandler(bytes4) external returns (address) envfree; +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Module management │ @@ -51,14 +55,16 @@ rule moduleManagementRule( */ ghost bool call; ghost address call_target; +ghost uint32 call_selector; ghost uint256 call_value; ghost uint256 call_argsLength; hook CALL(uint256 gas, address target, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { if (executingContract == currentContract) { - call = true; - call_target = target; - call_value = value; + call = true; + call_target = target; + call_selector = selector; + call_value = value; call_argsLength = argsLength; } } @@ -108,8 +114,8 @@ rule callOpcodeRule(env e, method f, calldataarg args) { ) ) ) || ( - // TODO: check target of call is fallbackHandler f.isFallback && + call_target == getFallbackHandler(to_bytes4(call_selector)) && call_value == e.msg.value ) ); From 6f2e783cf0790cd1598f5d7b2037259ccc8340ba Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 8 Jul 2025 19:36:39 +0200 Subject: [PATCH 8/8] minimize change --- .../access_manager_AccessManager.sol.patch | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/certora/diff/access_manager_AccessManager.sol.patch b/certora/diff/access_manager_AccessManager.sol.patch index e0d52931b43..cfb6cdf2f06 100644 --- a/certora/diff/access_manager_AccessManager.sol.patch +++ b/certora/diff/access_manager_AccessManager.sol.patch @@ -1,6 +1,6 @@ ---- access/manager/AccessManager.sol 2025-07-07 12:07:21.810735995 +0200 -+++ access/manager/AccessManager.sol 2025-07-08 18:40:55.443277009 +0200 -@@ -7,7 +7,6 @@ +--- access/manager/AccessManager.sol 2023-10-05 12:17:09.694051809 -0300 ++++ access/manager/AccessManager.sol 2023-10-05 12:26:18.498688718 -0300 +@@ -6,7 +6,6 @@ import {IAccessManaged} from "./IAccessManaged.sol"; import {Address} from "../../utils/Address.sol"; import {Context} from "../../utils/Context.sol"; @@ -8,9 +8,9 @@ import {Math} from "../../utils/math/Math.sol"; import {Time} from "../../utils/types/Time.sol"; -@@ -58,7 +57,8 @@ - * mindful of the danger associated with functions such as {Ownable-renounceOwnership} or - * {AccessControl-renounceRole}. +@@ -57,7 +56,8 @@ + * mindful of the danger associated with functions such as {{Ownable-renounceOwnership}} or + * {{AccessControl-renounceRole}}. */ -contract AccessManager is Context, Multicall, IAccessManager { +// NOTE: The FV version of this contract doesn't include Multicall because CVL HAVOCs on any `delegatecall`. @@ -18,7 +18,7 @@ using Time for *; // Structure that stores the details for a target contract. -@@ -114,7 +114,7 @@ +@@ -105,7 +105,7 @@ // Used to identify operations that are currently being executed via {execute}. // This should be transient storage when supported by the EVM. @@ -26,8 +26,8 @@ + bytes32 internal _executionId; // private → internal for FV /** - * @dev Check that the caller is authorized to perform the operation. -@@ -262,6 +262,11 @@ + * @dev Check that the caller is authorized to perform the operation, following the restrictions encoded in +@@ -253,6 +253,11 @@ _setGrantDelay(roleId, newDelay); } @@ -39,7 +39,7 @@ /** * @dev Internal version of {grantRole} without access control. Returns true if the role was newly granted. * -@@ -296,6 +301,11 @@ +@@ -287,6 +292,11 @@ return newMember; } @@ -51,16 +51,16 @@ /** * @dev Internal version of {revokeRole} without access control. This logic is also used by {renounceRole}. * Returns true if the role was previously granted. -@@ -595,7 +605,7 @@ - * - * WARNING: Carefully review the considerations of {AccessManaged-restricted} since they apply to this modifier. +@@ -586,7 +596,7 @@ + /** + * @dev Check if the current call is authorized according to admin logic. */ - function _checkAuthorized() private { + function _checkAuthorized() internal virtual { // private → internal virtual for FV address caller = _msgSender(); (bool immediate, uint32 delay) = _canCallSelf(caller, _msgData()); if (!immediate) { -@@ -618,7 +628,7 @@ +@@ -609,7 +619,7 @@ */ function _getAdminRestrictions( bytes calldata data @@ -69,7 +69,7 @@ if (data.length < 4) { return (false, 0, 0); } -@@ -671,7 +681,7 @@ +@@ -662,7 +672,7 @@ address caller, address target, bytes calldata data @@ -78,7 +78,7 @@ if (target == address(this)) { return _canCallSelf(caller, data); } else { -@@ -727,14 +737,14 @@ +@@ -716,14 +726,14 @@ /** * @dev Extracts the selector from calldata. Panics if data is not at least 4 bytes */