diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 86acca7f32b..6c907436ad3 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -12,7 +12,7 @@ on: env: PIP_VERSION: '3.11' JAVA_VERSION: '11' - SOLC_VERSION: '0.8.20' + SOLC_VERSION: '0.8.27' concurrency: ${{ github.workflow }}-${{ github.ref }} 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..8b281e24e68 --- /dev/null +++ b/certora/diff/account_extensions_draft-AccountERC7579.sol.patch @@ -0,0 +1,25 @@ +--- account/extensions/draft-AccountERC7579.sol 2025-07-22 11:18:42.944504471 +0200 ++++ account/extensions/draft-AccountERC7579.sol 2025-07-22 13:57:03.670277084 +0200 +@@ -60,8 +60,8 @@ + using EnumerableSet for *; + using Packing for bytes32; + +- EnumerableSet.AddressSet private _validators; +- EnumerableSet.AddressSet private _executors; ++ EnumerableSet.AddressSet internal _validators; // private → internal for FV ++ EnumerableSet.AddressSet internal _executors; // private → internal for FV + mapping(bytes4 selector => address) private _fallbacks; + + /// @dev The account's {fallback} was called with a selector that doesn't have an installed handler. +@@ -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..4ac6479e807 --- /dev/null +++ b/certora/harnesses/AccountHarness.sol @@ -0,0 +1,52 @@ +// 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"; +import {EnumerableSet} from "../patched/utils/structs/EnumerableSet.sol"; + +contract AccountHarness is AccountERC7702WithModulesMock { + using EnumerableSet for EnumerableSet.AddressSet; + + constructor(string memory name, string memory version) EIP712(name, version) {} + + function getFallbackHandler(bytes4 selector) external view returns (address) { + return _fallbackHandler(selector); + } + + function getDataSelector(bytes memory data) external pure returns (bytes4) { + return bytes4(data); + } + + function _validatorContains(address module) external view returns (bool) { + return _validators.contains(module); + } + + function _validatorLength() external view returns (uint256) { + return _validators.length(); + } + + function _validatorAt(uint256 index) external view returns (address) { + return _validators.at(index); + } + + function _validatorPositionOf(address module) external view returns (uint256) { + return _validators._inner._positions[bytes32(uint256(uint160(module)))]; + } + + function _executorContains(address module) external view returns (bool) { + return _executors.contains(module); + } + + function _executorLength() external view returns (uint256) { + return _executors.length(); + } + + function _executorAt(uint256 index) external view returns (address) { + return _executors.at(index); + } + + function _executorPositionOf(address module) external view returns (uint256) { + return _executors._inner._positions[bytes32(uint256(uint160(module)))]; + } +} 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..403ba570bea --- /dev/null +++ b/certora/specs/Account.spec @@ -0,0 +1,369 @@ +import "helpers/helpers.spec"; +import "methods/IAccount.spec"; + +methods { + function getDataSelector(bytes) external returns (bytes4) envfree; + function getFallbackHandler(bytes4) external returns (address) envfree; + + function _validatorLength() external returns (uint256) envfree; + function _validatorContains(address) external returns (bool) envfree; + function _validatorAt(uint256) external returns (address) envfree; + function _validatorPositionOf(address) external returns (uint256) envfree; + + function _executorLength() external returns (uint256) envfree; + function _executorContains(address) external returns (bool) envfree; + function _executorAt(uint256) external returns (address) envfree; + function _executorPositionOf(address) external returns (uint256) envfree; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Storage consistency - Copied from EnumerableSet.specs │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition moduleLengthSanity() returns bool = + _validatorLength() < max_uint256 && _executorLength() < max_uint256; + +invariant validatorAtUniquenessInvariant(uint256 index1, uint256 index2) + index1 == index2 <=> _validatorAt(index1) == _validatorAt(index2) + filtered { f -> f.selector != sig:execute(bytes32,bytes).selector && f.selector != sig:executeFromExecutor(bytes32,bytes).selector } + { + preserved uninstallModule(uint256 moduleTypeId, address module, bytes deInitData) with (env e) { + requireInvariant validatorAtUniquenessInvariant(index1, require_uint256(_validatorLength() - 1)); + requireInvariant validatorAtUniquenessInvariant(index2, require_uint256(_validatorLength() - 1)); + } + } + +invariant validatorConsistencyKeyInvariant(address module) + _validatorContains(module) <=> ( + _validatorPositionOf(module) > 0 && + _validatorPositionOf(module) <= _validatorLength() && + _validatorAt(require_uint256(_validatorPositionOf(module) - 1)) == module + ) + filtered { f -> f.selector != sig:execute(bytes32,bytes).selector && f.selector != sig:executeFromExecutor(bytes32,bytes).selector } + { + preserved uninstallModule(uint256 moduleTypeId, address otherModule, bytes deInitData) with (env e) { + requireInvariant validatorConsistencyKeyInvariant(otherModule); + requireInvariant validatorAtUniquenessInvariant( + require_uint256(_validatorPositionOf(module) - 1), + require_uint256(_validatorPositionOf(otherModule) - 1) + ); + } + } + +invariant executorAtUniquenessInvariant(uint256 index1, uint256 index2) + index1 == index2 <=> _executorAt(index1) == _executorAt(index2) + filtered { f -> f.selector != sig:execute(bytes32,bytes).selector && f.selector != sig:executeFromExecutor(bytes32,bytes).selector } + { + preserved uninstallModule(uint256 moduleTypeId, address module, bytes deInitData) with (env e) { + requireInvariant executorAtUniquenessInvariant(index1, require_uint256(_executorLength() - 1)); + requireInvariant executorAtUniquenessInvariant(index2, require_uint256(_executorLength() - 1)); + } + } + +invariant executorConsistencyKeyInvariant(address module) + _executorContains(module) <=> ( + _executorPositionOf(module) > 0 && + _executorPositionOf(module) <= _executorLength() && + _executorAt(require_uint256(_executorPositionOf(module) - 1)) == module + ) + filtered { f -> f.selector != sig:execute(bytes32,bytes).selector && f.selector != sig:executeFromExecutor(bytes32,bytes).selector } + { + preserved uninstallModule(uint256 moduleTypeId, address otherModule, bytes deInitData) with (env e) { + requireInvariant executorConsistencyKeyInvariant(otherModule); + requireInvariant executorAtUniquenessInvariant( + require_uint256(_executorPositionOf(module) - 1), + require_uint256(_executorPositionOf(otherModule) - 1) + ); + } + } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Module management │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// This guarantees that at most one fallback module is active for a given initData (i.e. selector) +invariant fallbackModule(address module, bytes initData) + isModuleInstalled(3, module, initData) <=> getFallbackHandler(getDataSelector(initData)) == module; + +rule moduleManagementRule(env e, method f, calldataarg args, uint256 moduleTypeId, address module, bytes additionalContext) + filtered { f -> !f.isView } +{ + 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 + ) + ); +} + +rule installModuleRule(env e, uint256 moduleTypeId, address module, bytes initData) { + uint256 otherModuleTypeId; + address otherModule; + bytes otherInitData; + + require moduleLengthSanity(); + requireInvariant executorConsistencyKeyInvariant(module); + requireInvariant validatorConsistencyKeyInvariant(module); + requireInvariant executorConsistencyKeyInvariant(otherModule); + requireInvariant validatorConsistencyKeyInvariant(otherModule); + + bool isModuleInstalledBefore = isModuleInstalled(moduleTypeId, module, initData); + bool isOtherModuleInstalledBefore = isModuleInstalled(otherModuleTypeId, otherModule, otherInitData); + + installModule(e, moduleTypeId, module, initData); + + bool isModuleInstalledAfter = isModuleInstalled(moduleTypeId, module, initData); + bool isOtherModuleInstalledAfter = isModuleInstalled(otherModuleTypeId, otherModule, otherInitData); + + // Module is installed correctly + assert !isModuleInstalledBefore && isModuleInstalledAfter; + + // No side effect on other modules + assert isOtherModuleInstalledBefore != isOtherModuleInstalledAfter => ( + ( + moduleTypeId == otherModuleTypeId && + module == otherModule + ) || ( + // when a fallback module is installed, the 0 module is "removed" for that selector + moduleTypeId == 3 && // fallback + otherModuleTypeId == 3 && // fallback + otherModule == 0 && + getDataSelector(otherInitData) == getDataSelector(initData) && + isOtherModuleInstalledBefore && + !isOtherModuleInstalledAfter + ) + ); +} + +rule uninstallModuleRule(env e, uint256 moduleTypeId, address module, bytes initData) { + uint256 otherModuleTypeId; + address otherModule; + bytes otherInitData; + + requireInvariant executorConsistencyKeyInvariant(module); + requireInvariant validatorConsistencyKeyInvariant(module); + requireInvariant executorConsistencyKeyInvariant(otherModule); + requireInvariant validatorConsistencyKeyInvariant(otherModule); + + bool isModuleInstalledBefore = isModuleInstalled(moduleTypeId, module, initData); + bool isOtherModuleInstalledBefore = isModuleInstalled(otherModuleTypeId, otherModule, otherInitData); + + uninstallModule(e, moduleTypeId, module, initData); + + bool isModuleInstalledAfter = isModuleInstalled(moduleTypeId, module, initData); + bool isOtherModuleInstalledAfter = isModuleInstalled(otherModuleTypeId, otherModule, otherInitData); + + // Module is installed correctly + assert isModuleInstalledBefore && !isModuleInstalledAfter; + + // No side effect on other modules + assert isOtherModuleInstalledBefore != isOtherModuleInstalledAfter => ( + ( + moduleTypeId == otherModuleTypeId && + module == otherModule + ) || ( + // when a fallback module is uninstalled, the 0 module is "added" for that selector + moduleTypeId == 3 && // fallback + otherModuleTypeId == 3 && // fallback + otherModule == 0 && + getDataSelector(otherInitData) == getDataSelector(initData) && + !isOtherModuleInstalledBefore && + isOtherModuleInstalledAfter + ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ CALL OPCODE │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +persistent ghost mathint calls; +persistent ghost address lastcall_target; +persistent ghost uint32 lastcall_selector; +persistent ghost uint256 lastcall_value; +persistent ghost uint256 lastcall_argsLength; + +hook CALL(uint256 gas, address target, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + if (executingContract == currentContract) { + calls = calls + 1; + lastcall_target = target; + lastcall_selector = selector; + lastcall_value = value; + lastcall_argsLength = argsLength; + } +} + +rule callOpcodeRule(env e, method f, calldataarg args) + filtered { f -> !f.isView } +{ + require calls == 0; + + 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 calls > 0 => ( + ( + // Can call any target with any data and value + f.selector == sig:execute(bytes32,bytes).selector && + isEntryPointOrSelf + ) || ( + // Can call any target with any data and value + f.selector == sig:executeFromExecutor(bytes32,bytes).selector && + isExecutionModule + ) || ( + // Can only call a module without any value. Target is verified by `callInstallModule`. + f.selector == sig:installModule(uint256,address,bytes).selector && + isEntryPointOrSelf && + calls == 1 && + lastcall_selector == 0x6d61fe70 && // onInstall(bytes) + lastcall_value == 0 + ) || ( + // Can only call a module without any value. Target is verified by `callInstallModule`. + f.selector == sig:uninstallModule(uint256,address,bytes).selector && + isEntryPointOrSelf && + calls == 1 && + lastcall_selector == 0x8a91b0e3 && // onUninstall(bytes) + lastcall_value == 0 + ) || ( + // Can send payment to the entrypoint or perform an external signature verification. + f.selector == sig:validateUserOp(Account.PackedUserOperation,bytes32,uint256).selector && + isEntryPoint && + calls <= 2 && + ( + ( + // payPrefund (target is entryPoint and argsLength is 0) + lastcall_target == entryPoint() && + lastcall_value > 0 && + lastcall_argsLength == 0 + ) || ( + // isValidSignatureWithSender (target is as validation module) + isModuleInstalled(1, lastcall_target, context) && + lastcall_selector == 0x97003203 && // validateUserOp(Account.PackedUserOperation,bytes32) + lastcall_value == 0 + ) + ) + ) || ( + // Arbitrary fallback, to the correct fallback handler + f.isFallback && + calls == 1 && + lastcall_target == getFallbackHandler(to_bytes4(lastcall_selector)) && + lastcall_value == e.msg.value + ) + ); +} + +rule callInstallModule(env e, uint256 moduleTypeId, address module, bytes initData) { + require calls == 0; + + installModule(e, moduleTypeId, module, initData); + + assert calls == 1; + assert lastcall_target == module; + assert lastcall_selector == 0x6d61fe70; // onInstall(bytes) + assert lastcall_value == 0; +} + +rule callUninstallModule(env e, uint256 moduleTypeId, address module, bytes deInitData) { + require calls == 0; + + uninstallModule(e, moduleTypeId, module, deInitData); + + assert calls == 1; + assert lastcall_target == module; + assert lastcall_selector == 0x8a91b0e3; // onUninstall(bytes) + assert lastcall_value == 0; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ DELEGATECALL OPCODE │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +persistent ghost mathint delegatecalls; +persistent ghost address lastdelegatecall_target; +persistent ghost uint32 lastdelegatecall_selector; +persistent ghost uint256 lastdelegatecall_argsLength; + +hook DELEGATECALL(uint256 gas, address target, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + if (executingContract == currentContract) { + delegatecalls = delegatecalls + 1; + lastdelegatecall_target = target; + lastdelegatecall_selector = selector; + lastdelegatecall_argsLength = argsLength; + } +} + +rule delegatecallOpcodeRule(env e, method f, calldataarg args) + filtered { f -> !f.isView } +{ + require delegatecalls == 0; + + 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 delegatecalls > 0 => ( + ( + // Can delegatecall to target with any data + f.selector == sig:execute(bytes32,bytes).selector && + isEntryPointOrSelf + ) || ( + // Can delegatecall to target with any data + f.selector == sig:executeFromExecutor(bytes32,bytes).selector && + isExecutionModule + ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ ERC-4337 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule validateUserOpPayment(env e){ + Account.PackedUserOperation userOp; + bytes32 userOpHash; + uint256 missingAccountFunds; + + uint256 balanceBefore = nativeBalances[currentContract]; + validateUserOp(e, userOp, userOpHash, missingAccountFunds); + uint256 balanceAfter = nativeBalances[currentContract]; + + assert balanceBefore - balanceAfter <= missingAccountFunds; +} 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 fabb8821c42..48ddd902dc8 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.1