feat: restore account modules and verification coverage

.gitignore

@@ -15,5 +15,11 @@ docs/
 
 coverage/
 lcov.info
+lcov*.info
 log/
 
+# Local verification output
+.certora_internal/
+coverage_*.log
+scratch_*.log
+scratch_*.txt

certora/AccessControl.conf

@@ -0,0 +1,23 @@
+{
+    "files": [
+        "certora/harness/WeightedECDSAValidatorHarness.sol"
+    ],
+    "verify": "WeightedECDSAValidatorHarness:certora/AccessControl.spec",
+    "solc": "solc8.30",
+    "solc_via_ir": true,
+    "solc_optimize": "20000",
+    "packages": [
+        "src/=src/",
+        "account-abstraction/=dependencies/eth-infinitism-account-abstraction-0.8.0/contracts/",
+        "solady/=dependencies/solady-0.1.26/src/",
+        "openzeppelin-contracts/contracts/=dependencies/@openzeppelin-contracts-5.5.0/",
+        "forge-std/=dependencies/forge-std-1.11.0/src/"
+    ],
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "384",
+    "rule_sanity": "basic",
+    "global_timeout": 600,
+    "msg": "AC-01: validateUserOp success implies a current guardian signed (no signature-less success path)"
+}

certora/AccessControl.spec

