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 new file mode 100644 index 00000000000..b921de86b17 --- /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(bytes4 selector) external view returns (address) { + return _fallbackHandler(selector); + } +} diff --git a/certora/run.js b/certora/run.js index 91f4a6aece1..37c26973eb3 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('') @@ -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)); 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..84516404746 --- /dev/null +++ b/certora/specs/Account.spec @@ -0,0 +1,182 @@ +import "helpers/helpers.spec"; +import "methods/IAccount.spec"; + +methods { + function getFallbackHandler(bytes4) external returns (address) envfree; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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 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_selector = selector; + 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); + + f(e, args); + + assert call => ( + ( + f.selector == sig:execute(bytes32,bytes).selector && + isEntryPointOrSelf + ) || ( + 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 + ) || ( + f.selector == sig:validateUserOp(Account.PackedUserOperation,bytes32,uint256).selector && + isEntryPoint && + ( + ( + // 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 + ) + ) + ) || ( + f.isFallback && + call_target == getFallbackHandler(to_bytes4(call_selector)) && + 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 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +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 { + if (executingContract == currentContract) { + 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 new file mode 100644 index 00000000000..fd00615e81c --- /dev/null +++ b/certora/specs/methods/IAccount.spec @@ -0,0 +1,34 @@ +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; +} 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