Skip to content

Commit a0f686b

Browse files
AmxxAmxx
committed
Formal verification of Account (7702+7579)
1 parent 0aaa23e commit a0f686b

File tree

6 files changed

+167
-2
lines changed

6 files changed

+167
-2
lines changed

‎certora/harnesses/AccountHarness.sol

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.26;
3+
4+
import {AccountERC7702WithModulesMock} from "../patched/mocks/account/AccountMock.sol";
5+
import {EIP712} from "../patched/utils/cryptography/EIP712.sol";
6+
7+
contract AccountHarness is AccountERC7702WithModulesMock {
8+
constructor(string memory name, string memory version) EIP712(name, version) {}
9+
10+
function getFallbackHandler(uint32 selector) external view returns (address) {
11+
return _fallbackHandler(bytes4(selector));
12+
}
13+
}

‎certora/run.js

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ import path from 'path';
1414
import yargs from 'yargs';
1515
import { hideBin } from 'yargs/helpers';
1616
import pLimit from 'p-limit';
17-
import fs from 'fs/promises';
17+
import fs from 'fs';
1818

1919
const argv = yargs(hideBin(process.argv))
2020
.env('')

‎certora/specs.json

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,5 +106,11 @@
106106
"spec": "Nonces",
107107
"contract": "NoncesHarness",
108108
"files": ["certora/harnesses/NoncesHarness.sol"]
109+
},
110+
{
111+
"spec": "Account",
112+
"contract": "AccountHarness",
113+
"files": ["certora/harnesses/AccountHarness.sol"],
114+
"options": ["--optimistic_loop"]
109115
}
110116
]

‎certora/specs/Account.spec

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
import "helpers/helpers.spec";
2+
import "methods/IAccount.spec";
3+
4+
/*
5+
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
6+
│ Module management │
7+
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
8+
*/
9+
rule moduleManagementRule(
10+
env e,
11+
method f,
12+
calldataarg args,
13+
uint256 moduleTypeId,
14+
address module,
15+
bytes additionalContext
16+
) {
17+
bytes context;
18+
require context.length == 0;
19+
20+
bool isEntryPoint = e.msg.sender == entryPoint();
21+
bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract;
22+
bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context);
23+
24+
bool isModuleInstalledBefore = isModuleInstalled(moduleTypeId, module, additionalContext);
25+
f(e, args);
26+
bool isModuleInstalledAfter = isModuleInstalled(moduleTypeId, module, additionalContext);
27+
28+
assert (
29+
isModuleInstalledBefore != isModuleInstalledAfter
30+
) => (
31+
(
32+
f.selector == sig:execute(bytes32,bytes).selector &&
33+
isEntryPointOrSelf
34+
) || (
35+
f.selector == sig:executeFromExecutor(bytes32,bytes).selector &&
36+
isExecutionModule
37+
) || (
38+
f.selector == sig:installModule(uint256,address,bytes).selector &&
39+
isEntryPointOrSelf
40+
) || (
41+
f.selector == sig:uninstallModule(uint256,address,bytes).selector &&
42+
isEntryPointOrSelf
43+
)
44+
);
45+
}
46+
47+
/*
48+
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
49+
│ CALL OPCODE │
50+
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
51+
*/
52+
ghost bool call;
53+
ghost address call_target;
54+
ghost uint256 call_value;
55+
ghost uint256 call_argsLength;
56+
57+
hook CALL(uint256 gas, address target, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc {
58+
call = true;
59+
call_target = target;
60+
call_value = value;
61+
call_argsLength = argsLength;
62+
}
63+
64+
rule callOpcodeRule(
65+
env e,
66+
method f,
67+
calldataarg args
68+
) {
69+
require !call;
70+
71+
bytes context;
72+
require context.length == 0;
73+
74+
bool isEntryPoint = e.msg.sender == entryPoint();
75+
bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract;
76+
bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context);
77+
address fallbackHandler = getFallbackHandler(f.selector);
78+
79+
f(e, args);
80+
81+
assert call => (
82+
(
83+
f.selector == sig:execute(bytes32,bytes).selector &&
84+
isEntryPointOrSelf
85+
) || (
86+
f.selector == sig:executeFromExecutor(bytes32,bytes).selector &&
87+
isExecutionModule
88+
) || (
89+
f.selector == sig:installModule(uint256,address,bytes).selector &&
90+
isEntryPointOrSelf
91+
) || (
92+
f.selector == sig:uninstallModule(uint256,address,bytes).selector &&
93+
isEntryPointOrSelf
94+
) || (
95+
f.selector == sig:validateUserOp(Account.PackedUserOperation,bytes32,uint256).selector &&
96+
isEntryPoint &&
97+
(
98+
// payPrefund (target is entryPoint and argsLength is 0)
99+
(call_target == entryPoint() && call_argsLength == 0 && call_value > 0)
100+
||
101+
// isValidSignatureWithSender (target is as validation module)
102+
(isModuleInstalled(1, call_target, context))
103+
)
104+
) || (
105+
fallbackHandler != 0 &&
106+
call_target == fallbackHandler
107+
)
108+
);
109+
}

‎certora/specs/methods/IAccount.spec

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
methods {
2+
// Account
3+
function entryPoint() external returns (address) envfree;
4+
function getNonce() external returns (uint256) envfree;
5+
function getNonce(uint192) external returns (uint256) envfree;
6+
function validateUserOp(Account.PackedUserOperation,bytes32,uint256) external returns (uint256);
7+
8+
// IERC1271
9+
function isValidSignature(bytes32,bytes) external returns (bytes4);
10+
11+
// IERC7579AccountConfig
12+
function accountId() external returns (string) envfree;
13+
function supportsExecutionMode(bytes32) external returns (bool) envfree;
14+
function supportsModule(uint256) external returns (bool) envfree;
15+
16+
// IERC7579ModuleConfig
17+
function installModule(uint256,address,bytes) external;
18+
function uninstallModule(uint256,address,bytes) external;
19+
function isModuleInstalled(uint256,address,bytes) external returns (bool) envfree;
20+
21+
// IERC7579Execution
22+
function execute(bytes32,bytes) external;
23+
function executeFromExecutor(bytes32,bytes) external returns (bytes[]);
24+
25+
// IERC721Receiver
26+
function onERC721Received(address,address,uint256,bytes) external returns (bytes4) envfree;
27+
28+
// IERC1155Receiver
29+
function onERC1155Received(address,address,uint256,uint256,bytes) external returns (bytes4) envfree;
30+
function onERC1155BatchReceived(address,address,uint256[],uint256[],bytes) external returns (bytes4) envfree;
31+
32+
// IERC165
33+
function supportsInterface(bytes4) external returns (bool) envfree;
34+
35+
// Harness
36+
function getFallbackHandler(uint32) external returns (address) envfree;
37+
}

‎fv-requirements.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
certora-cli==4.13.1
1+
certora-cli==7.31.0
22
# File uses a custom name (fv-requirements.txt) so that it isn't picked by Netlify's build
33
# whose latest Python version is 0.3.8, incompatible with most recent versions of Halmos
44
halmos==0.3.0

0 commit comments

Comments
 (0)