@@ -0,0 +1,111 @@
+/*
+ * AC-01 (audit Low, raised in FV as a signature-gating access-control invariant):
+ *   validateUserOp returns a success validationData (i.e. NOT SIG_VALIDATION_FAILED_UINT)
+ *   ONLY IF the address recovered from userOp.signature over toEthSignedMessageHash(userOpHash)
+ *   is a CURRENT guardian for the calling kernel (guardian[recovered][msg.sender].weight != 0).
+ *
+ * Equivalently: any userOp whose signature does NOT recover to an enabled guardian yields
+ * SIG_VALIDATION_FAILED_UINT, regardless of proposal.status (Approved), getApproval.passed,
+ * or paymasterAndData contents. There is NO signature-less success path.
+ *
+ * Target : src/validators/WeightedECDSAValidator.sol:204-272
+ * Success return sites:
+ *   - Ongoing branch  (line 259): gated by `passed && guardian[signer][sender].weight != 0`
+ *                                  where signer = recover(toEthSignedMessageHash(userOpHash), lastSig) (line 248)
+ *   - Approved/passed branch (line 268): gated by `guardian[signer][sender].weight != 0`
+ *                                  where signer = recover(toEthSignedMessageHash(userOpHash), userOp.signature) (line 265)
+ * Pre-fix bug: the Approved/paymaster sub-branch returned VALID with NO signature recovery.
+ *
+ * MODELING (TCB-disclosed):
+ *   - ECDSA.recover(bytes32,bytes memory)  -> uninterpreted `recoverGhost(hash)`.
+ *   - ECDSA.toEthSignedMessageHash(bytes32) -> uninterpreted `ethHashGhost(userOpHash)`.
+ *   - getApproval(...)                      -> NONDET (attacker gets `passed` and `totalWeight`
+ *                                              for free; SOUND over-approximation, and removes
+ *                                              the unbounded guardian linked-list loop).
+ *   recoverGhost is keyed on the *hash* argument only. This is sound for THIS property: the
+ *   success gate depends solely on recover over toEthSignedMessageHash(userOpHash); collapsing
+ *   distinct-signature-same-hash recoveries can only shrink the reachable state, never hide a
+ *   success-with-non-guardian state (which is driven by the userOpHash recovery alone).
+ *
+ * TAUTOLOGY CHECK: the postcondition asserts an access-control OUTCOME (success => the
+ *   userOpHash signer is an enabled guardian). It does not recompute recover or the weight
+ *   lookup; it reads guardian weight and compares the return code. Observable, not tautological.
+ *
+ * REACHABILITY: two witness rules below prove (i) success IS reachable on the Approved branch
+ *   with a real guardian signer (non-vacuous), and (ii) the exact pre-fix bypass
+ *   (paymasterAndData set, signature recovering to a non-guardian) now returns FAILED.
+ *
+ * @author taek <leekt216@gmail.com>
+ */
+
+using WeightedECDSAValidatorHarness as v;
+
+methods {
+    function weightOf(address, address) external returns (uint24) envfree;
+
+    // Uninterpreted ECDSA.recover: deterministic per message hash.
+    function ECDSA.recover(bytes32 hash, bytes memory) internal returns (address) => recoverGhost(hash);
+    // Uninterpreted EIP-191 prefixing: deterministic per raw hash.
+    function ECDSA.toEthSignedMessageHash(bytes32 h) internal returns (bytes32) => ethHashGhost(h);
+    // EIP-712 typed-data hashing for the Approve struct hash (Ongoing loop only). NONDET is
+    // sound: those recoveries feed the getApproval-independent vote tally, never the final gate.
+    function _.toEthSignedMessageHash(bytes32 h) external => ethHashGhost(h) expect bytes32;
+
+    // Guardian linked-list tally: fully symbolic (attacker-favourable). Removes the loop.
+    function getApproval(address, bytes32) external returns (uint256, bool) => NONDET;
+}
+
+ghost recoverGhost(bytes32) returns address;
+ghost ethHashGhost(bytes32) returns bytes32;
+
+definition FAILED() returns uint256 = 1; // SIG_VALIDATION_FAILED_UINT
+
+/*
+ * MAIN PROPERTY.
+ * If validateUserOp does NOT return FAILED, then the signer recovered from userOp.signature
+ * over toEthSignedMessageHash(userOpHash) is a current guardian of the calling kernel.
+ * Covers BOTH success branches (Ongoing line 259 and Approved/passed line 268) and every
+ * value of proposal.status / passed / paymasterAndData, because the assertion is on the
+ * return value irrespective of which branch produced it.
+ */
+rule successImpliesGuardianSigned(env e, WeightedECDSAValidator.PackedUserOperation userOp, bytes32 userOpHash) {
+    uint256 ret = v.validateUserOp(e, userOp, userOpHash);
+
+    address recovered = recoverGhost(ethHashGhost(userOpHash));
+
+    assert ret != FAILED() => weightOf(recovered, e.msg.sender) != 0,
+        "validateUserOp returned success but the userOpHash signer is not a current guardian";
+}
+
+/*
+ * REACHABILITY WITNESS (i) -- success is reachable (non-vacuous).
+ * A userOp on the Approved branch whose signature recovers to a real guardian CAN succeed.
+ * Stated as a violated `assert false` under satisfiable preconditions: if the tool finds a
+ * model, success-with-guardian is reachable.
+ */
+rule successReachableWithGuardian(env e, WeightedECDSAValidator.PackedUserOperation userOp, bytes32 userOpHash) {
+    address recovered = recoverGhost(ethHashGhost(userOpHash));
+    // recovered is an enabled guardian
+    require weightOf(recovered, e.msg.sender) != 0;
+
+    uint256 ret = v.validateUserOp(e, userOp, userOpHash);
+
+    satisfy ret != FAILED();
+}
+
+/*
+ * REACHABILITY WITNESS (ii) -- the exact pre-fix bypass is now BLOCKED.
+ * paymasterAndData is set and the signature recovers to a NON-guardian; the call must FAIL.
+ * (This is a specialization of the main rule pinned to the pre-fix exploit shape, kept
+ * separate so the counterexample, if any, isolates the paymaster path.)
+ */
+rule paymasterNonGuardianFails(env e, WeightedECDSAValidator.PackedUserOperation userOp, bytes32 userOpHash) {
+    require userOp.paymasterAndData.length != 0;                 // paymaster-sponsored
+    address recovered = recoverGhost(ethHashGhost(userOpHash));
+    require weightOf(recovered, e.msg.sender) == 0;              // signer is NOT a guardian
+
+    uint256 ret = v.validateUserOp(e, userOp, userOpHash);
+
+    assert ret == FAILED(),
+        "paymaster-sponsored op with non-guardian signature returned success (pre-fix bypass)";
+}

certora/DSHmut.conf

@@ -0,0 +1,22 @@
+{
+    "files": [
+        "certora/harness/DefaultSecurityHookHarness.sol"
+    ],
+    "verify": "DefaultSecurityHookHarness:certora/DSHmut.spec",
+    "solc": "solc8.30",
+    "solc_via_ir": true,
+    "solc_optimize": "20000",
+    "packages": [
+        "src/=src/",
+        "account-abstraction/=dependencies/eth-infinitism-account-abstraction-0.8.0/contracts/",
+        "solady/=dependencies/solady-0.1.26/src/",
+        "openzeppelin-contracts/contracts/=dependencies/@openzeppelin-contracts-5.5.0/",
+        "forge-std/=dependencies/forge-std-1.11.0/src/"
+    ],
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "384",
+    "global_timeout": 600,
+    "msg": "DSH-ALLOW-01 mutation check: mutants must be violated"
+}

certora/DSHmut.spec

@@ -0,0 +1,44 @@
+methods {
+    function checkCall(address, uint256, bytes) external;
+    function selOf(bytes) external returns (bytes4) envfree;
+    function h_allowed(address, address) external returns (bool) envfree;
+    function h_allSelectorsAllowed(address, address) external returns (bool) envfree;
+    function h_selectorMapped(address, address, bytes4) external returns (bool) envfree;
+    function DefaultSecurityHook._isModule(address) internal returns (bool) => notAModule();
+}
+function notAModule() returns bool { return false; }
+
+definition BLOCKED(bytes4 s) returns bool =
+       s == to_bytes4(0xa9059cbb) || s == to_bytes4(0x095ea7b3) || s == to_bytes4(0x23b872dd)
+    || s == to_bytes4(0x39509351) || s == to_bytes4(0xa457c2d7) || s == to_bytes4(0x42842e0e)
+    || s == to_bytes4(0xb88d4fde) || s == to_bytes4(0xa22cb465) || s == to_bytes4(0xf242432a)
+    || s == to_bytes4(0x2eb2c2d6);
+
+definition ALLOW_PASS(address acct, address target, bytes4 sel) returns bool =
+    h_allowed(acct, target) && ( h_allSelectorsAllowed(acct, target) || h_selectorMapped(acct, target, sel) );
+
+// MUTANT: asserts the OPPOSITE of the real property. Must be VIOLATED (counterexample),
+// proving the assert path is genuinely exercised (deny rule is not vacuous).
+rule mutantDenyDoesNotRevert(address target, bytes data) {
+    env e;
+    require e.msg.value == 0;
+    address account = e.msg.sender;
+    require data.length == 4;
+    bytes4 sel = selOf(data);
+    require BLOCKED(sel);
+    require target != account;
+    require !ALLOW_PASS(account, target, sel);
+    checkCall@withrevert(e, target, 0, data);
+    assert !lastReverted, "MUTANT expected to be violated";
+}
+
+// MUTANT: allSelectorsAllowed but asserts it DOES revert. Must be VIOLATED.
+rule mutantAllPassReverts(address target, uint256 value, bytes data) {
+    env e;
+    require e.msg.value == 0;
+    address account = e.msg.sender;
+    require h_allowed(account, target);
+    require h_allSelectorsAllowed(account, target);
+    checkCall@withrevert(e, target, value, data);
+    assert lastReverted, "MUTANT expected to be violated";
+}

certora/DefaultSecurityHook.conf

@@ -0,0 +1,23 @@
+{
+    "files": [
+        "certora/harness/DefaultSecurityHookHarness.sol"
+    ],
+    "verify": "DefaultSecurityHookHarness:certora/DefaultSecurityHook.spec",
+    "solc": "solc8.30",
+    "solc_via_ir": true,
+    "solc_optimize": "20000",
+    "packages": [
+        "src/=src/",
+        "account-abstraction/=dependencies/eth-infinitism-account-abstraction-0.8.0/contracts/",
+        "solady/=dependencies/solady-0.1.26/src/",
+        "openzeppelin-contracts/contracts/=dependencies/@openzeppelin-contracts-5.5.0/",
+        "forge-std/=dependencies/forge-std-1.11.0/src/"
+    ],
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "hashing_length_bound": "384",
+    "rule_sanity": "basic",
+    "global_timeout": 600,
+    "msg": "DSH-ALLOW-01: allowlist gating exact - blocked non-allowlisted selector reverts"
+}

certora/DefaultSecurityHook.spec

@@ -0,0 +1,137 @@
+/*
+ * DSH-ALLOW-01 — Allowlist gating is exact for blocked token selectors.
+ *
+ * Target: DefaultSecurityHook._checkCall (exposed via harness `checkCall`).
+ *
+ * OBSERVABLE property (not a recompute of _isBlockedSelector):
+ *   Given `sel` (the leading-4-byte selector of `data`, exactly as _checkCall reads
+ *   it) already CONSTRAINED to be one of the 10 blocked selectors — an INPUT
+ *   constraint, NOT a postcondition re-derivation — and given a non-self / non-module
+ *   / zero-value target:
+ *     - if NOT ( allowed && (allSelectorsAllowed || selectorMapped) ) then checkCall
+ *       MUST revert. Self / module / ETH branches are excluded by the preconditions,
+ *       so the only reachable revert is TokenTransferNotAllowed.
+ *   Conversely:
+ *     - if allSelectorsAllowed for the target, checkCall MUST NOT revert regardless of
+ *       selector or value.
+ *
+ * The allowlist facts are read via observable harness accessors
+ * (h_allowed / h_allSelectorsAllowed / h_selectorMapped) — state reads, not a
+ * reimplementation of blocked-set membership. `sel` comes from selOf (a calldata
+ * slice), the SAME key _checkCall uses for the mapping lookup.
+ */
+
+methods {
+    function checkCall(address, uint256, bytes) external; // NOT envfree: reads msg.sender (the account)
+    function selOf(bytes) external returns (bytes4) envfree; // bytes4(data[:4]) as _checkCall reads it
+    function h_allowed(address, address) external returns (bool) envfree;
+    function h_allSelectorsAllowed(address, address) external returns (bool) envfree;
+    function h_selectorMapped(address, address, bytes4) external returns (bool) envfree;
+
+    // _isModule(target) does a raw staticcall probe to `target`. We summarize the
+    // internal function directly to `false`, pinning the STATEMENT's "non-module"
+    // precondition: the module-revert branch is never taken, so a non-allowlisted
+    // blocked selector must flow to the TokenTransferNotAllowed branch.
+    // (The converse rule returns via the allowlist branch before _isModule is reached,
+    //  so this summary does not affect it.)
+    function DefaultSecurityHook._isModule(address) internal returns (bool) => notAModule();
+}
+
+// Non-module summary for _isModule (see methods note).
+function notAModule() returns bool {
+    return false;
+}
+
+// The 10 blocked selectors (input-constraint constants; see tautology note above).
+definition BLOCKED(bytes4 s) returns bool =
+       s == to_bytes4(0xa9059cbb)  // transfer(address,uint256)
+    || s == to_bytes4(0x095ea7b3)  // approve(address,uint256)
+    || s == to_bytes4(0x23b872dd)  // transferFrom(address,address,uint256)
+    || s == to_bytes4(0x39509351)  // increaseAllowance(address,uint256)
+    || s == to_bytes4(0xa457c2d7)  // decreaseAllowance(address,uint256)
+    || s == to_bytes4(0x42842e0e)  // safeTransferFrom(address,address,uint256)
+    || s == to_bytes4(0xb88d4fde)  // safeTransferFrom(address,address,uint256,bytes)
+    || s == to_bytes4(0xa22cb465)  // setApprovalForAll(address,bool)
+    || s == to_bytes4(0xf242432a)  // safeTransferFrom(address,address,uint256,uint256,bytes)
+    || s == to_bytes4(0x2eb2c2d6); // safeBatchTransferFrom(...)
+
+// Observable "allowlisted pass" predicate over harness state reads.
+definition ALLOW_PASS(address acct, address target, bytes4 sel) returns bool =
+    h_allowed(acct, target) && ( h_allSelectorsAllowed(acct, target) || h_selectorMapped(acct, target, sel) );
+
+// ---------------------------------------------------------------------------
+// MAIN RULE: deny direction (security-critical).
+// A blocked selector to a non-self, non-module, zero-value target that is NOT
+// allowlist-passing MUST revert.
+// ---------------------------------------------------------------------------
+rule blockedSelectorDenyReverts(address target, bytes data) {
+    env e;
+    require e.msg.value == 0;
+    address account = e.msg.sender; // account == msg.sender inside _checkCall
+
+    require data.length == 4;       // full selector determined, no trailing bytes
+    bytes4 sel = selOf(data);       // == bytes4(data[:4]) as _checkCall reads it
+
+    // INPUT constraint: selector is a blocked one (not a postcondition re-derivation).
+    require BLOCKED(sel);
+
+    // Preconditions from the STATEMENT: non-self (target!=account), non-module
+    // (_isModule summarized false), zero value (value==0 arg below).
+    require target != account;
+    require !ALLOW_PASS(account, target, sel);
+
+    checkCall@withrevert(e, target, /*value*/ 0, data);
+
+    // With self / module / ETH branches excluded, the ONLY reachable revert is
+    // TokenTransferNotAllowed. Assert it reverts.
+    assert lastReverted, "Blocked, non-allowlisted, non-module, zero-value call did not revert";
+}
+
+// ---------------------------------------------------------------------------
+// CONVERSE RULE: allSelectorsAllowed => never reverts regardless of selector/value.
+// ---------------------------------------------------------------------------
+rule allSelectorsAllowedNeverReverts(address target, uint256 value, bytes data) {
+    env e;
+    require e.msg.value == 0;
+    address account = e.msg.sender;
+
+    require h_allowed(account, target);
+    require h_allSelectorsAllowed(account, target);
+
+    checkCall@withrevert(e, target, value, data);
+
+    assert !lastReverted, "allSelectorsAllowed target reverted";
+}
+
+// ---------------------------------------------------------------------------
+// REACHABILITY WITNESS 1 (mandatory): deny branch is reachable.
+// ---------------------------------------------------------------------------
+rule witnessBlockedReverts(address target, bytes data) {
+    env e;
+    require e.msg.value == 0;
+    address account = e.msg.sender;
+
+    require data.length == 4;
+    bytes4 sel = selOf(data);
+    require BLOCKED(sel);
+    require target != account;
+    require !ALLOW_PASS(account, target, sel);
+
+    checkCall@withrevert(e, target, 0, data);
+    satisfy lastReverted, "no model where a blocked non-allowlisted call reverts";
+}
+
+// ---------------------------------------------------------------------------
+// REACHABILITY WITNESS 2 (mandatory): pass branch is reachable.
+// ---------------------------------------------------------------------------
+rule witnessAllowlistedPasses(address target, bytes data) {
+    env e;
+    require e.msg.value == 0;
+    address account = e.msg.sender;
+
+    require h_allowed(account, target);
+    require h_allSelectorsAllowed(account, target);
+
+    checkCall@withrevert(e, target, 0, data);
+    satisfy !lastReverted, "no model where an allSelectorsAllowed call passes";
+}